Metamath Proof Explorer

Theorem plyun0

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
Assertion plyun0 ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) = ( Poly ‘ 𝑆 )

Proof

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 ‘ 𝑆 )