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 ⊢ X = LSubSp ⁡ S
lmhmima.y ⊢ Y = LSubSp ⁡ T
Assertion lmhmpreima ⊢ F ∈ S LMHom T ∧ U ∈ Y → F -1 U ∈ X

Proof

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