Theorem elply

Description: Definition of a polynomial with coefficients in S . (Contributed by Mario Carneiro, 17-Jul-2014)

	Ref	Expression
Assertion	elply	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		plybss	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ⊆ ℂ )
2		plyval	⊢ ( 𝑆 ⊆ ℂ → ( Poly ‘ 𝑆 ) = { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } )
3	2	eleq2d	⊢ ( 𝑆 ⊆ ℂ → ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ↔ 𝐹 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } ) )
4		id	⊢ ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
5		cnex	⊢ ℂ ∈ V
6	5	mptex	⊢ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ V
7	4 6	eqeltrdi	⊢ ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → 𝐹 ∈ V )
8	7	a1i	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ) → ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → 𝐹 ∈ V ) )
9	8	rexlimivv	⊢ ( ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → 𝐹 ∈ V )
10		eqeq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
11	10	2rexbidv	⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
12	9 11	elab3	⊢ ( 𝐹 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } ↔ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
13	3 12	bitrdi	⊢ ( 𝑆 ⊆ ℂ → ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ↔ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
14	1 13	biadanii	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )