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

Proof

Step Hyp Ref Expression
1 lmhmfgsplit.z ⊢ 0 = ( 0g ‘ 𝑇 )
2 lmhmfgsplit.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
3 lmhmfgsplit.u ⊢ 𝑈 = ( 𝑆 ↾s 𝐾 )
4 lmhmfgsplit.v ⊢ 𝑉 = ( 𝑇 ↾s ran 𝐹 )
5 simp3 ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) → 𝑉 ∈ LFinGen )
6 lmhmlmod2 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑇 ∈ LMod )
7 6 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) → 𝑇 ∈ LMod )
8 lmhmrnlss ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ran 𝐹 ∈ ( LSubSp ‘ 𝑇 ) )
9 8 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) → ran 𝐹 ∈ ( LSubSp ‘ 𝑇 ) )
10 eqid ⊢ ( LSubSp ‘ 𝑇 ) = ( LSubSp ‘ 𝑇 )
11 eqid ⊢ ( LSpan ‘ 𝑇 ) = ( LSpan ‘ 𝑇 )
12 4 10 11 islssfg ⊢ ( ( 𝑇 ∈ LMod ∧ ran 𝐹 ∈ ( LSubSp ‘ 𝑇 ) ) → ( 𝑉 ∈ LFinGen ↔ ∃ 𝑎 ∈ 𝒫 ran 𝐹 ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) )
13 7 9 12 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) → ( 𝑉 ∈ LFinGen ↔ ∃ 𝑎 ∈ 𝒫 ran 𝐹 ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) )
14 5 13 mpbid ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) → ∃ 𝑎 ∈ 𝒫 ran 𝐹 ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) )
15 simpl1 ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
16 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
17 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
18 16 17 lmhmf ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
19 ffn ⊢ ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) → 𝐹 Fn ( Base ‘ 𝑆 ) )
20 15 18 19 3syl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) → 𝐹 Fn ( Base ‘ 𝑆 ) )
21 elpwi ⊢ ( 𝑎 ∈ 𝒫 ran 𝐹 → 𝑎 ⊆ ran 𝐹 )
22 21 ad2antrl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) → 𝑎 ⊆ ran 𝐹 )
23 simprrl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) → 𝑎 ∈ Fin )
24 fipreima ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑆 ) ∧ 𝑎 ⊆ ran 𝐹 ∧ 𝑎 ∈ Fin ) → ∃ 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ( 𝐹 “ 𝑏 ) = 𝑎 )
25 20 22 23 24 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) → ∃ 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ( 𝐹 “ 𝑏 ) = 𝑎 )
26 eqid ⊢ ( LSubSp ‘ 𝑆 ) = ( LSubSp ‘ 𝑆 )
27 eqid ⊢ ( LSSum ‘ 𝑆 ) = ( LSSum ‘ 𝑆 )
28 simpll1 ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
29 lmhmlmod1 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
30 29 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) → 𝑆 ∈ LMod )
31 30 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → 𝑆 ∈ LMod )
32 inss1 ⊢ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ⊆ 𝒫 ( Base ‘ 𝑆 )
33 32 sseli ⊢ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) → 𝑏 ∈ 𝒫 ( Base ‘ 𝑆 ) )
34 elpwi ⊢ ( 𝑏 ∈ 𝒫 ( Base ‘ 𝑆 ) → 𝑏 ⊆ ( Base ‘ 𝑆 ) )
35 33 34 syl ⊢ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) → 𝑏 ⊆ ( Base ‘ 𝑆 ) )
36 35 ad2antrl ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → 𝑏 ⊆ ( Base ‘ 𝑆 ) )
37 eqid ⊢ ( LSpan ‘ 𝑆 ) = ( LSpan ‘ 𝑆 )
38 16 26 37 lspcl ⊢ ( ( 𝑆 ∈ LMod ∧ 𝑏 ⊆ ( Base ‘ 𝑆 ) ) → ( ( LSpan ‘ 𝑆 ) ‘ 𝑏 ) ∈ ( LSubSp ‘ 𝑆 ) )
39 31 36 38 syl2anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → ( ( LSpan ‘ 𝑆 ) ‘ 𝑏 ) ∈ ( LSubSp ‘ 𝑆 ) )
40 16 37 11 lmhmlsp ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑏 ⊆ ( Base ‘ 𝑆 ) ) → ( 𝐹 “ ( ( LSpan ‘ 𝑆 ) ‘ 𝑏 ) ) = ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐹 “ 𝑏 ) ) )
41 28 36 40 syl2anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → ( 𝐹 “ ( ( LSpan ‘ 𝑆 ) ‘ 𝑏 ) ) = ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐹 “ 𝑏 ) ) )
42 fveq2 ⊢ ( ( 𝐹 “ 𝑏 ) = 𝑎 → ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐹 “ 𝑏 ) ) = ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) )
43 42 ad2antll ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐹 “ 𝑏 ) ) = ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) )
44 simp2rr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 )
45 44 3expa ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 )
46 41 43 45 3eqtrd ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → ( 𝐹 “ ( ( LSpan ‘ 𝑆 ) ‘ 𝑏 ) ) = ran 𝐹 )
47 26 27 1 2 16 28 39 46 kercvrlsm ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → ( 𝐾 ( LSSum ‘ 𝑆 ) ( ( LSpan ‘ 𝑆 ) ‘ 𝑏 ) ) = ( Base ‘ 𝑆 ) )
48 47 oveq2d ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → ( 𝑆 ↾s ( 𝐾 ( LSSum ‘ 𝑆 ) ( ( LSpan ‘ 𝑆 ) ‘ 𝑏 ) ) ) = ( 𝑆 ↾s ( Base ‘ 𝑆 ) ) )
49 16 ressid ⊢ ( 𝑆 ∈ LMod → ( 𝑆 ↾s ( Base ‘ 𝑆 ) ) = 𝑆 )
50 30 49 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) → ( 𝑆 ↾s ( Base ‘ 𝑆 ) ) = 𝑆 )
51 50 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → ( 𝑆 ↾s ( Base ‘ 𝑆 ) ) = 𝑆 )
52 48 51 eqtr2d ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → 𝑆 = ( 𝑆 ↾s ( 𝐾 ( LSSum ‘ 𝑆 ) ( ( LSpan ‘ 𝑆 ) ‘ 𝑏 ) ) ) )
53 eqid ⊢ ( 𝑆 ↾s ( ( LSpan ‘ 𝑆 ) ‘ 𝑏 ) ) = ( 𝑆 ↾s ( ( LSpan ‘ 𝑆 ) ‘ 𝑏 ) )
54 eqid ⊢ ( 𝑆 ↾s ( 𝐾 ( LSSum ‘ 𝑆 ) ( ( LSpan ‘ 𝑆 ) ‘ 𝑏 ) ) ) = ( 𝑆 ↾s ( 𝐾 ( LSSum ‘ 𝑆 ) ( ( LSpan ‘ 𝑆 ) ‘ 𝑏 ) ) )
55 2 1 26 lmhmkerlss ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐾 ∈ ( LSubSp ‘ 𝑆 ) )
56 55 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) → 𝐾 ∈ ( LSubSp ‘ 𝑆 ) )
57 56 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → 𝐾 ∈ ( LSubSp ‘ 𝑆 ) )
58 simpll2 ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → 𝑈 ∈ LFinGen )
59 inss2 ⊢ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ⊆ Fin
60 59 sseli ⊢ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) → 𝑏 ∈ Fin )
61 60 ad2antrl ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → 𝑏 ∈ Fin )
62 37 16 53 islssfgi ⊢ ( ( 𝑆 ∈ LMod ∧ 𝑏 ⊆ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ Fin ) → ( 𝑆 ↾s ( ( LSpan ‘ 𝑆 ) ‘ 𝑏 ) ) ∈ LFinGen )
63 31 36 61 62 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → ( 𝑆 ↾s ( ( LSpan ‘ 𝑆 ) ‘ 𝑏 ) ) ∈ LFinGen )
64 26 27 3 53 54 31 57 39 58 63 lsmfgcl ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → ( 𝑆 ↾s ( 𝐾 ( LSSum ‘ 𝑆 ) ( ( LSpan ‘ 𝑆 ) ‘ 𝑏 ) ) ) ∈ LFinGen )
65 52 64 eqeltrd ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ∧ ( 𝐹 “ 𝑏 ) = 𝑎 ) ) → 𝑆 ∈ LFinGen )
66 25 65 rexlimddv ⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) ∧ ( 𝑎 ∈ 𝒫 ran 𝐹 ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑇 ) ‘ 𝑎 ) = ran 𝐹 ) ) ) → 𝑆 ∈ LFinGen )
67 14 66 rexlimddv ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen ) → 𝑆 ∈ LFinGen )