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∈SLMHomT∧U∈Y→F-1U∈X

Proof

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