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 
|- X = ( LSubSp ` S )
lmhmima.y 
|- Y = ( LSubSp ` T )
Assertion lmhmima 
|- ( ( F e. ( S LMHom T ) /\ U e. X ) -> ( F " U ) e. Y )

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 lmhmlmod1 
 |-  ( F e. ( S LMHom T ) -> S e. LMod )
5 simpr 
 |-  ( ( F e. ( S LMHom T ) /\ U e. X ) -> U e. X )
6 1 lsssubg 
 |-  ( ( S e. LMod /\ U e. X ) -> U e. ( SubGrp ` S ) )
7 4 5 6 syl2an2r 
 |-  ( ( F e. ( S LMHom T ) /\ U e. X ) -> U e. ( SubGrp ` S ) )
8 ghmima 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. ( SubGrp ` S ) ) -> ( F " U ) e. ( SubGrp ` T ) )
9 3 7 8 syl2an2r 
 |-  ( ( F e. ( S LMHom T ) /\ U e. X ) -> ( F " U ) e. ( SubGrp ` T ) )
10 eqid 
 |-  ( Base ` S ) = ( Base ` S )
11 eqid 
 |-  ( Base ` T ) = ( Base ` T )
12 10 11 lmhmf 
 |-  ( F e. ( S LMHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
13 12 adantr 
 |-  ( ( F e. ( S LMHom T ) /\ U e. X ) -> F : ( Base ` S ) --> ( Base ` T ) )
14 ffn 
 |-  ( F : ( Base ` S ) --> ( Base ` T ) -> F Fn ( Base ` S ) )
15 13 14 syl 
 |-  ( ( F e. ( S LMHom T ) /\ U e. X ) -> F Fn ( Base ` S ) )
16 10 1 lssss 
 |-  ( U e. X -> U C_ ( Base ` S ) )
17 5 16 syl 
 |-  ( ( F e. ( S LMHom T ) /\ U e. X ) -> U C_ ( Base ` S ) )
18 15 17 fvelimabd 
 |-  ( ( F e. ( S LMHom T ) /\ U e. X ) -> ( b e. ( F " U ) <-> E. c e. U ( F ` c ) = b ) )
19 18 adantr 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ a e. ( Base ` ( Scalar ` T ) ) ) -> ( b e. ( F " U ) <-> E. c e. U ( F ` c ) = b ) )
20 simpll 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ c e. U ) ) -> F e. ( S LMHom T ) )
21 eqid 
 |-  ( Scalar ` S ) = ( Scalar ` S )
22 eqid 
 |-  ( Scalar ` T ) = ( Scalar ` T )
23 21 22 lmhmsca 
 |-  ( F e. ( S LMHom T ) -> ( Scalar ` T ) = ( Scalar ` S ) )
24 23 adantr 
 |-  ( ( F e. ( S LMHom T ) /\ U e. X ) -> ( Scalar ` T ) = ( Scalar ` S ) )
25 24 fveq2d 
 |-  ( ( F e. ( S LMHom T ) /\ U e. X ) -> ( Base ` ( Scalar ` T ) ) = ( Base ` ( Scalar ` S ) ) )
26 25 eleq2d 
 |-  ( ( F e. ( S LMHom T ) /\ U e. X ) -> ( a e. ( Base ` ( Scalar ` T ) ) <-> a e. ( Base ` ( Scalar ` S ) ) ) )
27 26 biimpa 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ a e. ( Base ` ( Scalar ` T ) ) ) -> a e. ( Base ` ( Scalar ` S ) ) )
28 27 adantrr 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ c e. U ) ) -> a e. ( Base ` ( Scalar ` S ) ) )
29 17 sselda 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ c e. U ) -> c e. ( Base ` S ) )
30 29 adantrl 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ c e. U ) ) -> c e. ( Base ` S ) )
31 eqid 
 |-  ( Base ` ( Scalar ` S ) ) = ( Base ` ( Scalar ` S ) )
32 eqid 
 |-  ( .s ` S ) = ( .s ` S )
33 eqid 
 |-  ( .s ` T ) = ( .s ` T )
