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 
|- P = ( z e. CC |-> sum_ k e. ( 0 ... 1 ) ( ( C ` k ) x. ( z ^ k ) ) )
linplyfv2.c 
|- C = ( x e. NN0 |-> if ( x = 0 , A , B ) )
Assertion linply2cfv 
|- ( ( S C_ CC /\ ( A e. S /\ B e. S ) /\ X e. CC ) -> ( P ` X ) = ( A + ( B x. X ) ) )

Proof

Step Hyp Ref Expression
1 linplyfv.p 
 |-  P = ( z e. CC |-> sum_ k e. ( 0 ... 1 ) ( ( C ` k ) x. ( z ^ k ) ) )
2 linplyfv2.c 
 |-  C = ( x e. NN0 |-> if ( x = 0 , A , B ) )
3 cnex 
 |-  CC e. _V
4 3 ssex 
 |-  ( S C_ CC -> S e. _V )
5 4 3ad2ant1 
 |-  ( ( S C_ CC /\ ( A e. S /\ B e. S ) /\ X e. CC ) -> S e. _V )
6 nn0ex 
 |-  NN0 e. _V
7 6 a1i 
 |-  ( ( S C_ CC /\ ( A e. S /\ B e. S ) /\ X e. CC ) -> NN0 e. _V )
8 ifcl 
 |-  ( ( A e. S /\ B e. S ) -> if ( x = 0 , A , B ) e. S )
9 8 3ad2ant2 
 |-  ( ( S C_ CC /\ ( A e. S /\ B e. S ) /\ X e. CC ) -> if ( x = 0 , A , B ) e. S )
10 9 adantr 
 |-  ( ( ( S C_ CC /\ ( A e. S /\ B e. S ) /\ X e. CC ) /\ x e. NN0 ) -> if ( x = 0 , A , B ) e. S )
11 10 2 fmptd 
 |-  ( ( S C_ CC /\ ( A e. S /\ B e. S ) /\ X e. CC ) -> C : NN0 --> S )
12 5 7 11 elmapdd 
 |-  ( ( S C_ CC /\ ( A e. S /\ B e. S ) /\ X e. CC ) -> C e. ( S ^m NN0 ) )
13 1 linplyfv 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( P ` X ) = ( ( C ` 0 ) + ( ( C ` 1 ) x. X ) ) )
14 12 13 syld3an2 
 |-  ( ( S C_ CC /\ ( A e. S /\ B e. S ) /\ X e. CC ) -> ( P ` X ) = ( ( C ` 0 ) + ( ( C ` 1 ) x. X ) ) )
15 2 a1i 
 |-  ( ( S C_ CC /\ ( A e. S /\ B e. S ) ) -> C = ( x e. NN0 |-> if ( x = 0 , A , B ) ) )
16 iftrue 
 |-  ( x = 0 -> if ( x = 0 , A , B ) = A )
17 16 adantl 
 |-  ( ( ( S C_ CC /\ ( A e. S /\ B e. S ) ) /\ x = 0 ) -> if ( x = 0 , A , B ) = A )
18 0nn0 
 |-  0 e. NN0
19 18 a1i 
 |-  ( ( S C_ CC /\ ( A e. S /\ B e. S ) ) -> 0 e. NN0 )
20 simprl 
 |-  ( ( S C_ CC /\ ( A e. S /\ B e. S ) ) -> A e. S )
21 15 17 19 20 fvmptd 
 |-  ( ( S C_ CC /\ ( A e. S /\ B e. S ) ) -> ( C ` 0 ) = A )
22 ax-1ne0 
 |-  1 =/= 0
23 22 neii 
 |-  -. 1 = 0
24 eqeq1 
 |-  ( x = 1 -> ( x = 0 <-> 1 = 0 ) )
25 23 24 mtbiri 
 |-  ( x = 1 -> -. x = 0 )
26 25 adantl 
 |-  ( ( ( S C_ CC /\ ( A e. S /\ B e. S ) ) /\ x = 1 ) -> -. x = 0 )
27 26 iffalsed 
 |-  ( ( ( S C_ CC /\ ( A e. S /\ B e. S ) ) /\ x = 1 ) -> if ( x = 0 , A , B ) = B )
28 1nn0 
 |-  1 e. NN0
29 28 a1i 
 |-  ( ( S C_ CC /\ ( A e. S /\ B e. S ) ) -> 1 e. NN0 )
30 simprr 
 |-  ( ( S C_ CC /\ ( A e. S /\ B e. S ) ) -> B e. S )
31 15 27 29 30 fvmptd 
 |-  ( ( S C_ CC /\ ( A e. S /\ B e. S ) ) -> ( C ` 1 ) = B )
32 31 oveq1d 
 |-  ( ( S C_ CC /\ ( A e. S /\ B e. S ) ) -> ( ( C ` 1 ) x. X ) = ( B x. X ) )
33 21 32 oveq12d 
 |-  ( ( S C_ CC /\ ( A e. S /\ B e. S ) ) -> ( ( C ` 0 ) + ( ( C ` 1 ) x. X ) ) = ( A + ( B x. X ) ) )
34 33 3adant3 
 |-  ( ( S C_ CC /\ ( A e. S /\ B e. S ) /\ X e. CC ) -> ( ( C ` 0 ) + ( ( C ` 1 ) x. X ) ) = ( A + ( B x. X ) ) )
35 14 34 eqtrd 
 |-  ( ( S C_ CC /\ ( A e. S /\ B e. S ) /\ X e. CC ) -> ( P ` X ) = ( A + ( B x. X ) ) )