---

Step * 1 1 of Lemma rng_of_alg_wf2


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)
BY
{ ((Eval ``ring_p`` 0) THEN Auto) }

---

Latex:

---

Latex:

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.  \mforall{}a:|a|.  Dist1op2opLR(m.car;m.act  a;m.times)
\mvdash{}  IsRing(|m\mdownarrow{}rg|;+m\mdownarrow{}rg;0;-m\mdownarrow{}rg;*;1)


By

---

Latex:
((Eval  ``ring\_p``  0)  THEN  Auto)

---

Home Index