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