Step
*
1
of Lemma
ident_mon_hom_shift
1. g : GrpSig
2. h : GrpSig
3. f : MonHom(g,h)
4. ∀[a1,a2:|g|]. ((f (a1 * a2)) = ((f a1) * (f a2)) ∈ |h|)
5. (f e) = e ∈ |h|
6. ∀a1,a2:|g|. (((f a1) = (f a2) ∈ |h|)
⇒ (a1 = a2 ∈ |g|))
7. ∀[x:|h|]. (((x * e) = x ∈ |h|) ∧ ((e * x) = x ∈ |h|))
8. x : |g|
⊢ ((x * e) = x ∈ |g|) ∧ ((e * x) = x ∈ |g|)
BY
{ ((D 0
THENM BHyp 6
THENM RWW "4 5" 0
THENM BHyp 7) THENA Auto) }
Latex:
Latex:
1. g : GrpSig
2. h : GrpSig
3. f : MonHom(g,h)
4. \mforall{}[a1,a2:|g|]. ((f (a1 * a2)) = ((f a1) * (f a2)))
5. (f e) = e
6. \mforall{}a1,a2:|g|. (((f a1) = (f a2)) {}\mRightarrow{} (a1 = a2))
7. \mforall{}[x:|h|]. (((x * e) = x) \mwedge{} ((e * x) = x))
8. x : |g|
\mvdash{} ((x * e) = x) \mwedge{} ((e * x) = x)
By
Latex:
((D 0
THENM BHyp 6
THENM RWW "4 5" 0
THENM BHyp 7) THENA Auto)
Home
Index