---

Step * 1 1 of Lemma rng_to_alg_wf


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

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

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

3
.....wf..... 
1. R : Rng
2. Comm(|R|;*)
3. m : algebra_sig{i:l}(|R|)
⊢ IsGroup(m.car;m.plus;m.zero;m.minus)
  ∧ Comm(m.car;m.plus)
  ∧ IsAction(|R|;*;1;m.car;m.act)
  ∧ IsBilinear(|R|;m.car;m.car;+R;m.plus;m.plus;m.act) ∈ Type

---

Latex:

---

Latex:

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


By

---

Latex:
MemTypeCD

---

Home Index