---

Step * 1 1 2 1 1 of Lemma rng_to_alg_wf


1. R : Rng
2. IsRing(|R|;+R;0;-R;*;1)
3. Comm(|R|;*)
⊢ IsGroup(|R|;+R;0;-R) ∧ Comm(|R|;+R) ∧ IsAction(|R|;*;1;|R|;*) ∧ IsBilinear(|R|;|R|;|R|;+R;+R;+R;*)
BY
{ Unfold `ring_p` 2 }

1
1. R : Rng
2. IsGroup(|R|;+R;0;-R) ∧ IsMonoid(|R|;*;1) ∧ BiLinear(|R|;+R;*)
3. Comm(|R|;*)
⊢ IsGroup(|R|;+R;0;-R) ∧ Comm(|R|;+R) ∧ IsAction(|R|;*;1;|R|;*) ∧ IsBilinear(|R|;|R|;|R|;+R;+R;+R;*)

---

Latex:

---

Latex:

1.  R  :  Rng
2.  IsRing(|R|;+R;0;-R;*;1)
3.  Comm(|R|;*)
\mvdash{}  IsGroup(|R|;+R;0;-R)  \mwedge{}  Comm(|R|;+R)  \mwedge{}  IsAction(|R|;*;1;|R|;*)  \mwedge{}  IsBilinear(|R|;|R|;|R|;+R;+R;+R;*)


By

---

Latex:
Unfold  `ring\_p`  2

---

Home Index