Metamath Proof Explorer


Theorem ply1term

Description: A one-term polynomial. (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Hypothesis ply1term.1 𝐹 = ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧𝑁 ) ) )
Assertion ply1term ( ( 𝑆 ⊆ ℂ ∧ 𝐴𝑆𝑁 ∈ ℕ0 ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 ply1term.1 𝐹 = ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧𝑁 ) ) )
2 ssel2 ( ( 𝑆 ⊆ ℂ ∧ 𝐴𝑆 ) → 𝐴 ∈ ℂ )
3 1 ply1termlem ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧𝑘 ) ) ) )
4 2 3 stoic3 ( ( 𝑆 ⊆ ℂ ∧ 𝐴𝑆𝑁 ∈ ℕ0 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧𝑘 ) ) ) )
5 simp1 ( ( 𝑆 ⊆ ℂ ∧ 𝐴𝑆𝑁 ∈ ℕ0 ) → 𝑆 ⊆ ℂ )
6 0cnd ( ( 𝑆 ⊆ ℂ ∧ 𝐴𝑆𝑁 ∈ ℕ0 ) → 0 ∈ ℂ )
7 6 snssd ( ( 𝑆 ⊆ ℂ ∧ 𝐴𝑆𝑁 ∈ ℕ0 ) → { 0 } ⊆ ℂ )
8 5 7 unssd ( ( 𝑆 ⊆ ℂ ∧ 𝐴𝑆𝑁 ∈ ℕ0 ) → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
9 simp3 ( ( 𝑆 ⊆ ℂ ∧ 𝐴𝑆𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
10 simpl2 ( ( ( 𝑆 ⊆ ℂ ∧ 𝐴𝑆𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴𝑆 )
11 elun1 ( 𝐴𝑆𝐴 ∈ ( 𝑆 ∪ { 0 } ) )
12 10 11 syl ( ( ( 𝑆 ⊆ ℂ ∧ 𝐴𝑆𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ( 𝑆 ∪ { 0 } ) )
13 ssun2 { 0 } ⊆ ( 𝑆 ∪ { 0 } )
14 c0ex 0 ∈ V
15 14 snss ( 0 ∈ ( 𝑆 ∪ { 0 } ) ↔ { 0 } ⊆ ( 𝑆 ∪ { 0 } ) )
16 13 15 mpbir 0 ∈ ( 𝑆 ∪ { 0 } )
17 ifcl ( ( 𝐴 ∈ ( 𝑆 ∪ { 0 } ) ∧ 0 ∈ ( 𝑆 ∪ { 0 } ) ) → if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ∈ ( 𝑆 ∪ { 0 } ) )
18 12 16 17 sylancl ( ( ( 𝑆 ⊆ ℂ ∧ 𝐴𝑆𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ∈ ( 𝑆 ∪ { 0 } ) )
19 8 9 18 elplyd ( ( 𝑆 ⊆ ℂ ∧ 𝐴𝑆𝑁 ∈ ℕ0 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧𝑘 ) ) ) ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) )
20 4 19 eqeltrd ( ( 𝑆 ⊆ ℂ ∧ 𝐴𝑆𝑁 ∈ ℕ0 ) → 𝐹 ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) )
21 plyun0 ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) = ( Poly ‘ 𝑆 )
22 20 21 eleqtrdi ( ( 𝑆 ⊆ ℂ ∧ 𝐴𝑆𝑁 ∈ ℕ0 ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )