Metamath Proof Explorer

Theorem lmhmfgsplit

Description: If the kernel and range of a homomorphism of left modules are finitely generated, then so is the domain. (Contributed by Stefan O'Rear, 1-Jan-2015) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypotheses lmhmfgsplit.z 
|- .0. = ( 0g ` T )
lmhmfgsplit.k 
|- K = ( `' F " { .0. } )
lmhmfgsplit.u 
|- U = ( S |`s K )
lmhmfgsplit.v 
|- V = ( T |`s ran F )
Assertion lmhmfgsplit 
|- ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) -> S e. LFinGen )

Proof

Step Hyp Ref Expression
1 lmhmfgsplit.z 
 |-  .0. = ( 0g ` T )
2 lmhmfgsplit.k 
 |-  K = ( `' F " { .0. } )
3 lmhmfgsplit.u 
 |-  U = ( S |`s K )
4 lmhmfgsplit.v 
 |-  V = ( T |`s ran F )
5 simp3 
 |-  ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) -> V e. LFinGen )
6 lmhmlmod2 
 |-  ( F e. ( S LMHom T ) -> T e. LMod )
7 6 3ad2ant1 
 |-  ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) -> T e. LMod )
8 lmhmrnlss 
 |-  ( F e. ( S LMHom T ) -> ran F e. ( LSubSp ` T ) )
9 8 3ad2ant1 
 |-  ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) -> ran F e. ( LSubSp ` T ) )
10 eqid 
 |-  ( LSubSp ` T ) = ( LSubSp ` T )
11 eqid 
 |-  ( LSpan ` T ) = ( LSpan ` T )
12 4 10 11 islssfg 
 |-  ( ( T e. LMod /\ ran F e. ( LSubSp ` T ) ) -> ( V e. LFinGen <-> E. a e. ~P ran F ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) )
13 7 9 12 syl2anc 
 |-  ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) -> ( V e. LFinGen <-> E. a e. ~P ran F ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) )
14 5 13 mpbid 
 |-  ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) -> E. a e. ~P ran F ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) )
15 simpl1 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) -> F e. ( S LMHom T ) )
16 eqid 
 |-  ( Base ` S ) = ( Base ` S )
17 eqid 
 |-  ( Base ` T ) = ( Base ` T )
18 16 17 lmhmf 
 |-  ( F e. ( S LMHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
19 ffn 
 |-  ( F : ( Base ` S ) --> ( Base ` T ) -> F Fn ( Base ` S ) )
20 15 18 19 3syl 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) -> F Fn ( Base ` S ) )
21 elpwi 
 |-  ( a e. ~P ran F -> a C_ ran F )
22 21 ad2antrl 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) -> a C_ ran F )
23 simprrl 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) -> a e. Fin )
24 fipreima 
 |-  ( ( F Fn ( Base ` S ) /\ a C_ ran F /\ a e. Fin ) -> E. b e. ( ~P ( Base ` S ) i^i Fin ) ( F " b ) = a )
25 20 22 23 24 syl3anc 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) -> E. b e. ( ~P ( Base ` S ) i^i Fin ) ( F " b ) = a )
26 eqid 
 |-  ( LSubSp ` S ) = ( LSubSp ` S )
27 eqid 
 |-  ( LSSum ` S ) = ( LSSum ` S )
28 simpll1 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> F e. ( S LMHom T ) )
29 lmhmlmod1 
 |-  ( F e. ( S LMHom T ) -> S e. LMod )
30 29 3ad2ant1 
 |-  ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) -> S e. LMod )
