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 } ) ↑m0 ) = ( ( 𝑆 ∪ { 0 } ) ↑m0 )
12 11 rexeqi ( ∃ 𝑎 ∈ ( ( ( 𝑆 ∪ { 0 } ) ∪ { 0 } ) ↑m0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ↔ ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) )
13 12 rexbii ( ∃ 𝑛 ∈ ℕ0𝑎 ∈ ( ( ( 𝑆 ∪ { 0 } ) ∪ { 0 } ) ↑m0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ↔ ∃ 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) )
14 6 13 anbi12i ( ( ( 𝑆 ∪ { 0 } ) ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0𝑎 ∈ ( ( ( 𝑆 ∪ { 0 } ) ∪ { 0 } ) ↑m0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
15 elply ( 𝑓 ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) ↔ ( ( 𝑆 ∪ { 0 } ) ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0𝑎 ∈ ( ( ( 𝑆 ∪ { 0 } ) ∪ { 0 } ) ↑m0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
16 elply ( 𝑓 ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
17 14 15 16 3bitr4i ( 𝑓 ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) ↔ 𝑓 ∈ ( Poly ‘ 𝑆 ) )
18 17 eqriv ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) = ( Poly ‘ 𝑆 )