Step
*
1
of Lemma
module_hom_is_grp_hom
1. A : Rng@i'
2. m : A-Module@i'
3. n : A-Module@i'
4. f : m.car ⟶ n.car@i
5. module_hom_p(A; m; n; f)@i
⊢ ∀a,b:|(m↓grp)|. ((f (a * b)) = ((f a) * (f b)) ∈ |(n↓grp)|)
BY
{ ((ARepD ["compound";"basic"]
THENM Reduce 0
THENM HypBackchain) THEN Auto) }
Latex:
Latex:
1. A : Rng@i'
2. m : A-Module@i'
3. n : A-Module@i'
4. f : m.car {}\mrightarrow{} n.car@i
5. module\_hom\_p(A; m; n; f)@i
\mvdash{} \mforall{}a,b:|(m\mdownarrow{}grp)|. ((f (a * b)) = ((f a) * (f b)))
By
Latex:
((ARepD ["compound";"basic"]
THENM Reduce 0
THENM HypBackchain) THEN Auto)
Home
Index