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 ⊢ 𝑌 = ( 𝑇 ↾s ( 𝐹 “ 𝐴 ) )
lmhmfgima.x ⊢ 𝑋 = ( 𝑆 ↾s 𝐴 )
lmhmfgima.u ⊢ 𝑈 = ( LSubSp ‘ 𝑆 )
lmhmfgima.xf ⊢ ( 𝜑 → 𝑋 ∈ LFinGen )
lmhmfgima.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
lmhmfgima.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
Assertion lmhmfgima ( 𝜑 → 𝑌 ∈ LFinGen )

Proof

Step Hyp Ref Expression
1 lmhmfgima.y ⊢ 𝑌 = ( 𝑇 ↾s ( 𝐹 “ 𝐴 ) )
2 lmhmfgima.x ⊢ 𝑋 = ( 𝑆 ↾s 𝐴 )
3 lmhmfgima.u ⊢ 𝑈 = ( LSubSp ‘ 𝑆 )
4 lmhmfgima.xf ⊢ ( 𝜑 → 𝑋 ∈ LFinGen )
5 lmhmfgima.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
6 lmhmfgima.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
7 lmhmlmod1 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
8 6 7 syl ⊢ ( 𝜑 → 𝑆 ∈ LMod )
9 eqid ⊢ ( LSpan ‘ 𝑆 ) = ( LSpan ‘ 𝑆 )
10 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
11 2 3 9 10 islssfg2 ⊢ ( ( 𝑆 ∈ LMod ∧ 𝐴 ∈ 𝑈 ) → ( 𝑋 ∈ LFinGen ↔ ∃ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ( ( LSpan ‘ 𝑆 ) ‘ 𝑥 ) = 𝐴 ) )
12 8 5 11 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∈ LFinGen ↔ ∃ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ( ( LSpan ‘ 𝑆 ) ‘ 𝑥 ) = 𝐴 ) )
13 4 12 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ( ( LSpan ‘ 𝑆 ) ‘ 𝑥 ) = 𝐴 )
14 inss1 ⊢ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ⊆ 𝒫 ( Base ‘ 𝑆 )
15 14 sseli ⊢ ( 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) → 𝑥 ∈ 𝒫 ( Base ‘ 𝑆 ) )
16 15 elpwid ⊢ ( 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) → 𝑥 ⊆ ( Base ‘ 𝑆 ) )
17 eqid ⊢ ( LSpan ‘ 𝑇 ) = ( LSpan ‘ 𝑇 )
18 10 9 17 lmhmlsp ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑥 ⊆ ( Base ‘ 𝑆 ) ) → ( 𝐹 “ ( ( LSpan ‘ 𝑆 ) ‘ 𝑥 ) ) = ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐹 “ 𝑥 ) ) )
19 6 16 18 syl2an ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ) → ( 𝐹 “ ( ( LSpan ‘ 𝑆 ) ‘ 𝑥 ) ) = ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐹 “ 𝑥 ) ) )
20 19 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ) → ( 𝑇 ↾s ( 𝐹 “ ( ( LSpan ‘ 𝑆 ) ‘ 𝑥 ) ) ) = ( 𝑇 ↾s ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐹 “ 𝑥 ) ) ) )
21 lmhmlmod2 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑇 ∈ LMod )
22 6 21 syl ⊢ ( 𝜑 → 𝑇 ∈ LMod )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ) → 𝑇 ∈ LMod )
24 imassrn ⊢ ( 𝐹 “ 𝑥 ) ⊆ ran 𝐹
25 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
26 10 25 lmhmf ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
27 6 26 syl ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
28 27 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ( Base ‘ 𝑇 ) )
29 24 28 sstrid ⊢ ( 𝜑 → ( 𝐹 “ 𝑥 ) ⊆ ( Base ‘ 𝑇 ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ) → ( 𝐹 “ 𝑥 ) ⊆ ( Base ‘ 𝑇 ) )
31 inss2 ⊢ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ⊆ Fin
32 31 sseli ⊢ ( 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) → 𝑥 ∈ Fin )
33 32 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ) → 𝑥 ∈ Fin )
34 27 ffund ⊢ ( 𝜑 → Fun 𝐹 )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ) → Fun 𝐹 )
36 16 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ) → 𝑥 ⊆ ( Base ‘ 𝑆 ) )
37 27 fdmd ⊢ ( 𝜑 → dom 𝐹 = ( Base ‘ 𝑆 ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ) → dom 𝐹 = ( Base ‘ 𝑆 ) )
39 36 38 sseqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ) → 𝑥 ⊆ dom 𝐹 )
40 fores ⊢ ( ( Fun 𝐹 ∧ 𝑥 ⊆ dom 𝐹 ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 –onto→ ( 𝐹 “ 𝑥 ) )
41 35 39 40 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 –onto→ ( 𝐹 “ 𝑥 ) )
42 fofi ⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝐹 ↾ 𝑥 ) : 𝑥 –onto→ ( 𝐹 “ 𝑥 ) ) → ( 𝐹 “ 𝑥 ) ∈ Fin )
43 33 41 42 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ) → ( 𝐹 “ 𝑥 ) ∈ Fin )
44 eqid ⊢ ( 𝑇 ↾s ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐹 “ 𝑥 ) ) ) = ( 𝑇 ↾s ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐹 “ 𝑥 ) ) )
45 17 25 44 islssfgi ⊢ ( ( 𝑇 ∈ LMod ∧ ( 𝐹 “ 𝑥 ) ⊆ ( Base ‘ 𝑇 ) ∧ ( 𝐹 “ 𝑥 ) ∈ Fin ) → ( 𝑇 ↾s ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐹 “ 𝑥 ) ) ) ∈ LFinGen )
46 23 30 43 45 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ) → ( 𝑇 ↾s ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐹 “ 𝑥 ) ) ) ∈ LFinGen )
47 20 46 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ) → ( 𝑇 ↾s ( 𝐹 “ ( ( LSpan ‘ 𝑆 ) ‘ 𝑥 ) ) ) ∈ LFinGen )
48 imaeq2 ⊢ ( ( ( LSpan ‘ 𝑆 ) ‘ 𝑥 ) = 𝐴 → ( 𝐹 “ ( ( LSpan ‘ 𝑆 ) ‘ 𝑥 ) ) = ( 𝐹 “ 𝐴 ) )
49 48 oveq2d ⊢ ( ( ( LSpan ‘ 𝑆 ) ‘ 𝑥 ) = 𝐴 → ( 𝑇 ↾s ( 𝐹 “ ( ( LSpan ‘ 𝑆 ) ‘ 𝑥 ) ) ) = ( 𝑇 ↾s ( 𝐹 “ 𝐴 ) ) )
50 49 eleq1d ⊢ ( ( ( LSpan ‘ 𝑆 ) ‘ 𝑥 ) = 𝐴 → ( ( 𝑇 ↾s ( 𝐹 “ ( ( LSpan ‘ 𝑆 ) ‘ 𝑥 ) ) ) ∈ LFinGen ↔ ( 𝑇 ↾s ( 𝐹 “ 𝐴 ) ) ∈ LFinGen ) )
51 47 50 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ) → ( ( ( LSpan ‘ 𝑆 ) ‘ 𝑥 ) = 𝐴 → ( 𝑇 ↾s ( 𝐹 “ 𝐴 ) ) ∈ LFinGen ) )
52 51 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝒫 ( Base ‘ 𝑆 ) ∩ Fin ) ( ( LSpan ‘ 𝑆 ) ‘ 𝑥 ) = 𝐴 → ( 𝑇 ↾s ( 𝐹 “ 𝐴 ) ) ∈ LFinGen ) )
53 13 52 mpd ⊢ ( 𝜑 → ( 𝑇 ↾s ( 𝐹 “ 𝐴 ) ) ∈ LFinGen )
54 1 53 eqeltrid ⊢ ( 𝜑 → 𝑌 ∈ LFinGen )