This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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