Metamath Proof Explorer

Theorem lmhmfgima

Description: A homomorphism maps finitely generated submodules to finitely generated submodules. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypotheses lmhmfgima.y 
|- Y = ( T |`s ( F " A ) )
lmhmfgima.x 
|- X = ( S |`s A )
lmhmfgima.u 
|- U = ( LSubSp ` S )
lmhmfgima.xf 
|- ( ph -> X e. LFinGen )
lmhmfgima.a 
|- ( ph -> A e. U )
lmhmfgima.f 
|- ( ph -> F e. ( S LMHom T ) )
Assertion lmhmfgima 
|- ( ph -> Y e. LFinGen )

Proof

Step Hyp Ref Expression
1 lmhmfgima.y 
 |-  Y = ( T |`s ( F " A ) )
2 lmhmfgima.x 
 |-  X = ( S |`s A )
3 lmhmfgima.u 
 |-  U = ( LSubSp ` S )
4 lmhmfgima.xf 
 |-  ( ph -> X e. LFinGen )
5 lmhmfgima.a 
 |-  ( ph -> A e. U )
6 lmhmfgima.f 
 |-  ( ph -> F e. ( S LMHom T ) )
7 lmhmlmod1 
 |-  ( F e. ( S LMHom T ) -> S e. LMod )
8 6 7 syl 
 |-  ( ph -> S e. LMod )
9 eqid 
 |-  ( LSpan ` S ) = ( LSpan ` S )
10 eqid 
 |-  ( Base ` S ) = ( Base ` S )
11 2 3 9 10 islssfg2 
 |-  ( ( S e. LMod /\ A e. U ) -> ( X e. LFinGen <-> E. x e. ( ~P ( Base ` S ) i^i Fin ) ( ( LSpan ` S ) ` x ) = A ) )
12 8 5 11 syl2anc 
 |-  ( ph -> ( X e. LFinGen <-> E. x e. ( ~P ( Base ` S ) i^i Fin ) ( ( LSpan ` S ) ` x ) = A ) )
13 4 12 mpbid 
 |-  ( ph -> E. x e. ( ~P ( Base ` S ) i^i Fin ) ( ( LSpan ` S ) ` x ) = A )
14 inss1 
 |-  ( ~P ( Base ` S ) i^i Fin ) C_ ~P ( Base ` S )
15 14 sseli 
 |-  ( x e. ( ~P ( Base ` S ) i^i Fin ) -> x e. ~P ( Base ` S ) )
16 15 elpwid 
 |-  ( x e. ( ~P ( Base ` S ) i^i Fin ) -> x C_ ( Base ` S ) )
17 eqid 
 |-  ( LSpan ` T ) = ( LSpan ` T )
18 10 9 17 lmhmlsp 
 |-  ( ( F e. ( S LMHom T ) /\ x C_ ( Base ` S ) ) -> ( F " ( ( LSpan ` S ) ` x ) ) = ( ( LSpan ` T ) ` ( F " x ) ) )