34 21 31 10 32 33 lmhmlin 
 |-  ( ( F e. ( S LMHom T ) /\ a e. ( Base ` ( Scalar ` S ) ) /\ c e. ( Base ` S ) ) -> ( F ` ( a ( .s ` S ) c ) ) = ( a ( .s ` T ) ( F ` c ) ) )
35 20 28 30 34 syl3anc 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ c e. U ) ) -> ( F ` ( a ( .s ` S ) c ) ) = ( a ( .s ` T ) ( F ` c ) ) )
36 20 12 14 3syl 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ c e. U ) ) -> F Fn ( Base ` S ) )
37 simplr 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ c e. U ) ) -> U e. X )
38 37 16 syl 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ c e. U ) ) -> U C_ ( Base ` S ) )
39 4 adantr 
 |-  ( ( F e. ( S LMHom T ) /\ U e. X ) -> S e. LMod )
40 39 adantr 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ c e. U ) ) -> S e. LMod )
41 simprr 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ c e. U ) ) -> c e. U )
42 21 32 31 1 lssvscl 
 |-  ( ( ( S e. LMod /\ U e. X ) /\ ( a e. ( Base ` ( Scalar ` S ) ) /\ c e. U ) ) -> ( a ( .s ` S ) c ) e. U )
43 40 37 28 41 42 syl22anc 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ c e. U ) ) -> ( a ( .s ` S ) c ) e. U )
44 fnfvima 
 |-  ( ( F Fn ( Base ` S ) /\ U C_ ( Base ` S ) /\ ( a ( .s ` S ) c ) e. U ) -> ( F ` ( a ( .s ` S ) c ) ) e. ( F " U ) )
45 36 38 43 44 syl3anc 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ c e. U ) ) -> ( F ` ( a ( .s ` S ) c ) ) e. ( F " U ) )
46 35 45 eqeltrrd 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ c e. U ) ) -> ( a ( .s ` T ) ( F ` c ) ) e. ( F " U ) )
47 46 anassrs 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ a e. ( Base ` ( Scalar ` T ) ) ) /\ c e. U ) -> ( a ( .s ` T ) ( F ` c ) ) e. ( F " U ) )
48 oveq2 
 |-  ( ( F ` c ) = b -> ( a ( .s ` T ) ( F ` c ) ) = ( a ( .s ` T ) b ) )
49 48 eleq1d 
 |-  ( ( F ` c ) = b -> ( ( a ( .s ` T ) ( F ` c ) ) e. ( F " U ) <-> ( a ( .s ` T ) b ) e. ( F " U ) ) )
50 47 49 syl5ibcom 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ a e. ( Base ` ( Scalar ` T ) ) ) /\ c e. U ) -> ( ( F ` c ) = b -> ( a ( .s ` T ) b ) e. ( F " U ) ) )
51 50 rexlimdva 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ a e. ( Base ` ( Scalar ` T ) ) ) -> ( E. c e. U ( F ` c ) = b -> ( a ( .s ` T ) b ) e. ( F " U ) ) )
52 19 51 sylbid 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ a e. ( Base ` ( Scalar ` T ) ) ) -> ( b e. ( F " U ) -> ( a ( .s ` T ) b ) e. ( F " U ) ) )
53 52 impr 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. X ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. ( F " U ) ) ) -> ( a ( .s ` T ) b ) e. ( F " U ) )
54 53 ralrimivva 
 |-  ( ( F e. ( S LMHom T ) /\ U e. X ) -> A. a e. ( Base ` ( Scalar ` T ) ) A. b e. ( F " U ) ( a ( .s ` T ) b ) e. ( F " U ) )
55 lmhmlmod2 
 |-  ( F e. ( S LMHom T ) -> T e. LMod )
56 55 adantr 
 |-  ( ( F e. ( S LMHom T ) /\ U e. X ) -> T e. LMod )
57 eqid 
 |-  ( Base ` ( Scalar ` T ) ) = ( Base ` ( Scalar ` T ) )
58 22 57 11 33 2 islss4 
 |-  ( T e. LMod -> ( ( F " U ) e. Y <-> ( ( F " U ) e. ( SubGrp ` T ) /\ A. a e. ( Base ` ( Scalar ` T ) ) A. b e. ( F " U ) ( a ( .s ` T ) b ) e. ( F " U ) ) ) )
59 56 58 syl 
 |-  ( ( F e. ( S LMHom T ) /\ U e. X ) -> ( ( F " U ) e. Y <-> ( ( F " U ) e. ( SubGrp ` T ) /\ A. a e. ( Base ` ( Scalar ` T ) ) A. b e. ( F " U ) ( a ( .s ` T ) b ) e. ( F " U ) ) ) )
60 9 54 59 mpbir2and 
 |-  ( ( F e. ( S LMHom T ) /\ U e. X ) -> ( F " U ) e. Y )