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

Metamath Proof Explorer

Theorem islmhm3

Description: Property of a module homomorphism, similar to ismhm . (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Hypotheses islmhm.k ⊢ 𝐾 = ( Scalar ‘ 𝑆 )
islmhm.l ⊢ 𝐿 = ( Scalar ‘ 𝑇 )
islmhm.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
islmhm.e ⊢ 𝐸 = ( Base ‘ 𝑆 )
islmhm.m ⊢ · = ( ·𝑠 ‘ 𝑆 )
islmhm.n ⊢ × = ( ·𝑠 ‘ 𝑇 )
Assertion islmhm3 ( ( 𝑆 ∈ LMod ∧ 𝑇 ∈ LMod ) → ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ↔ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 islmhm.k ⊢ 𝐾 = ( Scalar ‘ 𝑆 )
2 islmhm.l ⊢ 𝐿 = ( Scalar ‘ 𝑇 )
3 islmhm.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
4 islmhm.e ⊢ 𝐸 = ( Base ‘ 𝑆 )
5 islmhm.m ⊢ · = ( ·𝑠 ‘ 𝑆 )
6 islmhm.n ⊢ × = ( ·𝑠 ‘ 𝑇 )
7 1 2 3 4 5 6 islmhm ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ↔ ( ( 𝑆 ∈ LMod ∧ 𝑇 ∈ LMod ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) ) ) )
8 7 baib ⊢ ( ( 𝑆 ∈ LMod ∧ 𝑇 ∈ LMod ) → ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ↔ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐿 = 𝐾 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐸 ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑥 × ( 𝐹 ‘ 𝑦 ) ) ) ) )