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

Metamath Proof Explorer

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