---

Step * 1 1 2 1 of Lemma rng_to_alg_wf


1. R : Rng
2. Comm(|R|;*)
⊢ IsGroup(|R|;+R;0;-R) ∧ Comm(|R|;+R) ∧ IsAction(|R|;*;1;|R|;*) ∧ IsBilinear(|R|;|R|;|R|;+R;+R;+R;*)
BY
{ AddProperties 1 }

1
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;*)

---

Latex:

---

Latex:

1.  R  :  Rng
2.  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:
AddProperties  1

---

Home Index