Metamath Proof Explorer


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 𝑇 ) )