---

Step * of Lemma oal_lv_neg

∀s:LOSet. ∀g:AbDGrp. ∀ps:|oal(s;g)|.  ((¬(ps = 00 ∈ |oal(s;g)|)) ⇒ (lv(--ps) = (~ lv(ps)) ∈ |g|))
BY
{ ((RepD THENM RWW "lookup_oal_lk<" 0) THENA Auto) }

1
.....rewrite subgoal..... 
1. s : LOSet
2. g : AbDGrp
3. ps : |oal(s;g)|
4. ¬(ps = 00 ∈ |oal(s;g)|)
⊢ ¬((--ps) = 00 ∈ |oal(s;g)|)

2
1. s : LOSet
2. g : AbDGrp
3. ps : |oal(s;g)|
4. ¬(ps = 00 ∈ |oal(s;g)|)
⊢ ((--ps)[lk(--ps)]) = (~ (ps[lk(ps)])) ∈ |g|

---

Latex:

---

Latex:
\mforall{}s:LOSet.  \mforall{}g:AbDGrp.  \mforall{}ps:|oal(s;g)|.    ((\mneg{}(ps  =  00))  {}\mRightarrow{}  (lv(--ps)  =  (\msim{}  lv(ps))))


By

---

Latex:
((RepD  THENM  RWW  "lookup\_oal\_lk<"  0)  THENA  Auto)

---

Home Index