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