31 30 ad2antrr 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> S e. LMod )
32 inss1 
 |-  ( ~P ( Base ` S ) i^i Fin ) C_ ~P ( Base ` S )
33 32 sseli 
 |-  ( b e. ( ~P ( Base ` S ) i^i Fin ) -> b e. ~P ( Base ` S ) )
34 elpwi 
 |-  ( b e. ~P ( Base ` S ) -> b C_ ( Base ` S ) )
35 33 34 syl 
 |-  ( b e. ( ~P ( Base ` S ) i^i Fin ) -> b C_ ( Base ` S ) )
36 35 ad2antrl 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> b C_ ( Base ` S ) )
37 eqid 
 |-  ( LSpan ` S ) = ( LSpan ` S )
38 16 26 37 lspcl 
 |-  ( ( S e. LMod /\ b C_ ( Base ` S ) ) -> ( ( LSpan ` S ) ` b ) e. ( LSubSp ` S ) )
39 31 36 38 syl2anc 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> ( ( LSpan ` S ) ` b ) e. ( LSubSp ` S ) )
40 16 37 11 lmhmlsp 
 |-  ( ( F e. ( S LMHom T ) /\ b C_ ( Base ` S ) ) -> ( F " ( ( LSpan ` S ) ` b ) ) = ( ( LSpan ` T ) ` ( F " b ) ) )
41 28 36 40 syl2anc 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> ( F " ( ( LSpan ` S ) ` b ) ) = ( ( LSpan ` T ) ` ( F " b ) ) )
42 fveq2 
 |-  ( ( F " b ) = a -> ( ( LSpan ` T ) ` ( F " b ) ) = ( ( LSpan ` T ) ` a ) )
43 42 ad2antll 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> ( ( LSpan ` T ) ` ( F " b ) ) = ( ( LSpan ` T ) ` a ) )
44 simp2rr 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> ( ( LSpan ` T ) ` a ) = ran F )
45 44 3expa 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> ( ( LSpan ` T ) ` a ) = ran F )
46 41 43 45 3eqtrd 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> ( F " ( ( LSpan ` S ) ` b ) ) = ran F )
47 26 27 1 2 16 28 39 46 kercvrlsm 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> ( K ( LSSum ` S ) ( ( LSpan ` S ) ` b ) ) = ( Base ` S ) )
48 47 oveq2d 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> ( S |`s ( K ( LSSum ` S ) ( ( LSpan ` S ) ` b ) ) ) = ( S |`s ( Base ` S ) ) )
49 16 ressid 
 |-  ( S e. LMod -> ( S |`s ( Base ` S ) ) = S )
50 30 49 syl 
 |-  ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) -> ( S |`s ( Base ` S ) ) = S )
51 50 ad2antrr 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> ( S |`s ( Base ` S ) ) = S )
52 48 51 eqtr2d 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> S = ( S |`s ( K ( LSSum ` S ) ( ( LSpan ` S ) ` b ) ) ) )
53 eqid 
 |-  ( S |`s ( ( LSpan ` S ) ` b ) ) = ( S |`s ( ( LSpan ` S ) ` b ) )
54 eqid 
 |-  ( S |`s ( K ( LSSum ` S ) ( ( LSpan ` S ) ` b ) ) ) = ( S |`s ( K ( LSSum ` S ) ( ( LSpan ` S ) ` b ) ) )
55 2 1 26 lmhmkerlss 
 |-  ( F e. ( S LMHom T ) -> K e. ( LSubSp ` S ) )
56 55 3ad2ant1 
 |-  ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) -> K e. ( LSubSp ` S ) )
57 56 ad2antrr 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> K e. ( LSubSp ` S ) )
58 simpll2 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> U e. LFinGen )
59 inss2 
 |-  ( ~P ( Base ` S ) i^i Fin ) C_ Fin
60 59 sseli 
 |-  ( b e. ( ~P ( Base ` S ) i^i Fin ) -> b e. Fin )
61 60 ad2antrl 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> b e. Fin )
62 37 16 53 islssfgi 
 |-  ( ( S e. LMod /\ b C_ ( Base ` S ) /\ b e. Fin ) -> ( S |`s ( ( LSpan ` S ) ` b ) ) e. LFinGen )
63 31 36 61 62 syl3anc 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> ( S |`s ( ( LSpan ` S ) ` b ) ) e. LFinGen )
64 26 27 3 53 54 31 57 39 58 63 lsmfgcl 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> ( S |`s ( K ( LSSum ` S ) ( ( LSpan ` S ) ` b ) ) ) e. LFinGen )
65 52 64 eqeltrd 
 |-  ( ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) /\ ( b e. ( ~P ( Base ` S ) i^i Fin ) /\ ( F " b ) = a ) ) -> S e. LFinGen )
66 25 65 rexlimddv 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) /\ ( a e. ~P ran F /\ ( a e. Fin /\ ( ( LSpan ` T ) ` a ) = ran F ) ) ) -> S e. LFinGen )
67 14 66 rexlimddv 
 |-  ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) -> S e. LFinGen )