Theorem islmhmd

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

	Ref	Expression
Hypotheses	islmhmd.x	⊢ 𝑋 = ( Base ‘ 𝑆 )
	islmhmd.a	⊢ · = ( ·𝑠 ‘ 𝑆 )
	islmhmd.b	⊢ × = ( ·𝑠 ‘ 𝑇 )
	islmhmd.k	⊢ 𝐾 = ( Scalar ‘ 𝑆 )
	islmhmd.j	⊢ 𝐽 = ( Scalar ‘ 𝑇 )
	islmhmd.n	⊢ 𝑁 = ( Base ‘ 𝐾 )
	islmhmd.s	⊢ ( 𝜑 → 𝑆 ∈ LMod )
	islmhmd.t	⊢ ( 𝜑 → 𝑇 ∈ LMod )
	islmhmd.c	⊢ ( 𝜑 → 𝐽 = 𝐾 )
	islmhmd.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
	islmhmd.l	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) )
Assertion	islmhmd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		islmhmd.x	⊢ 𝑋 = ( Base ‘ 𝑆 )
2		islmhmd.a	⊢ · = ( ·𝑠 ‘ 𝑆 )
3		islmhmd.b	⊢ × = ( ·𝑠 ‘ 𝑇 )
4		islmhmd.k	⊢ 𝐾 = ( Scalar ‘ 𝑆 )
5		islmhmd.j	⊢ 𝐽 = ( Scalar ‘ 𝑇 )
6		islmhmd.n	⊢ 𝑁 = ( Base ‘ 𝐾 )
7		islmhmd.s	⊢ ( 𝜑 → 𝑆 ∈ LMod )
8		islmhmd.t	⊢ ( 𝜑 → 𝑇 ∈ LMod )
9		islmhmd.c	⊢ ( 𝜑 → 𝐽 = 𝐾 )
10		islmhmd.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
11		islmhmd.l	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) )
12	11	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) )
13	10 9 12	3jca	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐽 = 𝐾 ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) ) )
14	4 5 6 1 2 3	islmhm	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ↔ ( ( 𝑆 ∈ LMod ∧ 𝑇 ∈ LMod ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐽 = 𝐾 ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) ) ) )
15	7 8 13 14	syl21anbrc	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )