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 𝑇 ) ∧ 𝑈𝑋 ) → ( 𝐹𝑈 ) ∈ 𝑌 )