Metamath Proof Explorer

Theorem elplyd

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

Ref Expression
Hypotheses elplyd.1 ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
elplyd.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
elplyd.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ 𝑆 )
Assertion elplyd ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 elplyd.1 ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
2 elplyd.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3 elplyd.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ 𝑆 )
4 fveq2 ⊢ ( 𝑗 = 𝑘 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑗 ) = ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑘 ) )
5 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑧 ↑ 𝑗 ) = ( 𝑧 ↑ 𝑘 ) )
6 4 5 oveq12d ⊢ ( 𝑗 = 𝑘 → ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑗 ) · ( 𝑧 ↑ 𝑗 ) ) = ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
7 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑗 )
8 nfcv ⊢ Ⅎ 𝑘 ·
9 nfcv ⊢ Ⅎ 𝑘 ( 𝑧 ↑ 𝑗 )
10 7 8 9 nfov ⊢ Ⅎ 𝑘 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑗 ) · ( 𝑧 ↑ 𝑗 ) )
11 nfcv ⊢ Ⅎ 𝑗 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) )
12 6 10 11 cbvsum ⊢ Σ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑗 ) · ( 𝑧 ↑ 𝑗 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) )
13 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
14 iftrue ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) = 𝐴 )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) = 𝐴 )
16 15 3 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ∈ 𝑆 )
17 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) )
18 17 fvmpt2 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ∈ 𝑆 ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) )
19 13 16 18 syl2an2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) )
20 19 15 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑘 ) = 𝐴 )
21 20 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) )
22 21 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) )
23 12 22 eqtrid ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑗 ) · ( 𝑧 ↑ 𝑗 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) )
24 23 mpteq2dv ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑗 ) · ( 𝑧 ↑ 𝑗 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) ) )
25 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
26 25 snssd ⊢ ( 𝜑 → { 0 } ⊆ ℂ )
27 1 26 unssd ⊢ ( 𝜑 → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
28 elun1 ⊢ ( 𝐴 ∈ 𝑆 → 𝐴 ∈ ( 𝑆 ∪ { 0 } ) )
29 3 28 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ( 𝑆 ∪ { 0 } ) )
30 29 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ( 𝑆 ∪ { 0 } ) )
31 ssun2 ⊢ { 0 } ⊆ ( 𝑆 ∪ { 0 } )
32 c0ex ⊢ 0 ∈ V
33 32 snss ⊢ ( 0 ∈ ( 𝑆 ∪ { 0 } ) ↔ { 0 } ⊆ ( 𝑆 ∪ { 0 } ) )
34 31 33 mpbir ⊢ 0 ∈ ( 𝑆 ∪ { 0 } )
35 34 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 0 ∈ ( 𝑆 ∪ { 0 } ) )
36 30 35 ifclda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ∈ ( 𝑆 ∪ { 0 } ) )
37 36 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
38 elplyr ⊢ ( ( ( 𝑆 ∪ { 0 } ) ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑗 ) · ( 𝑧 ↑ 𝑗 ) ) ) ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) )
39 27 2 37 38 syl3anc ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ... 𝑁 ) , 𝐴 , 0 ) ) ‘ 𝑗 ) · ( 𝑧 ↑ 𝑗 ) ) ) ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) )
40 24 39 eqeltrrd ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) )
41 plyun0 ⊢ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) = ( Poly ‘ 𝑆 )
42 40 41 eleqtrdi ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ 𝑆 ) )