Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > plyun0 | Structured version Visualization version GIF version |
Description: The set of polynomials is unaffected by the addition of zero. (This is built into the definition because all higher powers of a polynomial are effectively zero, so we require that the coefficient field contain zero to simplify some of our closure theorems.) (Contributed by Mario Carneiro, 17-Jul-2014.) |
Ref | Expression |
---|---|
plyun0 | ⊢ (Poly‘(𝑆 ∪ {0})) = (Poly‘𝑆) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0cn 10711 | . . . . . . 7 ⊢ 0 ∈ ℂ | |
2 | snssi 4696 | . . . . . . 7 ⊢ (0 ∈ ℂ → {0} ⊆ ℂ) | |
3 | 1, 2 | ax-mp 5 | . . . . . 6 ⊢ {0} ⊆ ℂ |
4 | 3 | biantru 533 | . . . . 5 ⊢ (𝑆 ⊆ ℂ ↔ (𝑆 ⊆ ℂ ∧ {0} ⊆ ℂ)) |
5 | unss 4074 | . . . . 5 ⊢ ((𝑆 ⊆ ℂ ∧ {0} ⊆ ℂ) ↔ (𝑆 ∪ {0}) ⊆ ℂ) | |
6 | 4, 5 | bitr2i 279 | . . . 4 ⊢ ((𝑆 ∪ {0}) ⊆ ℂ ↔ 𝑆 ⊆ ℂ) |
7 | unass 4056 | . . . . . . . 8 ⊢ ((𝑆 ∪ {0}) ∪ {0}) = (𝑆 ∪ ({0} ∪ {0})) | |
8 | unidm 4042 | . . . . . . . . 9 ⊢ ({0} ∪ {0}) = {0} | |
9 | 8 | uneq2i 4050 | . . . . . . . 8 ⊢ (𝑆 ∪ ({0} ∪ {0})) = (𝑆 ∪ {0}) |
10 | 7, 9 | eqtri 2761 | . . . . . . 7 ⊢ ((𝑆 ∪ {0}) ∪ {0}) = (𝑆 ∪ {0}) |
11 | 10 | oveq1i 7180 | . . . . . 6 ⊢ (((𝑆 ∪ {0}) ∪ {0}) ↑m ℕ0) = ((𝑆 ∪ {0}) ↑m ℕ0) |
12 | 11 | rexeqi 3315 | . . . . 5 ⊢ (∃𝑎 ∈ (((𝑆 ∪ {0}) ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ↔ ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
13 | 12 | rexbii 3161 | . . . 4 ⊢ (∃𝑛 ∈ ℕ0 ∃𝑎 ∈ (((𝑆 ∪ {0}) ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ↔ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
14 | 6, 13 | anbi12i 630 | . . 3 ⊢ (((𝑆 ∪ {0}) ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ (((𝑆 ∪ {0}) ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
15 | elply 24944 | . . 3 ⊢ (𝑓 ∈ (Poly‘(𝑆 ∪ {0})) ↔ ((𝑆 ∪ {0}) ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ (((𝑆 ∪ {0}) ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) | |
16 | elply 24944 | . . 3 ⊢ (𝑓 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) | |
17 | 14, 15, 16 | 3bitr4i 306 | . 2 ⊢ (𝑓 ∈ (Poly‘(𝑆 ∪ {0})) ↔ 𝑓 ∈ (Poly‘𝑆)) |
18 | 17 | eqriv 2735 | 1 ⊢ (Poly‘(𝑆 ∪ {0})) = (Poly‘𝑆) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 399 = wceq 1542 ∈ wcel 2114 ∃wrex 3054 ∪ cun 3841 ⊆ wss 3843 {csn 4516 ↦ cmpt 5110 ‘cfv 6339 (class class class)co 7170 ↑m cmap 8437 ℂcc 10613 0cc0 10615 · cmul 10620 ℕ0cn0 11976 ...cfz 12981 ↑cexp 13521 Σcsu 15135 Polycply 24933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pr 5296 ax-un 7479 ax-cnex 10671 ax-1cn 10673 ax-icn 10674 ax-addcl 10675 ax-mulcl 10677 ax-i2m1 10683 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-ral 3058 df-rex 3059 df-reu 3060 df-rab 3062 df-v 3400 df-sbc 3681 df-csb 3791 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-pss 3862 df-nul 4212 df-if 4415 df-pw 4490 df-sn 4517 df-pr 4519 df-tp 4521 df-op 4523 df-uni 4797 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5429 df-eprel 5434 df-po 5442 df-so 5443 df-fr 5483 df-we 5485 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-pred 6129 df-ord 6175 df-on 6176 df-lim 6177 df-suc 6178 df-iota 6297 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-ov 7173 df-om 7600 df-wrecs 7976 df-recs 8037 df-rdg 8075 df-nn 11717 df-n0 11977 df-ply 24937 |
This theorem is referenced by: elplyd 24951 ply1term 24953 ply0 24957 plyaddlem 24964 plymullem 24965 plyco 24990 plycj 25026 |
Copyright terms: Public domain | W3C validator |