---

Step * of Lemma omral_alg_wf2

∀g:OCMon. ∀r:CDRng.  (omral_alg(g;r) ∈ CAlg(r))
BY
{ ((RepD THENM RepeatM MemTypeCD 
THENM Force `5` (Reduce 0)) THENA Auto) }

1
1. g : OCMon
2. r : CDRng
⊢ omral_alg(g;r) ∈ algebra_sig{i:l}(|r|)

2
1. g : OCMon
2. r : CDRng
⊢ IsGroup(omral_alg(g;r).car;omral_alg(g;r).plus;omral_alg(g;r).zero;omral_alg(g;r).minus)

3
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)
⊢ Comm(omral_alg(g;r).car;omral_alg(g;r).plus)

4
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)

5
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)
5. IsAction(|r|;*;1;omral_alg(g;r).car;omral_alg(g;r).act)
⊢ IsBilinear(|r|;omral_alg(g;r).car;omral_alg(g;r).car;+r;omral_alg(g;r).plus;omral_alg(g;r).plus;omral_alg(g;r).act)

6
1. g : OCMon
2. r : CDRng
⊢ IsMonoid(omral_alg(g;r).car;omral_alg(g;r).times;omral_alg(g;r).one)

7
1. g : OCMon
2. r : CDRng
3. IsMonoid(omral_alg(g;r).car;omral_alg(g;r).times;omral_alg(g;r).one)
⊢ BiLinear(omral_alg(g;r).car;omral_alg(g;r).plus;omral_alg(g;r).times)

8
1. g : OCMon
2. r : CDRng
3. IsMonoid(omral_alg(g;r).car;omral_alg(g;r).times;omral_alg(g;r).one)
4. BiLinear(omral_alg(g;r).car;omral_alg(g;r).plus;omral_alg(g;r).times)
5. a : |r|
⊢ Dist1op2opLR(omral_alg(g;r).car;omral_alg(g;r).act a;omral_alg(g;r).times)

9
.....set predicate..... 
1. g : OCMon
2. r : CDRng
⊢ Comm(omral_alg(g;r).car;omral_alg(g;r).times)

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.    (omral\_alg(g;r)  \mmember{}  CAlg(r))


By

---

Latex:
((RepD  THENM  RepeatM  MemTypeCD 
THENM  Force  `5`  (Reduce  0))  THENA  Auto)

---

Home Index