This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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