---

Step * 1 1 2 of Lemma rng_to_alg_wf

.....set predicate..... 
1. R : Rng
2. Comm(|R|;*)
⊢ IsGroup(rng_to_alg(R).car;rng_to_alg(R).plus;rng_to_alg(R).zero;rng_to_alg(R).minus)
∧ Comm(rng_to_alg(R).car;rng_to_alg(R).plus)
∧ IsAction(|R|;*;1;rng_to_alg(R).car;rng_to_alg(R).act)
∧ IsBilinear(|R|;rng_to_alg(R).car;rng_to_alg(R).car;+R;rng_to_alg(R).plus;rng_to_alg(R).plus;rng_to_alg(R).act)
BY
{ AbReduce 0 }

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

---

Latex:

---

Latex:
.....set  predicate..... 
1.  R  :  Rng
2.  Comm(|R|;*)
\mvdash{}  IsGroup(rng\_to\_alg(R).car;rng\_to\_alg(R).plus;rng\_to\_alg(R).zero;rng\_to\_alg(R).minus)
\mwedge{}  Comm(rng\_to\_alg(R).car;rng\_to\_alg(R).plus)
\mwedge{}  IsAction(|R|;*;1;rng\_to\_alg(R).car;rng\_to\_alg(R).act)
\mwedge{}  IsBilinear(|R|;rng\_to\_alg(R).car;rng\_to\_alg(R).car;+R;rng\_to\_alg(R).plus;rng\_to\_alg
                                                                                                                                                          (R).plus;rng\_to\_alg
                                                                                                                                                                                (R).act)


By

---

Latex:
AbReduce  0

---

Home Index