Metamath Proof Explorer

Theorem lmhmpreima

Description: The inverse 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 lmhmpreima ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) → ( ◡ 𝐹 “ 𝑈 ) ∈ 𝑋 )

Proof

Step Hyp Ref Expression
1 lmhmima.x ⊢ 𝑋 = ( LSubSp ‘ 𝑆 )
2 lmhmima.y ⊢ 𝑌 = ( LSubSp ‘ 𝑇 )
3 lmghm ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
4 lmhmlmod2 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑇 ∈ LMod )
5 2 lsssubg ⊢ ( ( 𝑇 ∈ LMod ∧ 𝑈 ∈ 𝑌 ) → 𝑈 ∈ ( SubGrp ‘ 𝑇 ) )
6 4 5 sylan ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) → 𝑈 ∈ ( SubGrp ‘ 𝑇 ) )
7 ghmpreima ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑇 ) ) → ( ◡ 𝐹 “ 𝑈 ) ∈ ( SubGrp ‘ 𝑆 ) )
8 3 6 7 syl2an2r ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) → ( ◡ 𝐹 “ 𝑈 ) ∈ ( SubGrp ‘ 𝑆 ) )
9 lmhmlmod1 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
10 9 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ) ) → 𝑆 ∈ LMod )
11 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
12 cnvimass ⊢ ( ◡ 𝐹 “ 𝑈 ) ⊆ dom 𝐹
13 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
14 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
15 13 14 lmhmf ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
16 15 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
17 12 16 fssdm ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) → ( ◡ 𝐹 “ 𝑈 ) ⊆ ( Base ‘ 𝑆 ) )
18 17 sselda ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ) → 𝑏 ∈ ( Base ‘ 𝑆 ) )
19 18 adantrl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑆 ) )
20 eqid ⊢ ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑆 )
21 eqid ⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 )
22 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) )
23 13 20 21 22 lmodvscl ⊢ ( ( 𝑆 ∈ LMod ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) )
24 10 11 19 23 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) )
25 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
26 eqid ⊢ ( ·𝑠 ‘ 𝑇 ) = ( ·𝑠 ‘ 𝑇 )
27 20 22 13 21 26 lmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑏 ) ) )
28 25 11 19 27 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑏 ) ) )
29 4 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ) ) → 𝑇 ∈ LMod )
30 simplr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ) ) → 𝑈 ∈ 𝑌 )
31 eqid ⊢ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
32 20 31 lmhmsca ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑆 ) )
33 32 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑆 ) )
34 33 fveq2d ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) → ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
35 34 eleq2d ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) → ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ↔ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) )
36 35 biimpar ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
37 36 adantrr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
38 16 ffund ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) → Fun 𝐹 )
39 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ) ) → 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) )
40 fvimacnvi ⊢ ( ( Fun 𝐹 ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝑈 )
41 38 39 40 syl2an2r ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ) ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝑈 )
42 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ ( Scalar ‘ 𝑇 ) )
43 31 26 42 2 lssvscl ⊢ ( ( ( 𝑇 ∈ LMod ∧ 𝑈 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝑈 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑏 ) ) ∈ 𝑈 )
44 29 30 37 41 43 syl22anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑏 ) ) ∈ 𝑈 )
45 28 44 eqeltrd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) ∈ 𝑈 )
46 ffn ⊢ ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) → 𝐹 Fn ( Base ‘ 𝑆 ) )
47 elpreima ⊢ ( 𝐹 Fn ( Base ‘ 𝑆 ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝑈 ) ↔ ( ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) ∈ 𝑈 ) ) )
48 16 46 47 3syl ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝑈 ) ↔ ( ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) ∈ 𝑈 ) ) )
49 48 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝑈 ) ↔ ( ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) ∈ 𝑈 ) ) )
50 24 45 49 mpbir2and ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝑈 ) )
51 50 ralrimivva ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) → ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∀ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝑈 ) )
52 9 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) → 𝑆 ∈ LMod )
53 20 22 13 21 1 islss4 ⊢ ( 𝑆 ∈ LMod → ( ( ◡ 𝐹 “ 𝑈 ) ∈ 𝑋 ↔ ( ( ◡ 𝐹 “ 𝑈 ) ∈ ( SubGrp ‘ 𝑆 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∀ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝑈 ) ) ) )
54 52 53 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) → ( ( ◡ 𝐹 “ 𝑈 ) ∈ 𝑋 ↔ ( ( ◡ 𝐹 “ 𝑈 ) ∈ ( SubGrp ‘ 𝑆 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∀ 𝑏 ∈ ( ◡ 𝐹 “ 𝑈 ) ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ∈ ( ◡ 𝐹 “ 𝑈 ) ) ) )
55 8 51 54 mpbir2and ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ 𝑌 ) → ( ◡ 𝐹 “ 𝑈 ) ∈ 𝑋 )