---

Step * of Lemma alg_act_is_rng_chom

∀a:CRng. ∀m:algebra{i:l}(a).  rng_chom_p(a;m↓rg;λx:|a|. m.act x m.one)
BY
{ ((AGenRepD ["compound";"basic"] 
THENM Reduce 0) THENA Auto) }

1
1. a : CRng
2. m : algebra{i:l}(a)
3. a1 : |a|
4. a2 : |a|
⊢ (m.act (a1 +a a2) m.one) = ((m.act a1 m.one) m.plus (m.act a2 m.one)) ∈ m.car

2
1. a : CRng
2. m : algebra{i:l}(a)
3. a1 : |a|
4. a2 : |a|
⊢ (m.act (a1 * a2) m.one) = ((m.act a1 m.one) m.times (m.act a2 m.one)) ∈ m.car

3
1. a : CRng
2. m : algebra{i:l}(a)
⊢ (m.act 1 m.one) = m.one ∈ m.car

4
1. a : CRng
2. m : algebra{i:l}(a)
3. a@0 : |a|
4. b : |a|
⊢ ((m.act a@0 m.one) m.times (m.act b m.one)) = ((m.act b m.one) m.times (m.act a@0 m.one)) ∈ m.car

---

Latex:

---

Latex:
\mforall{}a:CRng.  \mforall{}m:algebra\{i:l\}(a).    rng\_chom\_p(a;m\mdownarrow{}rg;\mlambda{}x:|a|.  m.act  x  m.one)


By

---

Latex:
((AGenRepD  ["compound";"basic"] 
THENM  Reduce  0)  THENA  Auto)

---

Home Index