Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lmhmfgima Structured version   Visualization version   GIF version

Theorem lmhmfgima 40620
Description: A homomorphism maps finitely generated submodules to finitely generated submodules. (Contributed by Stefan O'Rear, 24-Jan-2015.)
Hypotheses
Ref Expression
lmhmfgima.y 𝑌 = (𝑇s (𝐹𝐴))
lmhmfgima.x 𝑋 = (𝑆s 𝐴)
lmhmfgima.u 𝑈 = (LSubSp‘𝑆)
lmhmfgima.xf (𝜑𝑋 ∈ LFinGen)
lmhmfgima.a (𝜑𝐴𝑈)
lmhmfgima.f (𝜑𝐹 ∈ (𝑆 LMHom 𝑇))
Assertion
Ref Expression
lmhmfgima (𝜑𝑌 ∈ LFinGen)

Proof of Theorem lmhmfgima
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 lmhmfgima.y . 2 𝑌 = (𝑇s (𝐹𝐴))
2 lmhmfgima.xf . . . 4 (𝜑𝑋 ∈ LFinGen)
3 lmhmfgima.f . . . . . 6 (𝜑𝐹 ∈ (𝑆 LMHom 𝑇))
4 lmhmlmod1 20075 . . . . . 6 (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod)
53, 4syl 17 . . . . 5 (𝜑𝑆 ∈ LMod)
6 lmhmfgima.a . . . . 5 (𝜑𝐴𝑈)
7 lmhmfgima.x . . . . . 6 𝑋 = (𝑆s 𝐴)
8 lmhmfgima.u . . . . . 6 𝑈 = (LSubSp‘𝑆)
9 eqid 2737 . . . . . 6 (LSpan‘𝑆) = (LSpan‘𝑆)
10 eqid 2737 . . . . . 6 (Base‘𝑆) = (Base‘𝑆)
117, 8, 9, 10islssfg2 40607 . . . . 5 ((𝑆 ∈ LMod ∧ 𝐴𝑈) → (𝑋 ∈ LFinGen ↔ ∃𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)((LSpan‘𝑆)‘𝑥) = 𝐴))
125, 6, 11syl2anc 587 . . . 4 (𝜑 → (𝑋 ∈ LFinGen ↔ ∃𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)((LSpan‘𝑆)‘𝑥) = 𝐴))
132, 12mpbid 235 . . 3 (𝜑 → ∃𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)((LSpan‘𝑆)‘𝑥) = 𝐴)
14 inss1 4148 . . . . . . . . . 10 (𝒫 (Base‘𝑆) ∩ Fin) ⊆ 𝒫 (Base‘𝑆)
1514sseli 3901 . . . . . . . . 9 (𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin) → 𝑥 ∈ 𝒫 (Base‘𝑆))
1615elpwid 4529 . . . . . . . 8 (𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin) → 𝑥 ⊆ (Base‘𝑆))
17 eqid 2737 . . . . . . . . 9 (LSpan‘𝑇) = (LSpan‘𝑇)
1810, 9, 17lmhmlsp 20091 . . . . . . . 8 ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑥 ⊆ (Base‘𝑆)) → (𝐹 “ ((LSpan‘𝑆)‘𝑥)) = ((LSpan‘𝑇)‘(𝐹𝑥)))
193, 16, 18syl2an 599 . . . . . . 7 ((𝜑𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝐹 “ ((LSpan‘𝑆)‘𝑥)) = ((LSpan‘𝑇)‘(𝐹𝑥)))
2019oveq2d 7234 . . . . . 6 ((𝜑𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝑇s (𝐹 “ ((LSpan‘𝑆)‘𝑥))) = (𝑇s ((LSpan‘𝑇)‘(𝐹𝑥))))
21 lmhmlmod2 20074 . . . . . . . . 9 (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod)
223, 21syl 17 . . . . . . . 8 (𝜑𝑇 ∈ LMod)
2322adantr 484 . . . . . . 7 ((𝜑𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → 𝑇 ∈ LMod)
24 imassrn 5945 . . . . . . . . 9 (𝐹𝑥) ⊆ ran 𝐹
25 eqid 2737 . . . . . . . . . . . 12 (Base‘𝑇) = (Base‘𝑇)
2610, 25lmhmf 20076 . . . . . . . . . . 11 (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇))
273, 26syl 17 . . . . . . . . . 10 (𝜑𝐹:(Base‘𝑆)⟶(Base‘𝑇))
2827frnd 6558 . . . . . . . . 9 (𝜑 → ran 𝐹 ⊆ (Base‘𝑇))
2924, 28sstrid 3917 . . . . . . . 8 (𝜑 → (𝐹𝑥) ⊆ (Base‘𝑇))
3029adantr 484 . . . . . . 7 ((𝜑𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝐹𝑥) ⊆ (Base‘𝑇))
31 inss2 4149 . . . . . . . . . 10 (𝒫 (Base‘𝑆) ∩ Fin) ⊆ Fin
3231sseli 3901 . . . . . . . . 9 (𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin) → 𝑥 ∈ Fin)
3332adantl 485 . . . . . . . 8 ((𝜑𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → 𝑥 ∈ Fin)
3427ffund 6554 . . . . . . . . . 10 (𝜑 → Fun 𝐹)
3534adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → Fun 𝐹)
3616adantl 485 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → 𝑥 ⊆ (Base‘𝑆))
3727fdmd 6561 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = (Base‘𝑆))
3837adantr 484 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → dom 𝐹 = (Base‘𝑆))
3936, 38sseqtrrd 3947 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → 𝑥 ⊆ dom 𝐹)
40 fores 6648 . . . . . . . . 9 ((Fun 𝐹𝑥 ⊆ dom 𝐹) → (𝐹𝑥):𝑥onto→(𝐹𝑥))
4135, 39, 40syl2anc 587 . . . . . . . 8 ((𝜑𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝐹𝑥):𝑥onto→(𝐹𝑥))
42 fofi 8967 . . . . . . . 8 ((𝑥 ∈ Fin ∧ (𝐹𝑥):𝑥onto→(𝐹𝑥)) → (𝐹𝑥) ∈ Fin)
4333, 41, 42syl2anc 587 . . . . . . 7 ((𝜑𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝐹𝑥) ∈ Fin)
44 eqid 2737 . . . . . . . 8 (𝑇s ((LSpan‘𝑇)‘(𝐹𝑥))) = (𝑇s ((LSpan‘𝑇)‘(𝐹𝑥)))
4517, 25, 44islssfgi 40608 . . . . . . 7 ((𝑇 ∈ LMod ∧ (𝐹𝑥) ⊆ (Base‘𝑇) ∧ (𝐹𝑥) ∈ Fin) → (𝑇s ((LSpan‘𝑇)‘(𝐹𝑥))) ∈ LFinGen)
4623, 30, 43, 45syl3anc 1373 . . . . . 6 ((𝜑𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝑇s ((LSpan‘𝑇)‘(𝐹𝑥))) ∈ LFinGen)
4720, 46eqeltrd 2838 . . . . 5 ((𝜑𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝑇s (𝐹 “ ((LSpan‘𝑆)‘𝑥))) ∈ LFinGen)
48 imaeq2 5930 . . . . . . 7 (((LSpan‘𝑆)‘𝑥) = 𝐴 → (𝐹 “ ((LSpan‘𝑆)‘𝑥)) = (𝐹𝐴))
4948oveq2d 7234 . . . . . 6 (((LSpan‘𝑆)‘𝑥) = 𝐴 → (𝑇s (𝐹 “ ((LSpan‘𝑆)‘𝑥))) = (𝑇s (𝐹𝐴)))
5049eleq1d 2822 . . . . 5 (((LSpan‘𝑆)‘𝑥) = 𝐴 → ((𝑇s (𝐹 “ ((LSpan‘𝑆)‘𝑥))) ∈ LFinGen ↔ (𝑇s (𝐹𝐴)) ∈ LFinGen))
5147, 50syl5ibcom 248 . . . 4 ((𝜑𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (((LSpan‘𝑆)‘𝑥) = 𝐴 → (𝑇s (𝐹𝐴)) ∈ LFinGen))
5251rexlimdva 3208 . . 3 (𝜑 → (∃𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)((LSpan‘𝑆)‘𝑥) = 𝐴 → (𝑇s (𝐹𝐴)) ∈ LFinGen))
5313, 52mpd 15 . 2 (𝜑 → (𝑇s (𝐹𝐴)) ∈ LFinGen)
541, 53eqeltrid 2842 1 (𝜑𝑌 ∈ LFinGen)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1543  wcel 2110  wrex 3062  cin 3870  wss 3871  𝒫 cpw 4518  dom cdm 5556  ran crn 5557  cres 5558  cima 5559  Fun wfun 6379  wf 6381  ontowfo 6383  cfv 6385  (class class class)co 7218  Fincfn 8631  Basecbs 16765  s cress 16789  LModclmod 19904  LSubSpclss 19973  LSpanclspn 20013   LMHom clmhm 20061  LFinGenclfig 40603
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5184  ax-sep 5197  ax-nul 5204  ax-pow 5263  ax-pr 5327  ax-un 7528  ax-cnex 10790  ax-resscn 10791  ax-1cn 10792  ax-icn 10793  ax-addcl 10794  ax-addrcl 10795  ax-mulcl 10796  ax-mulrcl 10797  ax-mulcom 10798  ax-addass 10799  ax-mulass 10800  ax-distr 10801  ax-i2m1 10802  ax-1ne0 10803  ax-1rid 10804  ax-rnegex 10805  ax-rrecex 10806  ax-cnre 10807  ax-pre-lttri 10808  ax-pre-lttrn 10809  ax-pre-ltadd 10810  ax-pre-mulgt0 10811
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-pss 3890  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-tp 4551  df-op 4553  df-uni 4825  df-int 4865  df-iun 4911  df-br 5059  df-opab 5121  df-mpt 5141  df-tr 5167  df-id 5460  df-eprel 5465  df-po 5473  df-so 5474  df-fr 5514  df-we 5516  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-pred 6165  df-ord 6221  df-on 6222  df-lim 6223  df-suc 6224  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-riota 7175  df-ov 7221  df-oprab 7222  df-mpo 7223  df-om 7650  df-1st 7766  df-2nd 7767  df-wrecs 8052  df-recs 8113  df-rdg 8151  df-1o 8207  df-er 8396  df-en 8632  df-dom 8633  df-sdom 8634  df-fin 8635  df-pnf 10874  df-mnf 10875  df-xr 10876  df-ltxr 10877  df-le 10878  df-sub 11069  df-neg 11070  df-nn 11836  df-2 11898  df-3 11899  df-4 11900  df-5 11901  df-6 11902  df-sets 16722  df-slot 16740  df-ndx 16750  df-base 16766  df-ress 16790  df-plusg 16820  df-sca 16823  df-vsca 16824  df-0g 16951  df-mgm 18119  df-sgrp 18168  df-mnd 18179  df-grp 18373  df-minusg 18374  df-sbg 18375  df-subg 18545  df-ghm 18625  df-mgp 19510  df-ur 19522  df-ring 19569  df-lmod 19906  df-lss 19974  df-lsp 20014  df-lmhm 20064  df-lfig 40604
This theorem is referenced by:  lnmepi  40621
  Copyright terms: Public domain W3C validator