Metamath Proof Explorer

Theorem reslmhm2

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 reslmhm2 ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ∧ 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ) → 𝐹 ∈ ( 𝑆 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 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ∧ 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ) → 𝑆 ∈ LMod )
11 simp2 ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ∧ 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ) → 𝑇 ∈ LMod )
12 1 7 resssca ⊢ ( 𝑋 ∈ 𝐿 → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑈 ) )
13 12 3ad2ant3 ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ∧ 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ) → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑈 ) )
14 eqid ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
15 6 14 lmhmsca ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) → ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑆 ) )
16 15 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ∧ 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ) → ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑆 ) )
17 13 16 eqtrd ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ∧ 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ) → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑆 ) )
18 lmghm ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) )
19 18 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ∧ 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) )
20 2 lsssubg ⊢ ( ( 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ) → 𝑋 ∈ ( SubGrp ‘ 𝑇 ) )
21 20 3adant1 ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ∧ 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ) → 𝑋 ∈ ( SubGrp ‘ 𝑇 ) )
22 1 resghm2 ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ∧ 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
23 19 21 22 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ∧ 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
24 eqid ⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
25 6 8 3 4 24 lmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) )
26 25 3expb ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) )
27 26 3ad2antl1 ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ∧ 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) )
28 simpl3 ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ∧ 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑋 ∈ 𝐿 )
29 1 5 ressvsca ⊢ ( 𝑋 ∈ 𝐿 → ( ·𝑠 ‘ 𝑇 ) = ( ·𝑠 ‘ 𝑈 ) )
30 29 oveqd ⊢ ( 𝑋 ∈ 𝐿 → ( 𝑥 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) )
31 28 30 syl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ∧ 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) )
32 27 31 eqtr4d ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ∧ 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
33 3 4 5 6 7 8 10 11 17 23 32 islmhmd ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑈 ) ∧ 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )