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 ‘ 𝑇 )
lmhmfgsplit.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
lmhmfgsplit.u ⊢ 𝑈 = ( 𝑆 ↾s 𝐾 )
lmhmfgsplit.v ⊢ 𝑉 = ( 𝑇 ↾s ran 𝐹 )
Assertion lmhmlnmsplit ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) → 𝑆 ∈ LNoeM )

Proof

Step Hyp Ref Expression
1 lmhmfgsplit.z ⊢ 0 = ( 0g ‘ 𝑇 )
2 lmhmfgsplit.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
3 lmhmfgsplit.u ⊢ 𝑈 = ( 𝑆 ↾s 𝐾 )
4 lmhmfgsplit.v ⊢ 𝑉 = ( 𝑇 ↾s ran 𝐹 )
5 lmhmlmod1 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
6 5 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) → 𝑆 ∈ LMod )
7 eqid ⊢ ( LSubSp ‘ 𝑆 ) = ( LSubSp ‘ 𝑆 )
8 eqid ⊢ ( 𝑆 ↾s 𝑎 ) = ( 𝑆 ↾s 𝑎 )
9 7 8 reslmhm ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑎 ) ∈ ( ( 𝑆 ↾s 𝑎 ) LMHom 𝑇 ) )
10 9 3ad2antl1 ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑎 ) ∈ ( ( 𝑆 ↾s 𝑎 ) LMHom 𝑇 ) )
11 cnvresima ⊢ ( ◡ ( 𝐹 ↾ 𝑎 ) “ { 0 } ) = ( ( ◡ 𝐹 “ { 0 } ) ∩ 𝑎 )
12 2 eqcomi ⊢ ( ◡ 𝐹 “ { 0 } ) = 𝐾
13 12 ineq1i ⊢ ( ( ◡ 𝐹 “ { 0 } ) ∩ 𝑎 ) = ( 𝐾 ∩ 𝑎 )
14 incom ⊢ ( 𝐾 ∩ 𝑎 ) = ( 𝑎 ∩ 𝐾 )
15 11 13 14 3eqtri ⊢ ( ◡ ( 𝐹 ↾ 𝑎 ) “ { 0 } ) = ( 𝑎 ∩ 𝐾 )
16 15 oveq2i ⊢ ( ( 𝑆 ↾s 𝑎 ) ↾s ( ◡ ( 𝐹 ↾ 𝑎 ) “ { 0 } ) ) = ( ( 𝑆 ↾s 𝑎 ) ↾s ( 𝑎 ∩ 𝐾 ) )
17 vex ⊢ 𝑎 ∈ V
18 inss1 ⊢ ( 𝑎 ∩ 𝐾 ) ⊆ 𝑎
19 ressabs ⊢ ( ( 𝑎 ∈ V ∧ ( 𝑎 ∩ 𝐾 ) ⊆ 𝑎 ) → ( ( 𝑆 ↾s 𝑎 ) ↾s ( 𝑎 ∩ 𝐾 ) ) = ( 𝑆 ↾s ( 𝑎 ∩ 𝐾 ) ) )
20 17 18 19 mp2an ⊢ ( ( 𝑆 ↾s 𝑎 ) ↾s ( 𝑎 ∩ 𝐾 ) ) = ( 𝑆 ↾s ( 𝑎 ∩ 𝐾 ) )
21 3 oveq1i ⊢ ( 𝑈 ↾s ( 𝑎 ∩ 𝐾 ) ) = ( ( 𝑆 ↾s 𝐾 ) ↾s ( 𝑎 ∩ 𝐾 ) )
22 simpl1 ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
23 cnvexg ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ◡ 𝐹 ∈ V )
24 imaexg ⊢ ( ◡ 𝐹 ∈ V → ( ◡ 𝐹 “ { 0 } ) ∈ V )
25 23 24 syl ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( ◡ 𝐹 “ { 0 } ) ∈ V )
26 2 25 eqeltrid ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐾 ∈ V )
27 22 26 syl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → 𝐾 ∈ V )
28 inss2 ⊢ ( 𝑎 ∩ 𝐾 ) ⊆ 𝐾
29 ressabs ⊢ ( ( 𝐾 ∈ V ∧ ( 𝑎 ∩ 𝐾 ) ⊆ 𝐾 ) → ( ( 𝑆 ↾s 𝐾 ) ↾s ( 𝑎 ∩ 𝐾 ) ) = ( 𝑆 ↾s ( 𝑎 ∩ 𝐾 ) ) )
30 27 28 29 sylancl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ( ( 𝑆 ↾s 𝐾 ) ↾s ( 𝑎 ∩ 𝐾 ) ) = ( 𝑆 ↾s ( 𝑎 ∩ 𝐾 ) ) )
31 21 30 syl5eq ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ( 𝑈 ↾s ( 𝑎 ∩ 𝐾 ) ) = ( 𝑆 ↾s ( 𝑎 ∩ 𝐾 ) ) )
32 20 31 eqtr4id ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ( ( 𝑆 ↾s 𝑎 ) ↾s ( 𝑎 ∩ 𝐾 ) ) = ( 𝑈 ↾s ( 𝑎 ∩ 𝐾 ) ) )
33 16 32 syl5eq ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ( ( 𝑆 ↾s 𝑎 ) ↾s ( ◡ ( 𝐹 ↾ 𝑎 ) “ { 0 } ) ) = ( 𝑈 ↾s ( 𝑎 ∩ 𝐾 ) ) )
34 simpl2 ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → 𝑈 ∈ LNoeM )
35 6 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → 𝑆 ∈ LMod )
36 simpr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → 𝑎 ∈ ( LSubSp ‘ 𝑆 ) )
37 2 1 7 lmhmkerlss ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐾 ∈ ( LSubSp ‘ 𝑆 ) )
38 22 37 syl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → 𝐾 ∈ ( LSubSp ‘ 𝑆 ) )
39 7 lssincl ⊢ ( ( 𝑆 ∈ LMod ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ∧ 𝐾 ∈ ( LSubSp ‘ 𝑆 ) ) → ( 𝑎 ∩ 𝐾 ) ∈ ( LSubSp ‘ 𝑆 ) )
40 35 36 38 39 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ( 𝑎 ∩ 𝐾 ) ∈ ( LSubSp ‘ 𝑆 ) )
41 28 a1i ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ( 𝑎 ∩ 𝐾 ) ⊆ 𝐾 )
42 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
43 3 7 42 lsslss ⊢ ( ( 𝑆 ∈ LMod ∧ 𝐾 ∈ ( LSubSp ‘ 𝑆 ) ) → ( ( 𝑎 ∩ 𝐾 ) ∈ ( LSubSp ‘ 𝑈 ) ↔ ( ( 𝑎 ∩ 𝐾 ) ∈ ( LSubSp ‘ 𝑆 ) ∧ ( 𝑎 ∩ 𝐾 ) ⊆ 𝐾 ) ) )
44 35 38 43 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ( ( 𝑎 ∩ 𝐾 ) ∈ ( LSubSp ‘ 𝑈 ) ↔ ( ( 𝑎 ∩ 𝐾 ) ∈ ( LSubSp ‘ 𝑆 ) ∧ ( 𝑎 ∩ 𝐾 ) ⊆ 𝐾 ) ) )
45 40 41 44 mpbir2and ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ( 𝑎 ∩ 𝐾 ) ∈ ( LSubSp ‘ 𝑈 ) )
46 eqid ⊢ ( 𝑈 ↾s ( 𝑎 ∩ 𝐾 ) ) = ( 𝑈 ↾s ( 𝑎 ∩ 𝐾 ) )
47 42 46 lnmlssfg ⊢ ( ( 𝑈 ∈ LNoeM ∧ ( 𝑎 ∩ 𝐾 ) ∈ ( LSubSp ‘ 𝑈 ) ) → ( 𝑈 ↾s ( 𝑎 ∩ 𝐾 ) ) ∈ LFinGen )
48 34 45 47 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ( 𝑈 ↾s ( 𝑎 ∩ 𝐾 ) ) ∈ LFinGen )
49 33 48 eqeltrd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ( ( 𝑆 ↾s 𝑎 ) ↾s ( ◡ ( 𝐹 ↾ 𝑎 ) “ { 0 } ) ) ∈ LFinGen )
50 incom ⊢ ( ran 𝐹 ∩ ran ( 𝐹 ↾ 𝑎 ) ) = ( ran ( 𝐹 ↾ 𝑎 ) ∩ ran 𝐹 )
51 resss ⊢ ( 𝐹 ↾ 𝑎 ) ⊆ 𝐹
52 rnss ⊢ ( ( 𝐹 ↾ 𝑎 ) ⊆ 𝐹 → ran ( 𝐹 ↾ 𝑎 ) ⊆ ran 𝐹 )
53 51 52 ax-mp ⊢ ran ( 𝐹 ↾ 𝑎 ) ⊆ ran 𝐹
54 df-ss ⊢ ( ran ( 𝐹 ↾ 𝑎 ) ⊆ ran 𝐹 ↔ ( ran ( 𝐹 ↾ 𝑎 ) ∩ ran 𝐹 ) = ran ( 𝐹 ↾ 𝑎 ) )
55 53 54 mpbi ⊢ ( ran ( 𝐹 ↾ 𝑎 ) ∩ ran 𝐹 ) = ran ( 𝐹 ↾ 𝑎 )
56 50 55 eqtr2i ⊢ ran ( 𝐹 ↾ 𝑎 ) = ( ran 𝐹 ∩ ran ( 𝐹 ↾ 𝑎 ) )
57 56 oveq2i ⊢ ( 𝑇 ↾s ran ( 𝐹 ↾ 𝑎 ) ) = ( 𝑇 ↾s ( ran 𝐹 ∩ ran ( 𝐹 ↾ 𝑎 ) ) )
58 4 oveq1i ⊢ ( 𝑉 ↾s ran ( 𝐹 ↾ 𝑎 ) ) = ( ( 𝑇 ↾s ran 𝐹 ) ↾s ran ( 𝐹 ↾ 𝑎 ) )
59 rnexg ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ran 𝐹 ∈ V )
60 resexg ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝐹 ↾ 𝑎 ) ∈ V )
61 rnexg ⊢ ( ( 𝐹 ↾ 𝑎 ) ∈ V → ran ( 𝐹 ↾ 𝑎 ) ∈ V )
62 60 61 syl ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ran ( 𝐹 ↾ 𝑎 ) ∈ V )
63 ressress ⊢ ( ( ran 𝐹 ∈ V ∧ ran ( 𝐹 ↾ 𝑎 ) ∈ V ) → ( ( 𝑇 ↾s ran 𝐹 ) ↾s ran ( 𝐹 ↾ 𝑎 ) ) = ( 𝑇 ↾s ( ran 𝐹 ∩ ran ( 𝐹 ↾ 𝑎 ) ) ) )
64 59 62 63 syl2anc ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( ( 𝑇 ↾s ran 𝐹 ) ↾s ran ( 𝐹 ↾ 𝑎 ) ) = ( 𝑇 ↾s ( ran 𝐹 ∩ ran ( 𝐹 ↾ 𝑎 ) ) ) )
65 58 64 syl5eq ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝑉 ↾s ran ( 𝐹 ↾ 𝑎 ) ) = ( 𝑇 ↾s ( ran 𝐹 ∩ ran ( 𝐹 ↾ 𝑎 ) ) ) )
66 57 65 eqtr4id ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝑇 ↾s ran ( 𝐹 ↾ 𝑎 ) ) = ( 𝑉 ↾s ran ( 𝐹 ↾ 𝑎 ) ) )
67 22 66 syl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ( 𝑇 ↾s ran ( 𝐹 ↾ 𝑎 ) ) = ( 𝑉 ↾s ran ( 𝐹 ↾ 𝑎 ) ) )
68 simpl3 ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → 𝑉 ∈ LNoeM )
69 lmhmrnlss ⊢ ( ( 𝐹 ↾ 𝑎 ) ∈ ( ( 𝑆 ↾s 𝑎 ) LMHom 𝑇 ) → ran ( 𝐹 ↾ 𝑎 ) ∈ ( LSubSp ‘ 𝑇 ) )
70 10 69 syl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ran ( 𝐹 ↾ 𝑎 ) ∈ ( LSubSp ‘ 𝑇 ) )
71 53 a1i ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ran ( 𝐹 ↾ 𝑎 ) ⊆ ran 𝐹 )
72 lmhmlmod2 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑇 ∈ LMod )
73 22 72 syl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → 𝑇 ∈ LMod )
74 lmhmrnlss ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ran 𝐹 ∈ ( LSubSp ‘ 𝑇 ) )
75 22 74 syl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ran 𝐹 ∈ ( LSubSp ‘ 𝑇 ) )
76 eqid ⊢ ( LSubSp ‘ 𝑇 ) = ( LSubSp ‘ 𝑇 )
77 eqid ⊢ ( LSubSp ‘ 𝑉 ) = ( LSubSp ‘ 𝑉 )
78 4 76 77 lsslss ⊢ ( ( 𝑇 ∈ LMod ∧ ran 𝐹 ∈ ( LSubSp ‘ 𝑇 ) ) → ( ran ( 𝐹 ↾ 𝑎 ) ∈ ( LSubSp ‘ 𝑉 ) ↔ ( ran ( 𝐹 ↾ 𝑎 ) ∈ ( LSubSp ‘ 𝑇 ) ∧ ran ( 𝐹 ↾ 𝑎 ) ⊆ ran 𝐹 ) ) )
79 73 75 78 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ( ran ( 𝐹 ↾ 𝑎 ) ∈ ( LSubSp ‘ 𝑉 ) ↔ ( ran ( 𝐹 ↾ 𝑎 ) ∈ ( LSubSp ‘ 𝑇 ) ∧ ran ( 𝐹 ↾ 𝑎 ) ⊆ ran 𝐹 ) ) )
80 70 71 79 mpbir2and ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ran ( 𝐹 ↾ 𝑎 ) ∈ ( LSubSp ‘ 𝑉 ) )
81 eqid ⊢ ( 𝑉 ↾s ran ( 𝐹 ↾ 𝑎 ) ) = ( 𝑉 ↾s ran ( 𝐹 ↾ 𝑎 ) )
82 77 81 lnmlssfg ⊢ ( ( 𝑉 ∈ LNoeM ∧ ran ( 𝐹 ↾ 𝑎 ) ∈ ( LSubSp ‘ 𝑉 ) ) → ( 𝑉 ↾s ran ( 𝐹 ↾ 𝑎 ) ) ∈ LFinGen )
83 68 80 82 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ( 𝑉 ↾s ran ( 𝐹 ↾ 𝑎 ) ) ∈ LFinGen )
84 67 83 eqeltrd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ( 𝑇 ↾s ran ( 𝐹 ↾ 𝑎 ) ) ∈ LFinGen )
85 eqid ⊢ ( ◡ ( 𝐹 ↾ 𝑎 ) “ { 0 } ) = ( ◡ ( 𝐹 ↾ 𝑎 ) “ { 0 } )
86 eqid ⊢ ( ( 𝑆 ↾s 𝑎 ) ↾s ( ◡ ( 𝐹 ↾ 𝑎 ) “ { 0 } ) ) = ( ( 𝑆 ↾s 𝑎 ) ↾s ( ◡ ( 𝐹 ↾ 𝑎 ) “ { 0 } ) )
87 eqid ⊢ ( 𝑇 ↾s ran ( 𝐹 ↾ 𝑎 ) ) = ( 𝑇 ↾s ran ( 𝐹 ↾ 𝑎 ) )
88 1 85 86 87 lmhmfgsplit ⊢ ( ( ( 𝐹 ↾ 𝑎 ) ∈ ( ( 𝑆 ↾s 𝑎 ) LMHom 𝑇 ) ∧ ( ( 𝑆 ↾s 𝑎 ) ↾s ( ◡ ( 𝐹 ↾ 𝑎 ) “ { 0 } ) ) ∈ LFinGen ∧ ( 𝑇 ↾s ran ( 𝐹 ↾ 𝑎 ) ) ∈ LFinGen ) → ( 𝑆 ↾s 𝑎 ) ∈ LFinGen )
89 10 49 84 88 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ) → ( 𝑆 ↾s 𝑎 ) ∈ LFinGen )
90 89 ralrimiva ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) → ∀ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ( 𝑆 ↾s 𝑎 ) ∈ LFinGen )
91 7 islnm ⊢ ( 𝑆 ∈ LNoeM ↔ ( 𝑆 ∈ LMod ∧ ∀ 𝑎 ∈ ( LSubSp ‘ 𝑆 ) ( 𝑆 ↾s 𝑎 ) ∈ LFinGen ) )
92 6 90 91 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM ) → 𝑆 ∈ LNoeM )