Metamath Proof Explorer

Theorem lmhmlnmsplit

Description: If the kernel and range of a homomorphism of left modules are Noetherian, then so is the domain. (Contributed by Stefan O'Rear, 1-Jan-2015) (Revised by Stefan O'Rear, 12-Jun-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 lmhmlnmsplit 
|- ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) -> S e. LNoeM )

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 lmhmlmod1 
 |-  ( F e. ( S LMHom T ) -> S e. LMod )
6 5 3ad2ant1 
 |-  ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) -> S e. LMod )
7 eqid 
 |-  ( LSubSp ` S ) = ( LSubSp ` S )
8 eqid 
 |-  ( S |`s a ) = ( S |`s a )
9 7 8 reslmhm 
 |-  ( ( F e. ( S LMHom T ) /\ a e. ( LSubSp ` S ) ) -> ( F |` a ) e. ( ( S |`s a ) LMHom T ) )
10 9 3ad2antl1 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ( F |` a ) e. ( ( S |`s a ) LMHom T ) )
11 cnvresima 
 |-  ( `' ( F |` a ) " { .0. } ) = ( ( `' F " { .0. } ) i^i a )
12 2 eqcomi 
 |-  ( `' F " { .0. } ) = K
13 12 ineq1i 
 |-  ( ( `' F " { .0. } ) i^i a ) = ( K i^i a )
14 incom 
 |-  ( K i^i a ) = ( a i^i K )
15 11 13 14 3eqtri 
 |-  ( `' ( F |` a ) " { .0. } ) = ( a i^i K )
16 15 oveq2i 
 |-  ( ( S |`s a ) |`s ( `' ( F |` a ) " { .0. } ) ) = ( ( S |`s a ) |`s ( a i^i K ) )
17 vex 
 |-  a e. _V
18 inss1 
 |-  ( a i^i K ) C_ a
19 ressabs 
 |-  ( ( a e. _V /\ ( a i^i K ) C_ a ) -> ( ( S |`s a ) |`s ( a i^i K ) ) = ( S |`s ( a i^i K ) ) )
20 17 18 19 mp2an 
 |-  ( ( S |`s a ) |`s ( a i^i K ) ) = ( S |`s ( a i^i K ) )
21 3 oveq1i 
 |-  ( U |`s ( a i^i K ) ) = ( ( S |`s K ) |`s ( a i^i K ) )
22 simpl1 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> F e. ( S LMHom T ) )
23 cnvexg 
 |-  ( F e. ( S LMHom T ) -> `' F e. _V )
24 imaexg 
 |-  ( `' F e. _V -> ( `' F " { .0. } ) e. _V )
25 23 24 syl 
 |-  ( F e. ( S LMHom T ) -> ( `' F " { .0. } ) e. _V )
26 2 25 eqeltrid 
 |-  ( F e. ( S LMHom T ) -> K e. _V )
27 22 26 syl 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> K e. _V )
28 inss2 
 |-  ( a i^i K ) C_ K
29 ressabs 
 |-  ( ( K e. _V /\ ( a i^i K ) C_ K ) -> ( ( S |`s K ) |`s ( a i^i K ) ) = ( S |`s ( a i^i K ) ) )
30 27 28 29 sylancl 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ( ( S |`s K ) |`s ( a i^i K ) ) = ( S |`s ( a i^i K ) ) )
31 21 30 syl5eq 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ( U |`s ( a i^i K ) ) = ( S |`s ( a i^i K ) ) )
32 20 31 eqtr4id 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ( ( S |`s a ) |`s ( a i^i K ) ) = ( U |`s ( a i^i K ) ) )
33 16 32 syl5eq 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ( ( S |`s a ) |`s ( `' ( F |` a ) " { .0. } ) ) = ( U |`s ( a i^i K ) ) )
34 simpl2 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> U e. LNoeM )
35 6 adantr 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> S e. LMod )
36 simpr 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> a e. ( LSubSp ` S ) )
37 2 1 7 lmhmkerlss 
 |-  ( F e. ( S LMHom T ) -> K e. ( LSubSp ` S ) )
38 22 37 syl 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> K e. ( LSubSp ` S ) )
39 7 lssincl 
 |-  ( ( S e. LMod /\ a e. ( LSubSp ` S ) /\ K e. ( LSubSp ` S ) ) -> ( a i^i K ) e. ( LSubSp ` S ) )
40 35 36 38 39 syl3anc 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ( a i^i K ) e. ( LSubSp ` S ) )
41 28 a1i 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ( a i^i K ) C_ K )
42 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
43 3 7 42 lsslss 
 |-  ( ( S e. LMod /\ K e. ( LSubSp ` S ) ) -> ( ( a i^i K ) e. ( LSubSp ` U ) <-> ( ( a i^i K ) e. ( LSubSp ` S ) /\ ( a i^i K ) C_ K ) ) )
44 35 38 43 syl2anc 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ( ( a i^i K ) e. ( LSubSp ` U ) <-> ( ( a i^i K ) e. ( LSubSp ` S ) /\ ( a i^i K ) C_ K ) ) )
45 40 41 44 mpbir2and 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ( a i^i K ) e. ( LSubSp ` U ) )
46 eqid 
 |-  ( U |`s ( a i^i K ) ) = ( U |`s ( a i^i K ) )
47 42 46 lnmlssfg 
 |-  ( ( U e. LNoeM /\ ( a i^i K ) e. ( LSubSp ` U ) ) -> ( U |`s ( a i^i K ) ) e. LFinGen )
48 34 45 47 syl2anc 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ( U |`s ( a i^i K ) ) e. LFinGen )
49 33 48 eqeltrd 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ( ( S |`s a ) |`s ( `' ( F |` a ) " { .0. } ) ) e. LFinGen )
50 incom 
 |-  ( ran F i^i ran ( F |` a ) ) = ( ran ( F |` a ) i^i ran F )
51 resss 
 |-  ( F |` a ) C_ F
52 rnss 
 |-  ( ( F |` a ) C_ F -> ran ( F |` a ) C_ ran F )
53 51 52 ax-mp 
 |-  ran ( F |` a ) C_ ran F
54 df-ss 
 |-  ( ran ( F |` a ) C_ ran F <-> ( ran ( F |` a ) i^i ran F ) = ran ( F |` a ) )
55 53 54 mpbi 
 |-  ( ran ( F |` a ) i^i ran F ) = ran ( F |` a )
56 50 55 eqtr2i 
 |-  ran ( F |` a ) = ( ran F i^i ran ( F |` a ) )
57 56 oveq2i 
 |-  ( T |`s ran ( F |` a ) ) = ( T |`s ( ran F i^i ran ( F |` a ) ) )
58 4 oveq1i 
 |-  ( V |`s ran ( F |` a ) ) = ( ( T |`s ran F ) |`s ran ( F |` a ) )
59 rnexg 
 |-  ( F e. ( S LMHom T ) -> ran F e. _V )
60 resexg 
 |-  ( F e. ( S LMHom T ) -> ( F |` a ) e. _V )
61 rnexg 
 |-  ( ( F |` a ) e. _V -> ran ( F |` a ) e. _V )
62 60 61 syl 
 |-  ( F e. ( S LMHom T ) -> ran ( F |` a ) e. _V )
63 ressress 
 |-  ( ( ran F e. _V /\ ran ( F |` a ) e. _V ) -> ( ( T |`s ran F ) |`s ran ( F |` a ) ) = ( T |`s ( ran F i^i ran ( F |` a ) ) ) )
64 59 62 63 syl2anc 
 |-  ( F e. ( S LMHom T ) -> ( ( T |`s ran F ) |`s ran ( F |` a ) ) = ( T |`s ( ran F i^i ran ( F |` a ) ) ) )
65 58 64 syl5eq 
 |-  ( F e. ( S LMHom T ) -> ( V |`s ran ( F |` a ) ) = ( T |`s ( ran F i^i ran ( F |` a ) ) ) )
66 57 65 eqtr4id 
 |-  ( F e. ( S LMHom T ) -> ( T |`s ran ( F |` a ) ) = ( V |`s ran ( F |` a ) ) )
67 22 66 syl 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ( T |`s ran ( F |` a ) ) = ( V |`s ran ( F |` a ) ) )
68 simpl3 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> V e. LNoeM )
69 lmhmrnlss 
 |-  ( ( F |` a ) e. ( ( S |`s a ) LMHom T ) -> ran ( F |` a ) e. ( LSubSp ` T ) )
70 10 69 syl 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ran ( F |` a ) e. ( LSubSp ` T ) )
71 53 a1i 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ran ( F |` a ) C_ ran F )
72 lmhmlmod2 
 |-  ( F e. ( S LMHom T ) -> T e. LMod )
73 22 72 syl 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> T e. LMod )
74 lmhmrnlss 
 |-  ( F e. ( S LMHom T ) -> ran F e. ( LSubSp ` T ) )
75 22 74 syl 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ran F e. ( LSubSp ` T ) )
76 eqid 
 |-  ( LSubSp ` T ) = ( LSubSp ` T )
77 eqid 
 |-  ( LSubSp ` V ) = ( LSubSp ` V )
78 4 76 77 lsslss 
 |-  ( ( T e. LMod /\ ran F e. ( LSubSp ` T ) ) -> ( ran ( F |` a ) e. ( LSubSp ` V ) <-> ( ran ( F |` a ) e. ( LSubSp ` T ) /\ ran ( F |` a ) C_ ran F ) ) )
79 73 75 78 syl2anc 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ( ran ( F |` a ) e. ( LSubSp ` V ) <-> ( ran ( F |` a ) e. ( LSubSp ` T ) /\ ran ( F |` a ) C_ ran F ) ) )
80 70 71 79 mpbir2and 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ran ( F |` a ) e. ( LSubSp ` V ) )
81 eqid 
 |-  ( V |`s ran ( F |` a ) ) = ( V |`s ran ( F |` a ) )
82 77 81 lnmlssfg 
 |-  ( ( V e. LNoeM /\ ran ( F |` a ) e. ( LSubSp ` V ) ) -> ( V |`s ran ( F |` a ) ) e. LFinGen )
83 68 80 82 syl2anc 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ( V |`s ran ( F |` a ) ) e. LFinGen )
84 67 83 eqeltrd 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ( T |`s ran ( F |` a ) ) e. LFinGen )
85 eqid 
 |-  ( `' ( F |` a ) " { .0. } ) = ( `' ( F |` a ) " { .0. } )
86 eqid 
 |-  ( ( S |`s a ) |`s ( `' ( F |` a ) " { .0. } ) ) = ( ( S |`s a ) |`s ( `' ( F |` a ) " { .0. } ) )
87 eqid 
 |-  ( T |`s ran ( F |` a ) ) = ( T |`s ran ( F |` a ) )
88 1 85 86 87 lmhmfgsplit 
 |-  ( ( ( F |` a ) e. ( ( S |`s a ) LMHom T ) /\ ( ( S |`s a ) |`s ( `' ( F |` a ) " { .0. } ) ) e. LFinGen /\ ( T |`s ran ( F |` a ) ) e. LFinGen ) -> ( S |`s a ) e. LFinGen )
89 10 49 84 88 syl3anc 
 |-  ( ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) /\ a e. ( LSubSp ` S ) ) -> ( S |`s a ) e. LFinGen )
90 89 ralrimiva 
 |-  ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) -> A. a e. ( LSubSp ` S ) ( S |`s a ) e. LFinGen )
91 7 islnm 
 |-  ( S e. LNoeM <-> ( S e. LMod /\ A. a e. ( LSubSp ` S ) ( S |`s a ) e. LFinGen ) )
92 6 90 91 sylanbrc 
 |-  ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) -> S e. LNoeM )