Metamath Proof Explorer

Theorem linply2cfv

Description: The evaluation of a linear polynomial over a subset of the complex numbers with explicit coefficients at a complex number. (Contributed by AV, 31-Oct-2026)

Ref Expression
Hypotheses linplyfv.p ⊢ 𝑃 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
linplyfv2.c ⊢ 𝐶 = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝐴 , 𝐵 ) )
Assertion linply2cfv ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝑋 ∈ ℂ ) → ( 𝑃 ‘ 𝑋 ) = ( 𝐴 + ( 𝐵 · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 linplyfv.p ⊢ 𝑃 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 𝐶 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
2 linplyfv2.c ⊢ 𝐶 = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝐴 , 𝐵 ) )
3 cnex ⊢ ℂ ∈ V
4 3 ssex ⊢ ( 𝑆 ⊆ ℂ → 𝑆 ∈ V )
5 4 3ad2ant1 ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝑋 ∈ ℂ ) → 𝑆 ∈ V )
6 nn0ex ⊢ ℕ0 ∈ V
7 6 a1i ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝑋 ∈ ℂ ) → ℕ0 ∈ V )
8 ifcl ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → if ( 𝑥 = 0 , 𝐴 , 𝐵 ) ∈ 𝑆 )
9 8 3ad2ant2 ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝑋 ∈ ℂ ) → if ( 𝑥 = 0 , 𝐴 , 𝐵 ) ∈ 𝑆 )
10 9 adantr ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝑋 ∈ ℂ ) ∧ 𝑥 ∈ ℕ0 ) → if ( 𝑥 = 0 , 𝐴 , 𝐵 ) ∈ 𝑆 )
11 10 2 fmptd ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝑋 ∈ ℂ ) → 𝐶 : ℕ0 ⟶ 𝑆 )
12 5 7 11 elmapdd ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝑋 ∈ ℂ ) → 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) )
13 1 linplyfv ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐶 ∈ ( 𝑆 ↑m ℕ0 ) ∧ 𝑋 ∈ ℂ ) → ( 𝑃 ‘ 𝑋 ) = ( ( 𝐶 ‘ 0 ) + ( ( 𝐶 ‘ 1 ) · 𝑋 ) ) )
14 12 13 syld3an2 ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝑋 ∈ ℂ ) → ( 𝑃 ‘ 𝑋 ) = ( ( 𝐶 ‘ 0 ) + ( ( 𝐶 ‘ 1 ) · 𝑋 ) ) )
15 2 a1i ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → 𝐶 = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝐴 , 𝐵 ) ) )
16 iftrue ⊢ ( 𝑥 = 0 → if ( 𝑥 = 0 , 𝐴 , 𝐵 ) = 𝐴 )
17 16 adantl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) ∧ 𝑥 = 0 ) → if ( 𝑥 = 0 , 𝐴 , 𝐵 ) = 𝐴 )
18 0nn0 ⊢ 0 ∈ ℕ0
19 18 a1i ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → 0 ∈ ℕ0 )
20 simprl ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → 𝐴 ∈ 𝑆 )
21 15 17 19 20 fvmptd ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐶 ‘ 0 ) = 𝐴 )
22 ax-1ne0 ⊢ 1 ≠ 0
23 22 neii ⊢ ¬ 1 = 0
24 eqeq1 ⊢ ( 𝑥 = 1 → ( 𝑥 = 0 ↔ 1 = 0 ) )
25 23 24 mtbiri ⊢ ( 𝑥 = 1 → ¬ 𝑥 = 0 )
26 25 adantl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) ∧ 𝑥 = 1 ) → ¬ 𝑥 = 0 )
27 26 iffalsed ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) ∧ 𝑥 = 1 ) → if ( 𝑥 = 0 , 𝐴 , 𝐵 ) = 𝐵 )
28 1nn0 ⊢ 1 ∈ ℕ0
29 28 a1i ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → 1 ∈ ℕ0 )
30 simprr ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → 𝐵 ∈ 𝑆 )
31 15 27 29 30 fvmptd ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐶 ‘ 1 ) = 𝐵 )
32 31 oveq1d ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( ( 𝐶 ‘ 1 ) · 𝑋 ) = ( 𝐵 · 𝑋 ) )
33 21 32 oveq12d ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( ( 𝐶 ‘ 0 ) + ( ( 𝐶 ‘ 1 ) · 𝑋 ) ) = ( 𝐴 + ( 𝐵 · 𝑋 ) ) )
34 33 3adant3 ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝑋 ∈ ℂ ) → ( ( 𝐶 ‘ 0 ) + ( ( 𝐶 ‘ 1 ) · 𝑋 ) ) = ( 𝐴 + ( 𝐵 · 𝑋 ) ) )
35 14 34 eqtrd ⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝑋 ∈ ℂ ) → ( 𝑃 ‘ 𝑋 ) = ( 𝐴 + ( 𝐵 · 𝑋 ) ) )