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 e. ( S LMHom T ) /\ U e. Y ) -> ( `' F " U ) e. X )

Proof

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