---

Step * 1 of Lemma rng_of_alg_wf2


1. a : CRng@i'
2. m : algebra{i:l}(a)@i'
⊢ m↓rg ∈ Rng
BY
{ ((AddAllProperties 2 
THENM RepeatM MemTypeCD) THEN Auto) }

1
1. a : CRng@i'
2. m : algebra{i:l}(a)@i'
3. IsGroup(m.car;m.plus;m.zero;m.minus)
4. Comm(m.car;m.plus)
5. IsAction(|a|;*;1;m.car;m.act)
6. IsBilinear(|a|;m.car;m.car;+a;m.plus;m.plus;m.act)
7. IsMonoid(m.car;m.times;m.one)
8. BiLinear(m.car;m.plus;m.times)
9. ∀a:|a|. Dist1op2opLR(m.car;m.act a;m.times)
⊢ IsRing(|m↓rg|;+m↓rg;0;-m↓rg;*;1)

---

Latex:

---

Latex:

1.  a  :  CRng@i'
2.  m  :  algebra\{i:l\}(a)@i'
\mvdash{}  m\mdownarrow{}rg  \mmember{}  Rng


By

---

Latex:
((AddAllProperties  2 
THENM  RepeatM  MemTypeCD)  THEN  Auto)

---

Home Index