Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  gsumlsscl Structured version   Visualization version   GIF version

Theorem gsumlsscl 45400
Description: Closure of a group sum in a linear subspace: A (finitely supported) sum of scalar multiplications of vectors of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019.) (Revised by AV, 28-Jul-2019.)
Hypotheses
Ref Expression
gsumlsscl.s 𝑆 = (LSubSp‘𝑀)
gsumlsscl.r 𝑅 = (Scalar‘𝑀)
gsumlsscl.b 𝐵 = (Base‘𝑅)
Assertion
Ref Expression
gsumlsscl ((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) → ((𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅)) → (𝑀 Σg (𝑣𝑉 ↦ ((𝐹𝑣)( ·𝑠𝑀)𝑣))) ∈ 𝑍))
Distinct variable groups:   𝑣,𝐵   𝑣,𝐹   𝑣,𝑀   𝑣,𝑅   𝑣,𝑆   𝑣,𝑉   𝑣,𝑍

Proof of Theorem gsumlsscl
StepHypRef Expression
1 eqid 2737 . . 3 (0g𝑀) = (0g𝑀)
2 lmodabl 19951 . . . . 5 (𝑀 ∈ LMod → 𝑀 ∈ Abel)
323ad2ant1 1135 . . . 4 ((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) → 𝑀 ∈ Abel)
43adantr 484 . . 3 (((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) ∧ (𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅))) → 𝑀 ∈ Abel)
5 ssexg 5221 . . . . . 6 ((𝑉𝑍𝑍𝑆) → 𝑉 ∈ V)
65ancoms 462 . . . . 5 ((𝑍𝑆𝑉𝑍) → 𝑉 ∈ V)
763adant1 1132 . . . 4 ((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) → 𝑉 ∈ V)
87adantr 484 . . 3 (((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) ∧ (𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅))) → 𝑉 ∈ V)
9 3simpa 1150 . . . . 5 ((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) → (𝑀 ∈ LMod ∧ 𝑍𝑆))
10 gsumlsscl.s . . . . . 6 𝑆 = (LSubSp‘𝑀)
1110lsssubg 19999 . . . . 5 ((𝑀 ∈ LMod ∧ 𝑍𝑆) → 𝑍 ∈ (SubGrp‘𝑀))
129, 11syl 17 . . . 4 ((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) → 𝑍 ∈ (SubGrp‘𝑀))
1312adantr 484 . . 3 (((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) ∧ (𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅))) → 𝑍 ∈ (SubGrp‘𝑀))
149adantr 484 . . . . . 6 (((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) ∧ (𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅))) → (𝑀 ∈ LMod ∧ 𝑍𝑆))
1514adantr 484 . . . . 5 ((((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) ∧ (𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅))) ∧ 𝑣𝑉) → (𝑀 ∈ LMod ∧ 𝑍𝑆))
16 elmapi 8535 . . . . . . . 8 (𝐹 ∈ (𝐵m 𝑉) → 𝐹:𝑉𝐵)
17 ffvelrn 6907 . . . . . . . . 9 ((𝐹:𝑉𝐵𝑣𝑉) → (𝐹𝑣) ∈ 𝐵)
1817ex 416 . . . . . . . 8 (𝐹:𝑉𝐵 → (𝑣𝑉 → (𝐹𝑣) ∈ 𝐵))
1916, 18syl 17 . . . . . . 7 (𝐹 ∈ (𝐵m 𝑉) → (𝑣𝑉 → (𝐹𝑣) ∈ 𝐵))
2019ad2antrl 728 . . . . . 6 (((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) ∧ (𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅))) → (𝑣𝑉 → (𝐹𝑣) ∈ 𝐵))
2120imp 410 . . . . 5 ((((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) ∧ (𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅))) ∧ 𝑣𝑉) → (𝐹𝑣) ∈ 𝐵)
22 ssel 3898 . . . . . . . 8 (𝑉𝑍 → (𝑣𝑉𝑣𝑍))
23223ad2ant3 1137 . . . . . . 7 ((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) → (𝑣𝑉𝑣𝑍))
2423adantr 484 . . . . . 6 (((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) ∧ (𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅))) → (𝑣𝑉𝑣𝑍))
2524imp 410 . . . . 5 ((((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) ∧ (𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅))) ∧ 𝑣𝑉) → 𝑣𝑍)
26 gsumlsscl.r . . . . . 6 𝑅 = (Scalar‘𝑀)
27 eqid 2737 . . . . . 6 ( ·𝑠𝑀) = ( ·𝑠𝑀)
28 gsumlsscl.b . . . . . 6 𝐵 = (Base‘𝑅)
2926, 27, 28, 10lssvscl 19997 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑍𝑆) ∧ ((𝐹𝑣) ∈ 𝐵𝑣𝑍)) → ((𝐹𝑣)( ·𝑠𝑀)𝑣) ∈ 𝑍)
3015, 21, 25, 29syl12anc 837 . . . 4 ((((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) ∧ (𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅))) ∧ 𝑣𝑉) → ((𝐹𝑣)( ·𝑠𝑀)𝑣) ∈ 𝑍)
3130fmpttd 6937 . . 3 (((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) ∧ (𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅))) → (𝑣𝑉 ↦ ((𝐹𝑣)( ·𝑠𝑀)𝑣)):𝑉𝑍)
32 simp1 1138 . . . . . 6 ((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) → 𝑀 ∈ LMod)
33 eqid 2737 . . . . . . . . . . 11 (Base‘𝑀) = (Base‘𝑀)
3433, 10lssss 19978 . . . . . . . . . 10 (𝑍𝑆𝑍 ⊆ (Base‘𝑀))
35 sstr 3914 . . . . . . . . . . 11 ((𝑉𝑍𝑍 ⊆ (Base‘𝑀)) → 𝑉 ⊆ (Base‘𝑀))
3635expcom 417 . . . . . . . . . 10 (𝑍 ⊆ (Base‘𝑀) → (𝑉𝑍𝑉 ⊆ (Base‘𝑀)))
3734, 36syl 17 . . . . . . . . 9 (𝑍𝑆 → (𝑉𝑍𝑉 ⊆ (Base‘𝑀)))
3837a1i 11 . . . . . . . 8 (𝑀 ∈ LMod → (𝑍𝑆 → (𝑉𝑍𝑉 ⊆ (Base‘𝑀))))
39383imp 1113 . . . . . . 7 ((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) → 𝑉 ⊆ (Base‘𝑀))
40 elpwg 4521 . . . . . . . 8 (𝑉 ∈ V → (𝑉 ∈ 𝒫 (Base‘𝑀) ↔ 𝑉 ⊆ (Base‘𝑀)))
417, 40syl 17 . . . . . . 7 ((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) → (𝑉 ∈ 𝒫 (Base‘𝑀) ↔ 𝑉 ⊆ (Base‘𝑀)))
4239, 41mpbird 260 . . . . . 6 ((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) → 𝑉 ∈ 𝒫 (Base‘𝑀))
4332, 42jca 515 . . . . 5 ((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) → (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)))
4443adantr 484 . . . 4 (((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) ∧ (𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅))) → (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)))
45 simprl 771 . . . 4 (((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) ∧ (𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅))) → 𝐹 ∈ (𝐵m 𝑉))
46 simprr 773 . . . 4 (((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) ∧ (𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅))) → 𝐹 finSupp (0g𝑅))
4726, 28scmfsupp 45395 . . . 4 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅)) → (𝑣𝑉 ↦ ((𝐹𝑣)( ·𝑠𝑀)𝑣)) finSupp (0g𝑀))
4844, 45, 46, 47syl3anc 1373 . . 3 (((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) ∧ (𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅))) → (𝑣𝑉 ↦ ((𝐹𝑣)( ·𝑠𝑀)𝑣)) finSupp (0g𝑀))
491, 4, 8, 13, 31, 48gsumsubgcl 19310 . 2 (((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) ∧ (𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅))) → (𝑀 Σg (𝑣𝑉 ↦ ((𝐹𝑣)( ·𝑠𝑀)𝑣))) ∈ 𝑍)
5049ex 416 1 ((𝑀 ∈ LMod ∧ 𝑍𝑆𝑉𝑍) → ((𝐹 ∈ (𝐵m 𝑉) ∧ 𝐹 finSupp (0g𝑅)) → (𝑀 Σg (𝑣𝑉 ↦ ((𝐹𝑣)( ·𝑠𝑀)𝑣))) ∈ 𝑍))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1089   = wceq 1543  wcel 2110  Vcvv 3413  wss 3871  𝒫 cpw 4518   class class class wbr 5058  cmpt 5140  wf 6381  cfv 6385  (class class class)co 7218  m cmap 8513   finSupp cfsupp 8990  Basecbs 16765  Scalarcsca 16810   ·𝑠 cvsca 16811  0gc0g 16949   Σg cgsu 16950  SubGrpcsubg 18542  Abelcabl 19176  LModclmod 19904  LSubSpclss 19973
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-se 5515  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-isom 6394  df-riota 7175  df-ov 7221  df-oprab 7222  df-mpo 7223  df-om 7650  df-1st 7766  df-2nd 7767  df-supp 7909  df-wrecs 8052  df-recs 8113  df-rdg 8151  df-1o 8207  df-er 8396  df-map 8515  df-en 8632  df-dom 8633  df-sdom 8634  df-fin 8635  df-fsupp 8991  df-oi 9131  df-card 9560  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-n0 12096  df-z 12182  df-uz 12444  df-fz 13101  df-fzo 13244  df-seq 13580  df-hash 13902  df-sets 16722  df-slot 16740  df-ndx 16750  df-base 16766  df-ress 16790  df-plusg 16820  df-0g 16951  df-gsum 16952  df-mgm 18119  df-sgrp 18168  df-mnd 18179  df-submnd 18224  df-grp 18373  df-minusg 18374  df-sbg 18375  df-subg 18545  df-cntz 18716  df-cmn 19177  df-abl 19178  df-mgp 19510  df-ur 19522  df-ring 19569  df-lmod 19906  df-lss 19974
This theorem is referenced by:  lincellss  45448
  Copyright terms: Public domain W3C validator