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