---

Step * 1 2 of Lemma rng_to_alg_wf

.....set predicate..... 
1. R : Rng
2. Comm(|R|;*)
⊢ IsMonoid(rng_to_alg(R).car;rng_to_alg(R).times;rng_to_alg(R).one)
∧ BiLinear(rng_to_alg(R).car;rng_to_alg(R).plus;rng_to_alg(R).times)
∧ (∀a:|R|. Dist1op2opLR(rng_to_alg(R).car;rng_to_alg(R).act a;rng_to_alg(R).times))
BY
{ AbReduce 0 }

1
1. R : Rng
2. Comm(|R|;*)
⊢ IsMonoid(|R|;*;1) ∧ BiLinear(|R|;+R;*) ∧ (∀a:|R|. Dist1op2opLR(|R|;* a;*))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  R  :  Rng
2.  Comm(|R|;*)
\mvdash{}  IsMonoid(rng\_to\_alg(R).car;rng\_to\_alg(R).times;rng\_to\_alg(R).one)
\mwedge{}  BiLinear(rng\_to\_alg(R).car;rng\_to\_alg(R).plus;rng\_to\_alg(R).times)
\mwedge{}  (\mforall{}a:|R|.  Dist1op2opLR(rng\_to\_alg(R).car;rng\_to\_alg(R).act  a;rng\_to\_alg(R).times))


By

---

Latex:
AbReduce  0

---

Home Index