Theorem islmhmd

Description: Deduction for a module homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015)

	Ref	Expression
Hypotheses	islmhmd.x	|- X = ( Base ` S )
	islmhmd.a	|- .x. = ( .s ` S )
	islmhmd.b	|- .X. = ( .s ` T )
	islmhmd.k	|- K = ( Scalar ` S )
	islmhmd.j	|- J = ( Scalar ` T )
	islmhmd.n	|- N = ( Base ` K )
	islmhmd.s	|- ( ph -> S e. LMod )
	islmhmd.t	|- ( ph -> T e. LMod )
	islmhmd.c	|- ( ph -> J = K )
	islmhmd.f	|- ( ph -> F e. ( S GrpHom T ) )
	islmhmd.l	|- ( ( ph /\ ( x e. N /\ y e. X ) ) -> ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) )
Assertion	islmhmd	|- ( ph -> F e. ( S LMHom T ) )

Proof

Step	Hyp	Ref	Expression
1		islmhmd.x	|- X = ( Base ` S )
2		islmhmd.a	|- .x. = ( .s ` S )
3		islmhmd.b	|- .X. = ( .s ` T )
4		islmhmd.k	|- K = ( Scalar ` S )
5		islmhmd.j	|- J = ( Scalar ` T )
6		islmhmd.n	|- N = ( Base ` K )
7		islmhmd.s	|- ( ph -> S e. LMod )
8		islmhmd.t	|- ( ph -> T e. LMod )
9		islmhmd.c	|- ( ph -> J = K )
10		islmhmd.f	|- ( ph -> F e. ( S GrpHom T ) )
11		islmhmd.l	|- ( ( ph /\ ( x e. N /\ y e. X ) ) -> ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) )
12	11	ralrimivva	|- ( ph -> A. x e. N A. y e. X ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) )
13	10 9 12	3jca	|- ( ph -> ( F e. ( S GrpHom T ) /\ J = K /\ A. x e. N A. y e. X ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) )
14	4 5 6 1 2 3	islmhm	|- ( F e. ( S LMHom T ) <-> ( ( S e. LMod /\ T e. LMod ) /\ ( F e. ( S GrpHom T ) /\ J = K /\ A. x e. N A. y e. X ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )
15	7 8 13 14	syl21anbrc	|- ( ph -> F e. ( S LMHom T ) )