Metamath Proof Explorer

Theorem lmhmima

Description: The image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015)

Ref Expression
Hypotheses lmhmima.x ⊢ 𝑋 = ( LSubSp ‘ 𝑆 )
lmhmima.y ⊢ 𝑌 = ( LSubSp ‘ 𝑇 )
Assertion lmhmima ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) → ( 𝐹 “ 𝑈 ) ∈ 𝑌 )

Proof

Step Hyp Ref Expression
1 lmhmima.x ⊢ 𝑋 = ( LSubSp ‘ 𝑆 )
2 lmhmima.y ⊢ 𝑌 = ( LSubSp ‘ 𝑇 )
3 lmghm ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
4 lmhmlmod1 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
5 simpr ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) → 𝑈 ∈ 𝑋 )
6 1 lsssubg ⊢ ( ( 𝑆 ∈ LMod ∧ 𝑈 ∈ 𝑋 ) → 𝑈 ∈ ( SubGrp ‘ 𝑆 ) )
7 4 5 6 syl2an2r ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) → 𝑈 ∈ ( SubGrp ‘ 𝑆 ) )
8 ghmima ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑆 ) ) → ( 𝐹 “ 𝑈 ) ∈ ( SubGrp ‘ 𝑇 ) )
9 3 7 8 syl2an2r ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) → ( 𝐹 “ 𝑈 ) ∈ ( SubGrp ‘ 𝑇 ) )
10 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
11 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
12 10 11 lmhmf ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
13 12 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
14 ffn ⊢ ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) → 𝐹 Fn ( Base ‘ 𝑆 ) )
15 13 14 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) → 𝐹 Fn ( Base ‘ 𝑆 ) )
16 10 1 lssss ⊢ ( 𝑈 ∈ 𝑋 → 𝑈 ⊆ ( Base ‘ 𝑆 ) )
17 5 16 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) → 𝑈 ⊆ ( Base ‘ 𝑆 ) )
18 15 17 fvelimabd ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) → ( 𝑏 ∈ ( 𝐹 “ 𝑈 ) ↔ ∃ 𝑐 ∈ 𝑈 ( 𝐹 ‘ 𝑐 ) = 𝑏 ) )
19 18 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ) → ( 𝑏 ∈ ( 𝐹 “ 𝑈 ) ↔ ∃ 𝑐 ∈ 𝑈 ( 𝐹 ‘ 𝑐 ) = 𝑏 ) )
20 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑐 ∈ 𝑈 ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
21 eqid ⊢ ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑆 )
22 eqid ⊢ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
23 21 22 lmhmsca ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑆 ) )
24 23 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑆 ) )
25 24 fveq2d ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) → ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
26 25 eleq2d ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) → ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ↔ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) )
27 26 biimpa ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
28 27 adantrr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑐 ∈ 𝑈 ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
29 17 sselda ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑈 ) → 𝑐 ∈ ( Base ‘ 𝑆 ) )
30 29 adantrl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑐 ∈ 𝑈 ) ) → 𝑐 ∈ ( Base ‘ 𝑆 ) )
31 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) )
32 eqid ⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 )
33 eqid ⊢ ( ·𝑠 ‘ 𝑇 ) = ( ·𝑠 ‘ 𝑇 )
34 21 31 10 32 33 lmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑐 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑐 ) ) )
35 20 28 30 34 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑐 ∈ 𝑈 ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑐 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑐 ) ) )
36 20 12 14 3syl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑐 ∈ 𝑈 ) ) → 𝐹 Fn ( Base ‘ 𝑆 ) )
37 simplr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑐 ∈ 𝑈 ) ) → 𝑈 ∈ 𝑋 )
38 37 16 syl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑐 ∈ 𝑈 ) ) → 𝑈 ⊆ ( Base ‘ 𝑆 ) )
39 4 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) → 𝑆 ∈ LMod )
40 39 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑐 ∈ 𝑈 ) ) → 𝑆 ∈ LMod )
41 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑐 ∈ 𝑈 ) ) → 𝑐 ∈ 𝑈 )
42 21 32 31 1 lssvscl ⊢ ( ( ( 𝑆 ∈ LMod ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑐 ∈ 𝑈 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑐 ) ∈ 𝑈 )
43 40 37 28 41 42 syl22anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑐 ∈ 𝑈 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑐 ) ∈ 𝑈 )
44 fnfvima ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑆 ) ∧ 𝑈 ⊆ ( Base ‘ 𝑆 ) ∧ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑐 ) ∈ 𝑈 ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑐 ) ) ∈ ( 𝐹 “ 𝑈 ) )
45 36 38 43 44 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑐 ∈ 𝑈 ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑐 ) ) ∈ ( 𝐹 “ 𝑈 ) )
46 35 45 eqeltrrd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑐 ∈ 𝑈 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑐 ) ) ∈ ( 𝐹 “ 𝑈 ) )
47 46 anassrs ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ) ∧ 𝑐 ∈ 𝑈 ) → ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑐 ) ) ∈ ( 𝐹 “ 𝑈 ) )
48 oveq2 ⊢ ( ( 𝐹 ‘ 𝑐 ) = 𝑏 → ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑐 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) 𝑏 ) )
49 48 eleq1d ⊢ ( ( 𝐹 ‘ 𝑐 ) = 𝑏 → ( ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑐 ) ) ∈ ( 𝐹 “ 𝑈 ) ↔ ( 𝑎 ( ·𝑠 ‘ 𝑇 ) 𝑏 ) ∈ ( 𝐹 “ 𝑈 ) ) )
50 47 49 syl5ibcom ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ) ∧ 𝑐 ∈ 𝑈 ) → ( ( 𝐹 ‘ 𝑐 ) = 𝑏 → ( 𝑎 ( ·𝑠 ‘ 𝑇 ) 𝑏 ) ∈ ( 𝐹 “ 𝑈 ) ) )
51 50 rexlimdva ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ) → ( ∃ 𝑐 ∈ 𝑈 ( 𝐹 ‘ 𝑐 ) = 𝑏 → ( 𝑎 ( ·𝑠 ‘ 𝑇 ) 𝑏 ) ∈ ( 𝐹 “ 𝑈 ) ) )
52 19 51 sylbid ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ) → ( 𝑏 ∈ ( 𝐹 “ 𝑈 ) → ( 𝑎 ( ·𝑠 ‘ 𝑇 ) 𝑏 ) ∈ ( 𝐹 “ 𝑈 ) ) )
53 52 impr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏 ∈ ( 𝐹 “ 𝑈 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑇 ) 𝑏 ) ∈ ( 𝐹 “ 𝑈 ) )
54 53 ralrimivva ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) → ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∀ 𝑏 ∈ ( 𝐹 “ 𝑈 ) ( 𝑎 ( ·𝑠 ‘ 𝑇 ) 𝑏 ) ∈ ( 𝐹 “ 𝑈 ) )
55 lmhmlmod2 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑇 ∈ LMod )
56 55 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) → 𝑇 ∈ LMod )
57 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ ( Scalar ‘ 𝑇 ) )
58 22 57 11 33 2 islss4 ⊢ ( 𝑇 ∈ LMod → ( ( 𝐹 “ 𝑈 ) ∈ 𝑌 ↔ ( ( 𝐹 “ 𝑈 ) ∈ ( SubGrp ‘ 𝑇 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∀ 𝑏 ∈ ( 𝐹 “ 𝑈 ) ( 𝑎 ( ·𝑠 ‘ 𝑇 ) 𝑏 ) ∈ ( 𝐹 “ 𝑈 ) ) ) )
59 56 58 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) → ( ( 𝐹 “ 𝑈 ) ∈ 𝑌 ↔ ( ( 𝐹 “ 𝑈 ) ∈ ( SubGrp ‘ 𝑇 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∀ 𝑏 ∈ ( 𝐹 “ 𝑈 ) ( 𝑎 ( ·𝑠 ‘ 𝑇 ) 𝑏 ) ∈ ( 𝐹 “ 𝑈 ) ) ) )
60 9 54 59 mpbir2and ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ) → ( 𝐹 “ 𝑈 ) ∈ 𝑌 )