Theorem elplyr

Description: Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Assertion	elplyr	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ 𝑆 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ 𝑆 ) → 𝑆 ⊆ ℂ )
2		simp2	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ 𝑆 ) → 𝑁 ∈ ℕ0 )
3		simp3	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ 𝑆 ) → 𝐴 : ℕ0 ⟶ 𝑆 )
4		ssun1	⊢ 𝑆 ⊆ ( 𝑆 ∪ { 0 } )
5		fss	⊢ ( ( 𝐴 : ℕ0 ⟶ 𝑆 ∧ 𝑆 ⊆ ( 𝑆 ∪ { 0 } ) ) → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
6	3 4 5	sylancl	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ 𝑆 ) → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
7		0cnd	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ 𝑆 ) → 0 ∈ ℂ )
8	7	snssd	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ 𝑆 ) → { 0 } ⊆ ℂ )
9	1 8	unssd	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ 𝑆 ) → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
10		cnex	⊢ ℂ ∈ V
11		ssexg	⊢ ( ( ( 𝑆 ∪ { 0 } ) ⊆ ℂ ∧ ℂ ∈ V ) → ( 𝑆 ∪ { 0 } ) ∈ V )
12	9 10 11	sylancl	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ 𝑆 ) → ( 𝑆 ∪ { 0 } ) ∈ V )
13		nn0ex	⊢ ℕ0 ∈ V
14		elmapg	⊢ ( ( ( 𝑆 ∪ { 0 } ) ∈ V ∧ ℕ0 ∈ V ) → ( 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
15	12 13 14	sylancl	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ 𝑆 ) → ( 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
16	6 15	mpbird	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ 𝑆 ) → 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
17		eqidd	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ 𝑆 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
18		oveq2	⊢ ( 𝑛 = 𝑁 → ( 0 ... 𝑛 ) = ( 0 ... 𝑁 ) )
19	18	sumeq1d	⊢ ( 𝑛 = 𝑁 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
20	19	mpteq2dv	⊢ ( 𝑛 = 𝑁 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
21	20	eqeq2d	⊢ ( 𝑛 = 𝑁 → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
22		fveq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) )
23	22	oveq1d	⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
24	23	sumeq2sdv	⊢ ( 𝑎 = 𝐴 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
25	24	mpteq2dv	⊢ ( 𝑎 = 𝐴 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
26	25	eqeq2d	⊢ ( 𝑎 = 𝐴 → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
27	21 26	rspc2ev	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ∧ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) → ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
28	2 16 17 27	syl3anc	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ 𝑆 ) → ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
29		elply	⊢ ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ 𝑆 ) ↔ ( 𝑆 ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
30	1 28 29	sylanbrc	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ 𝑆 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ 𝑆 ) )