---

Step * 4 of Lemma omral_alg_wf2


1. g : OCMon
2. r : CDRng
3. IsGroup(omral_alg(g;r).car;omral_alg(g;r).plus;omral_alg(g;r).zero;omral_alg(g;r).minus)
4. Comm(omral_alg(g;r).car;omral_alg(g;r).plus)
⊢ IsAction(|r|;*;1;omral_alg(g;r).car;omral_alg(g;r).act)
BY
{ ((AGenRepD ["compound";"basic"]) THENA Auto) }

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) omral_alg(g;r).act u) = (a omral_alg(g;r).act (b omral_alg(g;r).act u)) ∈ omral_alg(g;r).car

2
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

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  IsGroup(omral\_alg(g;r).car;omral\_alg(g;r).plus;omral\_alg(g;r).zero;omral\_alg(g;r).minus)
4.  Comm(omral\_alg(g;r).car;omral\_alg(g;r).plus)
\mvdash{}  IsAction(|r|;*;1;omral\_alg(g;r).car;omral\_alg(g;r).act)


By

---

Latex:
((AGenRepD  ["compound";"basic"])  THENA  Auto)

---

Home Index