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

Theorem ellcoellss 44666
 Description: Every linear combination of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.)
Assertion
Ref Expression
ellcoellss ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) → ∀𝑥 ∈ (𝑀 LinCo 𝑉)𝑥𝑆)
Distinct variable groups:   𝑥,𝑀   𝑥,𝑆   𝑥,𝑉

Proof of Theorem ellcoellss
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 simp1 1133 . . . 4 ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) → 𝑀 ∈ LMod)
2 eqid 2821 . . . . . . 7 (Base‘𝑀) = (Base‘𝑀)
3 eqid 2821 . . . . . . 7 (LSubSp‘𝑀) = (LSubSp‘𝑀)
42, 3lssss 19684 . . . . . 6 (𝑆 ∈ (LSubSp‘𝑀) → 𝑆 ⊆ (Base‘𝑀))
543ad2ant2 1131 . . . . 5 ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) → 𝑆 ⊆ (Base‘𝑀))
6 sstr 3951 . . . . . . . 8 ((𝑉𝑆𝑆 ⊆ (Base‘𝑀)) → 𝑉 ⊆ (Base‘𝑀))
7 fvex 6656 . . . . . . . . . 10 (Base‘𝑀) ∈ V
87ssex 5198 . . . . . . . . 9 (𝑉 ⊆ (Base‘𝑀) → 𝑉 ∈ V)
9 elpwg 4515 . . . . . . . . . 10 (𝑉 ∈ V → (𝑉 ∈ 𝒫 (Base‘𝑀) ↔ 𝑉 ⊆ (Base‘𝑀)))
109biimprd 251 . . . . . . . . 9 (𝑉 ∈ V → (𝑉 ⊆ (Base‘𝑀) → 𝑉 ∈ 𝒫 (Base‘𝑀)))
118, 10mpcom 38 . . . . . . . 8 (𝑉 ⊆ (Base‘𝑀) → 𝑉 ∈ 𝒫 (Base‘𝑀))
126, 11syl 17 . . . . . . 7 ((𝑉𝑆𝑆 ⊆ (Base‘𝑀)) → 𝑉 ∈ 𝒫 (Base‘𝑀))
1312ex 416 . . . . . 6 (𝑉𝑆 → (𝑆 ⊆ (Base‘𝑀) → 𝑉 ∈ 𝒫 (Base‘𝑀)))
14133ad2ant3 1132 . . . . 5 ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) → (𝑆 ⊆ (Base‘𝑀) → 𝑉 ∈ 𝒫 (Base‘𝑀)))
155, 14mpd 15 . . . 4 ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) → 𝑉 ∈ 𝒫 (Base‘𝑀))
16 eqid 2821 . . . . 5 (Scalar‘𝑀) = (Scalar‘𝑀)
17 eqid 2821 . . . . 5 (Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀))
182, 16, 17lcoval 44643 . . . 4 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝑥 ∈ (𝑀 LinCo 𝑉) ↔ (𝑥 ∈ (Base‘𝑀) ∧ ∃𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑓 finSupp (0g‘(Scalar‘𝑀)) ∧ 𝑥 = (𝑓( linC ‘𝑀)𝑉)))))
191, 15, 18syl2anc 587 . . 3 ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) → (𝑥 ∈ (𝑀 LinCo 𝑉) ↔ (𝑥 ∈ (Base‘𝑀) ∧ ∃𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑓 finSupp (0g‘(Scalar‘𝑀)) ∧ 𝑥 = (𝑓( linC ‘𝑀)𝑉)))))
20 lincellss 44657 . . . . . . . . . . . . 13 ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) → ((𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑓 finSupp (0g‘(Scalar‘𝑀))) → (𝑓( linC ‘𝑀)𝑉) ∈ 𝑆))
2120imp 410 . . . . . . . . . . . 12 (((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) ∧ (𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑓 finSupp (0g‘(Scalar‘𝑀)))) → (𝑓( linC ‘𝑀)𝑉) ∈ 𝑆)
22 eleq1 2899 . . . . . . . . . . . 12 (𝑥 = (𝑓( linC ‘𝑀)𝑉) → (𝑥𝑆 ↔ (𝑓( linC ‘𝑀)𝑉) ∈ 𝑆))
2321, 22syl5ibr 249 . . . . . . . . . . 11 (𝑥 = (𝑓( linC ‘𝑀)𝑉) → (((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) ∧ (𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑓 finSupp (0g‘(Scalar‘𝑀)))) → 𝑥𝑆))
2423expd 419 . . . . . . . . . 10 (𝑥 = (𝑓( linC ‘𝑀)𝑉) → ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) → ((𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑓 finSupp (0g‘(Scalar‘𝑀))) → 𝑥𝑆)))
2524com12 32 . . . . . . . . 9 ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) → (𝑥 = (𝑓( linC ‘𝑀)𝑉) → ((𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑓 finSupp (0g‘(Scalar‘𝑀))) → 𝑥𝑆)))
2625adantr 484 . . . . . . . 8 (((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) ∧ 𝑥 ∈ (Base‘𝑀)) → (𝑥 = (𝑓( linC ‘𝑀)𝑉) → ((𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑓 finSupp (0g‘(Scalar‘𝑀))) → 𝑥𝑆)))
2726com13 88 . . . . . . 7 ((𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑓 finSupp (0g‘(Scalar‘𝑀))) → (𝑥 = (𝑓( linC ‘𝑀)𝑉) → (((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) ∧ 𝑥 ∈ (Base‘𝑀)) → 𝑥𝑆)))
2827impr 458 . . . . . 6 ((𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑓 finSupp (0g‘(Scalar‘𝑀)) ∧ 𝑥 = (𝑓( linC ‘𝑀)𝑉))) → (((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) ∧ 𝑥 ∈ (Base‘𝑀)) → 𝑥𝑆))
2928rexlimiva 3267 . . . . 5 (∃𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑓 finSupp (0g‘(Scalar‘𝑀)) ∧ 𝑥 = (𝑓( linC ‘𝑀)𝑉)) → (((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) ∧ 𝑥 ∈ (Base‘𝑀)) → 𝑥𝑆))
3029com12 32 . . . 4 (((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) ∧ 𝑥 ∈ (Base‘𝑀)) → (∃𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑓 finSupp (0g‘(Scalar‘𝑀)) ∧ 𝑥 = (𝑓( linC ‘𝑀)𝑉)) → 𝑥𝑆))
3130expimpd 457 . . 3 ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) → ((𝑥 ∈ (Base‘𝑀) ∧ ∃𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑓 finSupp (0g‘(Scalar‘𝑀)) ∧ 𝑥 = (𝑓( linC ‘𝑀)𝑉))) → 𝑥𝑆))
3219, 31sylbid 243 . 2 ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) → (𝑥 ∈ (𝑀 LinCo 𝑉) → 𝑥𝑆))
3332ralrimiv 3169 1 ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉𝑆) → ∀𝑥 ∈ (𝑀 LinCo 𝑉)𝑥𝑆)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115  ∀wral 3126  ∃wrex 3127  Vcvv 3471   ⊆ wss 3910  𝒫 cpw 4512   class class class wbr 5039  ‘cfv 6328  (class class class)co 7130   ↑m cmap 8381   finSupp cfsupp 8809  Basecbs 16462  Scalarcsca 16547  0gc0g 16692  LModclmod 19610  LSubSpclss 19679   linC clinc 44635   LinCo clinco 44636 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-rep 5163  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-cnex 10570  ax-resscn 10571  ax-1cn 10572  ax-icn 10573  ax-addcl 10574  ax-addrcl 10575  ax-mulcl 10576  ax-mulrcl 10577  ax-mulcom 10578  ax-addass 10579  ax-mulass 10580  ax-distr 10581  ax-i2m1 10582  ax-1ne0 10583  ax-1rid 10584  ax-rnegex 10585  ax-rrecex 10586  ax-cnre 10587  ax-pre-lttri 10588  ax-pre-lttrn 10589  ax-pre-ltadd 10590  ax-pre-mulgt0 10591 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-nel 3112  df-ral 3131  df-rex 3132  df-reu 3133  df-rmo 3134  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-uni 4812  df-int 4850  df-iun 4894  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-se 5488  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7088  df-ov 7133  df-oprab 7134  df-mpo 7135  df-om 7556  df-1st 7664  df-2nd 7665  df-supp 7806  df-wrecs 7922  df-recs 7983  df-rdg 8021  df-1o 8077  df-oadd 8081  df-er 8264  df-map 8383  df-en 8485  df-dom 8486  df-sdom 8487  df-fin 8488  df-fsupp 8810  df-oi 8950  df-card 9344  df-pnf 10654  df-mnf 10655  df-xr 10656  df-ltxr 10657  df-le 10658  df-sub 10849  df-neg 10850  df-nn 11616  df-2 11678  df-n0 11876  df-z 11960  df-uz 12222  df-fz 12876  df-fzo 13017  df-seq 13353  df-hash 13675  df-ndx 16465  df-slot 16466  df-base 16468  df-sets 16469  df-ress 16470  df-plusg 16557  df-0g 16694  df-gsum 16695  df-mgm 17831  df-sgrp 17880  df-mnd 17891  df-submnd 17936  df-grp 18085  df-minusg 18086  df-sbg 18087  df-subg 18255  df-cntz 18426  df-cmn 18887  df-abl 18888  df-mgp 19219  df-ur 19231  df-ring 19278  df-lmod 19612  df-lss 19680  df-linc 44637  df-lco 44638 This theorem is referenced by:  lcosslsp  44669
 Copyright terms: Public domain W3C validator