Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  plyss Structured version   Visualization version   GIF version

Theorem plyss 24507
 Description: The polynomial set function preserves the subset relation. (Contributed by Mario Carneiro, 17-Jul-2014.)
Assertion
Ref Expression
plyss ((𝑆𝑇𝑇 ⊆ ℂ) → (Poly‘𝑆) ⊆ (Poly‘𝑇))

Proof of Theorem plyss
Dummy variables 𝑘 𝑎 𝑛 𝑧 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 477 . . . . . . . 8 ((𝑆𝑇𝑇 ⊆ ℂ) → 𝑇 ⊆ ℂ)
2 cnex 10414 . . . . . . . 8 ℂ ∈ V
3 ssexg 5079 . . . . . . . 8 ((𝑇 ⊆ ℂ ∧ ℂ ∈ V) → 𝑇 ∈ V)
41, 2, 3sylancl 578 . . . . . . 7 ((𝑆𝑇𝑇 ⊆ ℂ) → 𝑇 ∈ V)
5 snex 5184 . . . . . . 7 {0} ∈ V
6 unexg 7287 . . . . . . 7 ((𝑇 ∈ V ∧ {0} ∈ V) → (𝑇 ∪ {0}) ∈ V)
74, 5, 6sylancl 578 . . . . . 6 ((𝑆𝑇𝑇 ⊆ ℂ) → (𝑇 ∪ {0}) ∈ V)
8 unss1 4037 . . . . . . 7 (𝑆𝑇 → (𝑆 ∪ {0}) ⊆ (𝑇 ∪ {0}))
98adantr 473 . . . . . 6 ((𝑆𝑇𝑇 ⊆ ℂ) → (𝑆 ∪ {0}) ⊆ (𝑇 ∪ {0}))
10 mapss 8249 . . . . . 6 (((𝑇 ∪ {0}) ∈ V ∧ (𝑆 ∪ {0}) ⊆ (𝑇 ∪ {0})) → ((𝑆 ∪ {0}) ↑𝑚0) ⊆ ((𝑇 ∪ {0}) ↑𝑚0))
117, 9, 10syl2anc 576 . . . . 5 ((𝑆𝑇𝑇 ⊆ ℂ) → ((𝑆 ∪ {0}) ↑𝑚0) ⊆ ((𝑇 ∪ {0}) ↑𝑚0))
12 ssrexv 3917 . . . . 5 (((𝑆 ∪ {0}) ↑𝑚0) ⊆ ((𝑇 ∪ {0}) ↑𝑚0) → (∃𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) → ∃𝑎 ∈ ((𝑇 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))))
1311, 12syl 17 . . . 4 ((𝑆𝑇𝑇 ⊆ ℂ) → (∃𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) → ∃𝑎 ∈ ((𝑇 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))))
1413reximdv 3211 . . 3 ((𝑆𝑇𝑇 ⊆ ℂ) → (∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))) → ∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑇 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))))
1514ss2abdv 3927 . 2 ((𝑆𝑇𝑇 ⊆ ℂ) → {𝑓 ∣ ∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))} ⊆ {𝑓 ∣ ∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑇 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))})
16 sstr 3859 . . 3 ((𝑆𝑇𝑇 ⊆ ℂ) → 𝑆 ⊆ ℂ)
17 plyval 24501 . . 3 (𝑆 ⊆ ℂ → (Poly‘𝑆) = {𝑓 ∣ ∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))})
1816, 17syl 17 . 2 ((𝑆𝑇𝑇 ⊆ ℂ) → (Poly‘𝑆) = {𝑓 ∣ ∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))})
19 plyval 24501 . . 3 (𝑇 ⊆ ℂ → (Poly‘𝑇) = {𝑓 ∣ ∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑇 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))})
2019adantl 474 . 2 ((𝑆𝑇𝑇 ⊆ ℂ) → (Poly‘𝑇) = {𝑓 ∣ ∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑇 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))})
2115, 18, 203sstr4d 3897 1 ((𝑆𝑇𝑇 ⊆ ℂ) → (Poly‘𝑆) ⊆ (Poly‘𝑇))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 387   = wceq 1508   ∈ wcel 2051  {cab 2751  ∃wrex 3082  Vcvv 3408   ∪ cun 3820   ⊆ wss 3822  {csn 4435   ↦ cmpt 5004  ‘cfv 6185  (class class class)co 6974   ↑𝑚 cmap 8204  ℂcc 10331  0cc0 10333   · cmul 10338  ℕ0cn0 11705  ...cfz 12706  ↑cexp 13242  Σcsu 14901  Polycply 24492 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2743  ax-rep 5045  ax-sep 5056  ax-nul 5063  ax-pow 5115  ax-pr 5182  ax-un 7277  ax-cnex 10389  ax-1cn 10391  ax-addcl 10393 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-ne 2961  df-ral 3086  df-rex 3087  df-reu 3088  df-rab 3090  df-v 3410  df-sbc 3675  df-csb 3780  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-pss 3838  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4709  df-iun 4790  df-br 4926  df-opab 4988  df-mpt 5005  df-tr 5027  df-id 5308  df-eprel 5313  df-po 5322  df-so 5323  df-fr 5362  df-we 5364  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-res 5415  df-ima 5416  df-pred 5983  df-ord 6029  df-on 6030  df-lim 6031  df-suc 6032  df-iota 6149  df-fun 6187  df-fn 6188  df-f 6189  df-f1 6190  df-fo 6191  df-f1o 6192  df-fv 6193  df-ov 6977  df-oprab 6978  df-mpo 6979  df-om 7395  df-1st 7499  df-2nd 7500  df-wrecs 7748  df-recs 7810  df-rdg 7848  df-map 8206  df-nn 11438  df-n0 11706  df-ply 24496 This theorem is referenced by:  plyssc  24508  elqaa  24629  aacjcl  24634  aalioulem3  24641  itgoss  39197  cnsrplycl  39201
 Copyright terms: Public domain W3C validator