---

Step * 1 of Lemma rng_to_alg_wf


1. R : Rng
2. Comm(|R|;*)
⊢ rng_to_alg(R) ∈ algebra{i:l}(R)
BY
{ MemTypeCD }

1
1. R : Rng
2. Comm(|R|;*)
⊢ rng_to_alg(R) ∈ R-Module

2
.....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))

3
.....wf..... 
1. R : Rng
2. Comm(|R|;*)
3. m : R-Module
⊢ IsMonoid(m.car;m.times;m.one) ∧ BiLinear(m.car;m.plus;m.times) ∧ (∀a:|R|. Dist1op2opLR(m.car;m.act a;m.times)) ∈ Type

---

Latex:

---

Latex:

1.  R  :  Rng
2.  Comm(|R|;*)
\mvdash{}  rng\_to\_alg(R)  \mmember{}  algebra\{i:l\}(R)


By

---

Latex:
MemTypeCD

---

Home Index