Metamath Proof Explorer


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 } ) ↑m0 ) 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎𝑘 ) · ( 𝑧𝑘 ) ) ) ) )

Proof

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