Step |
Hyp |
Ref |
Expression |
1 |
|
0cn |
⊢ 0 ∈ ℂ |
2 |
|
snssi |
⊢ ( 0 ∈ ℂ → { 0 } ⊆ ℂ ) |
3 |
1 2
|
ax-mp |
⊢ { 0 } ⊆ ℂ |
4 |
3
|
biantru |
⊢ ( 𝑆 ⊆ ℂ ↔ ( 𝑆 ⊆ ℂ ∧ { 0 } ⊆ ℂ ) ) |
5 |
|
unss |
⊢ ( ( 𝑆 ⊆ ℂ ∧ { 0 } ⊆ ℂ ) ↔ ( 𝑆 ∪ { 0 } ) ⊆ ℂ ) |
6 |
4 5
|
bitr2i |
⊢ ( ( 𝑆 ∪ { 0 } ) ⊆ ℂ ↔ 𝑆 ⊆ ℂ ) |
7 |
|
unass |
⊢ ( ( 𝑆 ∪ { 0 } ) ∪ { 0 } ) = ( 𝑆 ∪ ( { 0 } ∪ { 0 } ) ) |
8 |
|
unidm |
⊢ ( { 0 } ∪ { 0 } ) = { 0 } |
9 |
8
|
uneq2i |
⊢ ( 𝑆 ∪ ( { 0 } ∪ { 0 } ) ) = ( 𝑆 ∪ { 0 } ) |
10 |
7 9
|
eqtri |
⊢ ( ( 𝑆 ∪ { 0 } ) ∪ { 0 } ) = ( 𝑆 ∪ { 0 } ) |
11 |
10
|
oveq1i |
⊢ ( ( ( 𝑆 ∪ { 0 } ) ∪ { 0 } ) ↑m ℕ0 ) = ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) |
12 |
11
|
rexeqi |
⊢ ( ∃ 𝑎 ∈ ( ( ( 𝑆 ∪ { 0 } ) ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
13 |
12
|
rexbii |
⊢ ( ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( ( 𝑆 ∪ { 0 } ) ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
14 |
6 13
|
anbi12i |
⊢ ( ( ( 𝑆 ∪ { 0 } ) ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( ( 𝑆 ∪ { 0 } ) ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) |
15 |
|
elply |
⊢ ( 𝑓 ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) ↔ ( ( 𝑆 ∪ { 0 } ) ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( ( 𝑆 ∪ { 0 } ) ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) |
16 |
|
elply |
⊢ ( 𝑓 ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) |
17 |
14 15 16
|
3bitr4i |
⊢ ( 𝑓 ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) ↔ 𝑓 ∈ ( Poly ‘ 𝑆 ) ) |
18 |
17
|
eqriv |
⊢ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) = ( Poly ‘ 𝑆 ) |