Metamath Proof Explorer


Theorem reslmhm2b

Description: Expansion of the codomain of a homomorphism. (Contributed by Stefan O'Rear, 3-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

Ref Expression
Hypotheses reslmhm2.u 𝑈 = ( 𝑇s 𝑋 )
reslmhm2.l 𝐿 = ( LSubSp ‘ 𝑇 )
Assertion reslmhm2b ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) → ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 reslmhm2.u 𝑈 = ( 𝑇s 𝑋 )
2 reslmhm2.l 𝐿 = ( LSubSp ‘ 𝑇 )
3 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
4 eqid ( ·𝑠𝑆 ) = ( ·𝑠𝑆 )
5 eqid ( ·𝑠𝑈 ) = ( ·𝑠𝑈 )
6 eqid ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑆 )
7 eqid ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
8 eqid ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) )
9 lmhmlmod1 ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
10 9 adantl ( ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ) → 𝑆 ∈ LMod )
11 simpl1 ( ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ) → 𝑇 ∈ LMod )
12 simpl2 ( ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ) → 𝑋𝐿 )
13 1 2 lsslmod ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ) → 𝑈 ∈ LMod )
14 11 12 13 syl2anc ( ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ) → 𝑈 ∈ LMod )
15 eqid ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
16 1 15 resssca ( 𝑋𝐿 → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑈 ) )
17 16 3ad2ant2 ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑈 ) )
18 6 15 lmhmsca ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑆 ) )
19 17 18 sylan9req ( ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ) → ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑆 ) )
20 lmghm ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
21 2 lsssubg ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ) → 𝑋 ∈ ( SubGrp ‘ 𝑇 ) )
22 1 resghm2b ( ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ∧ ran 𝐹𝑋 ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ) )
23 21 22 stoic3 ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ) )
24 23 biimpa ( ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) )
25 20 24 sylan2 ( ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) )
26 eqid ( ·𝑠𝑇 ) = ( ·𝑠𝑇 )
27 6 8 3 4 26 lmhmlin ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠𝑆 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠𝑇 ) ( 𝐹𝑦 ) ) )
28 27 3expb ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠𝑆 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠𝑇 ) ( 𝐹𝑦 ) ) )
29 28 adantll ( ( ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠𝑆 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠𝑇 ) ( 𝐹𝑦 ) ) )
30 simpll2 ( ( ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑋𝐿 )
31 1 26 ressvsca ( 𝑋𝐿 → ( ·𝑠𝑇 ) = ( ·𝑠𝑈 ) )
32 31 oveqd ( 𝑋𝐿 → ( 𝑥 ( ·𝑠𝑇 ) ( 𝐹𝑦 ) ) = ( 𝑥 ( ·𝑠𝑈 ) ( 𝐹𝑦 ) ) )
33 30 32 syl ( ( ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠𝑇 ) ( 𝐹𝑦 ) ) = ( 𝑥 ( ·𝑠𝑈 ) ( 𝐹𝑦 ) ) )
34 29 33 eqtrd ( ( ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠𝑆 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠𝑈 ) ( 𝐹𝑦 ) ) )
35 3 4 5 6 7 8 10 14 19 25 34 islmhmd ( ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) )
36 simpr ( ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) )
37 simpl1 ( ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ) → 𝑇 ∈ LMod )
38 simpl2 ( ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ) → 𝑋𝐿 )
39 1 2 reslmhm2 ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ∧ 𝑇 ∈ LMod ∧ 𝑋𝐿 ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
40 36 37 38 39 syl3anc ( ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) ∧ 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
41 35 40 impbida ( ( 𝑇 ∈ LMod ∧ 𝑋𝐿 ∧ ran 𝐹𝑋 ) → ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ) )