19 6 16 18 syl2an 
 |-  ( ( ph /\ x e. ( ~P ( Base ` S ) i^i Fin ) ) -> ( F " ( ( LSpan ` S ) ` x ) ) = ( ( LSpan ` T ) ` ( F " x ) ) )
20 19 oveq2d 
 |-  ( ( ph /\ x e. ( ~P ( Base ` S ) i^i Fin ) ) -> ( T |`s ( F " ( ( LSpan ` S ) ` x ) ) ) = ( T |`s ( ( LSpan ` T ) ` ( F " x ) ) ) )
21 lmhmlmod2 
 |-  ( F e. ( S LMHom T ) -> T e. LMod )
22 6 21 syl 
 |-  ( ph -> T e. LMod )
23 22 adantr 
 |-  ( ( ph /\ x e. ( ~P ( Base ` S ) i^i Fin ) ) -> T e. LMod )
24 imassrn 
 |-  ( F " x ) C_ ran F
25 eqid 
 |-  ( Base ` T ) = ( Base ` T )
26 10 25 lmhmf 
 |-  ( F e. ( S LMHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
27 6 26 syl 
 |-  ( ph -> F : ( Base ` S ) --> ( Base ` T ) )
28 27 frnd 
 |-  ( ph -> ran F C_ ( Base ` T ) )
29 24 28 sstrid 
 |-  ( ph -> ( F " x ) C_ ( Base ` T ) )
30 29 adantr 
 |-  ( ( ph /\ x e. ( ~P ( Base ` S ) i^i Fin ) ) -> ( F " x ) C_ ( Base ` T ) )
31 inss2 
 |-  ( ~P ( Base ` S ) i^i Fin ) C_ Fin
32 31 sseli 
 |-  ( x e. ( ~P ( Base ` S ) i^i Fin ) -> x e. Fin )
33 32 adantl 
 |-  ( ( ph /\ x e. ( ~P ( Base ` S ) i^i Fin ) ) -> x e. Fin )
34 27 ffund 
 |-  ( ph -> Fun F )
35 34 adantr 
 |-  ( ( ph /\ x e. ( ~P ( Base ` S ) i^i Fin ) ) -> Fun F )
36 16 adantl 
 |-  ( ( ph /\ x e. ( ~P ( Base ` S ) i^i Fin ) ) -> x C_ ( Base ` S ) )
37 27 fdmd 
 |-  ( ph -> dom F = ( Base ` S ) )
38 37 adantr 
 |-  ( ( ph /\ x e. ( ~P ( Base ` S ) i^i Fin ) ) -> dom F = ( Base ` S ) )
39 36 38 sseqtrrd 
 |-  ( ( ph /\ x e. ( ~P ( Base ` S ) i^i Fin ) ) -> x C_ dom F )
40 fores 
 |-  ( ( Fun F /\ x C_ dom F ) -> ( F |` x ) : x -onto-> ( F " x ) )
41 35 39 40 syl2anc 
 |-  ( ( ph /\ x e. ( ~P ( Base ` S ) i^i Fin ) ) -> ( F |` x ) : x -onto-> ( F " x ) )
42 fofi 
 |-  ( ( x e. Fin /\ ( F |` x ) : x -onto-> ( F " x ) ) -> ( F " x ) e. Fin )
43 33 41 42 syl2anc 
 |-  ( ( ph /\ x e. ( ~P ( Base ` S ) i^i Fin ) ) -> ( F " x ) e. Fin )
44 eqid 
 |-  ( T |`s ( ( LSpan ` T ) ` ( F " x ) ) ) = ( T |`s ( ( LSpan ` T ) ` ( F " x ) ) )
45 17 25 44 islssfgi 
 |-  ( ( T e. LMod /\ ( F " x ) C_ ( Base ` T ) /\ ( F " x ) e. Fin ) -> ( T |`s ( ( LSpan ` T ) ` ( F " x ) ) ) e. LFinGen )
46 23 30 43 45 syl3anc 
 |-  ( ( ph /\ x e. ( ~P ( Base ` S ) i^i Fin ) ) -> ( T |`s ( ( LSpan ` T ) ` ( F " x ) ) ) e. LFinGen )
47 20 46 eqeltrd 
 |-  ( ( ph /\ x e. ( ~P ( Base ` S ) i^i Fin ) ) -> ( T |`s ( F " ( ( LSpan ` S ) ` x ) ) ) e. LFinGen )
48 imaeq2 
 |-  ( ( ( LSpan ` S ) ` x ) = A -> ( F " ( ( LSpan ` S ) ` x ) ) = ( F " A ) )
49 48 oveq2d 
 |-  ( ( ( LSpan ` S ) ` x ) = A -> ( T |`s ( F " ( ( LSpan ` S ) ` x ) ) ) = ( T |`s ( F " A ) ) )
50 49 eleq1d 
 |-  ( ( ( LSpan ` S ) ` x ) = A -> ( ( T |`s ( F " ( ( LSpan ` S ) ` x ) ) ) e. LFinGen <-> ( T |`s ( F " A ) ) e. LFinGen ) )
51 47 50 syl5ibcom 
 |-  ( ( ph /\ x e. ( ~P ( Base ` S ) i^i Fin ) ) -> ( ( ( LSpan ` S ) ` x ) = A -> ( T |`s ( F " A ) ) e. LFinGen ) )
52 51 rexlimdva 
 |-  ( ph -> ( E. x e. ( ~P ( Base ` S ) i^i Fin ) ( ( LSpan ` S ) ` x ) = A -> ( T |`s ( F " A ) ) e. LFinGen ) )
53 13 52 mpd 
 |-  ( ph -> ( T |`s ( F " A ) ) e. LFinGen )
54 1 53 eqeltrid 
 |-  ( ph -> Y e. LFinGen )