---

Step * 4 1 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. a : |r|
8. b : |r|
9. u : omral_alg(g;r).car
⊢ ((a * b) omral_alg(g;r).act u) = (a omral_alg(g;r).act (b omral_alg(g;r).act u)) ∈ omral_alg(g;r).car
BY
{ % Can't keep reducing or would go too far... % 
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. a : |r|
8. b : |r|
9. u : omral_alg(g;r).car
⊢ ((a * b) ⋅⋅ u) = (a ⋅⋅ (b ⋅⋅ 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.  a  :  |r|
8.  b  :  |r|
9.  u  :  omral\_alg(g;r).car
\mvdash{}  ((a  *  b)  omral\_alg(g;r).act  u)  =  (a  omral\_alg(g;r).act  (b  omral\_alg(g;r).act  u))


By

---

Latex:
\%  Can't  keep  reducing  or  would  go  too  far...  \% 
RWH  AbRedexC  0  THENM  Force  `5`  (Reduce  0)

---

Home Index