---

Step * 4 2 of Lemma omral_alg_wf2


1. g : OCMon
2. r : CDRng
3. ∀[x,y,z:omral_alg(g;r).car].
     ((x omral_alg(g;r).plus (y omral_alg(g;r).plus z))
     = ((x omral_alg(g;r).plus y) omral_alg(g;r).plus z)
     ∈ omral_alg(g;r).car)
4. ∀[x:omral_alg(g;r).car]
     (((x omral_alg(g;r).plus omral_alg(g;r).zero) = x ∈ omral_alg(g;r).car)
     ∧ ((omral_alg(g;r).zero omral_alg(g;r).plus x) = x ∈ omral_alg(g;r).car))
5. ∀[x:omral_alg(g;r).car]
     (((x omral_alg(g;r).plus (omral_alg(g;r).minus x)) = omral_alg(g;r).zero ∈ omral_alg(g;r).car)
     ∧ (((omral_alg(g;r).minus x) omral_alg(g;r).plus x) = omral_alg(g;r).zero ∈ omral_alg(g;r).car))
6. ∀[x,y:omral_alg(g;r).car].  ((x omral_alg(g;r).plus y) = (y omral_alg(g;r).plus x) ∈ omral_alg(g;r).car)
7. u : omral_alg(g;r).car
⊢ (1 omral_alg(g;r).act u) = u ∈ omral_alg(g;r).car
BY
{ RWH AbRedexC 0 THENM Force `5` (Reduce 0) }

1
1. g : OCMon
2. r : CDRng
3. ∀[x,y,z:omral_alg(g;r).car].
     ((x omral_alg(g;r).plus (y omral_alg(g;r).plus z))
     = ((x omral_alg(g;r).plus y) omral_alg(g;r).plus z)
     ∈ omral_alg(g;r).car)
4. ∀[x:omral_alg(g;r).car]
     (((x omral_alg(g;r).plus omral_alg(g;r).zero) = x ∈ omral_alg(g;r).car)
     ∧ ((omral_alg(g;r).zero omral_alg(g;r).plus x) = x ∈ omral_alg(g;r).car))
5. ∀[x:omral_alg(g;r).car]
     (((x omral_alg(g;r).plus (omral_alg(g;r).minus x)) = omral_alg(g;r).zero ∈ omral_alg(g;r).car)
     ∧ (((omral_alg(g;r).minus x) omral_alg(g;r).plus x) = omral_alg(g;r).zero ∈ omral_alg(g;r).car))
6. ∀[x,y:omral_alg(g;r).car].  ((x omral_alg(g;r).plus y) = (y omral_alg(g;r).plus x) ∈ omral_alg(g;r).car)
7. u : omral_alg(g;r).car
⊢ (1 ⋅⋅ u) = u ∈ |omral(g;r)|

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  \mforall{}[x,y,z:omral\_alg(g;r).car].
          ((x  omral\_alg(g;r).plus  (y  omral\_alg(g;r).plus  z))
          =  ((x  omral\_alg(g;r).plus  y)  omral\_alg(g;r).plus  z))
4.  \mforall{}[x:omral\_alg(g;r).car]
          (((x  omral\_alg(g;r).plus  omral\_alg(g;r).zero)  =  x)
          \mwedge{}  ((omral\_alg(g;r).zero  omral\_alg(g;r).plus  x)  =  x))
5.  \mforall{}[x:omral\_alg(g;r).car]
          (((x  omral\_alg(g;r).plus  (omral\_alg(g;r).minus  x))  =  omral\_alg(g;r).zero)
          \mwedge{}  (((omral\_alg(g;r).minus  x)  omral\_alg(g;r).plus  x)  =  omral\_alg(g;r).zero))
6.  \mforall{}[x,y:omral\_alg(g;r).car].    ((x  omral\_alg(g;r).plus  y)  =  (y  omral\_alg(g;r).plus  x))
7.  u  :  omral\_alg(g;r).car
\mvdash{}  (1  omral\_alg(g;r).act  u)  =  u


By

---

Latex:
RWH  AbRedexC  0  THENM  Force  `5`  (Reduce  0)

---

Home Index