Metamath Proof Explorer

Theorem linplyfv

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

Ref Expression
Hypothesis linplyfv.p 
|- P = ( z e. CC |-> sum_ k e. ( 0 ... 1 ) ( ( C ` k ) x. ( z ^ k ) ) )
Assertion linplyfv 
|- ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( P ` X ) = ( ( C ` 0 ) + ( ( C ` 1 ) 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 1 a1i 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> P = ( z e. CC |-> sum_ k e. ( 0 ... 1 ) ( ( C ` k ) x. ( z ^ k ) ) ) )
3 oveq1 
 |-  ( z = X -> ( z ^ k ) = ( X ^ k ) )
4 3 oveq2d 
 |-  ( z = X -> ( ( C ` k ) x. ( z ^ k ) ) = ( ( C ` k ) x. ( X ^ k ) ) )
5 4 a1d 
 |-  ( z = X -> ( k e. ( 0 ... 1 ) -> ( ( C ` k ) x. ( z ^ k ) ) = ( ( C ` k ) x. ( X ^ k ) ) ) )
6 5 ralrimiv 
 |-  ( z = X -> A. k e. ( 0 ... 1 ) ( ( C ` k ) x. ( z ^ k ) ) = ( ( C ` k ) x. ( X ^ k ) ) )
7 6 sumeq2d 
 |-  ( z = X -> sum_ k e. ( 0 ... 1 ) ( ( C ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... 1 ) ( ( C ` k ) x. ( X ^ k ) ) )
8 fz01pr 
 |-  ( 0 ... 1 ) = { 0 , 1 }
9 8 sumeq1i 
 |-  sum_ k e. ( 0 ... 1 ) ( ( C ` k ) x. ( X ^ k ) ) = sum_ k e. { 0 , 1 } ( ( C ` k ) x. ( X ^ k ) )
10 fveq2 
 |-  ( k = 0 -> ( C ` k ) = ( C ` 0 ) )
11 oveq2 
 |-  ( k = 0 -> ( X ^ k ) = ( X ^ 0 ) )
12 10 11 oveq12d 
 |-  ( k = 0 -> ( ( C ` k ) x. ( X ^ k ) ) = ( ( C ` 0 ) x. ( X ^ 0 ) ) )
13 fveq2 
 |-  ( k = 1 -> ( C ` k ) = ( C ` 1 ) )
14 oveq2 
 |-  ( k = 1 -> ( X ^ k ) = ( X ^ 1 ) )
15 13 14 oveq12d 
 |-  ( k = 1 -> ( ( C ` k ) x. ( X ^ k ) ) = ( ( C ` 1 ) x. ( X ^ 1 ) ) )
16 cnex 
 |-  CC e. _V
17 simp1 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> S C_ CC )
18 mapss 
 |-  ( ( CC e. _V /\ S C_ CC ) -> ( S ^m NN0 ) C_ ( CC ^m NN0 ) )
19 16 17 18 sylancr 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( S ^m NN0 ) C_ ( CC ^m NN0 ) )
20 simp2 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> C e. ( S ^m NN0 ) )
21 19 20 sseldd 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> C e. ( CC ^m NN0 ) )
22 21 elmaprd 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> C : NN0 --> CC )
23 0nn0 
 |-  0 e. NN0
24 23 a1i 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> 0 e. NN0 )
25 22 24 ffvelcdmd 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( C ` 0 ) e. CC )
26 id 
 |-  ( X e. CC -> X e. CC )
27 23 a1i 
 |-  ( X e. CC -> 0 e. NN0 )
28 26 27 expcld 
 |-  ( X e. CC -> ( X ^ 0 ) e. CC )
29 28 3ad2ant3 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( X ^ 0 ) e. CC )
30 25 29 mulcld 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( ( C ` 0 ) x. ( X ^ 0 ) ) e. CC )
31 1nn0 
 |-  1 e. NN0
32 31 a1i 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> 1 e. NN0 )
33 22 32 ffvelcdmd 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( C ` 1 ) e. CC )
34 31 a1i 
 |-  ( X e. CC -> 1 e. NN0 )
35 26 34 expcld 
 |-  ( X e. CC -> ( X ^ 1 ) e. CC )
36 35 3ad2ant3 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( X ^ 1 ) e. CC )
37 33 36 mulcld 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( ( C ` 1 ) x. ( X ^ 1 ) ) e. CC )
38 30 37 jca 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( ( ( C ` 0 ) x. ( X ^ 0 ) ) e. CC /\ ( ( C ` 1 ) x. ( X ^ 1 ) ) e. CC ) )
39 0z 
 |-  0 e. ZZ
40 1z 
 |-  1 e. ZZ
41 39 40 pm3.2i 
 |-  ( 0 e. ZZ /\ 1 e. ZZ )
42 41 a1i 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( 0 e. ZZ /\ 1 e. ZZ ) )
43 0ne1 
 |-  0 =/= 1
44 43 a1i 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> 0 =/= 1 )
45 12 15 38 42 44 sumpr 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> sum_ k e. { 0 , 1 } ( ( C ` k ) x. ( X ^ k ) ) = ( ( ( C ` 0 ) x. ( X ^ 0 ) ) + ( ( C ` 1 ) x. ( X ^ 1 ) ) ) )
46 exp0 
 |-  ( X e. CC -> ( X ^ 0 ) = 1 )
47 46 3ad2ant3 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( X ^ 0 ) = 1 )
48 47 oveq2d 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( ( C ` 0 ) x. ( X ^ 0 ) ) = ( ( C ` 0 ) x. 1 ) )
49 25 mulridd 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( ( C ` 0 ) x. 1 ) = ( C ` 0 ) )
50 48 49 eqtrd 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( ( C ` 0 ) x. ( X ^ 0 ) ) = ( C ` 0 ) )
51 exp1 
 |-  ( X e. CC -> ( X ^ 1 ) = X )
52 51 3ad2ant3 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( X ^ 1 ) = X )
53 52 oveq2d 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( ( C ` 1 ) x. ( X ^ 1 ) ) = ( ( C ` 1 ) x. X ) )
54 50 53 oveq12d 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( ( ( C ` 0 ) x. ( X ^ 0 ) ) + ( ( C ` 1 ) x. ( X ^ 1 ) ) ) = ( ( C ` 0 ) + ( ( C ` 1 ) x. X ) ) )
55 45 54 eqtrd 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> sum_ k e. { 0 , 1 } ( ( C ` k ) x. ( X ^ k ) ) = ( ( C ` 0 ) + ( ( C ` 1 ) x. X ) ) )
56 9 55 eqtrid 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> sum_ k e. ( 0 ... 1 ) ( ( C ` k ) x. ( X ^ k ) ) = ( ( C ` 0 ) + ( ( C ` 1 ) x. X ) ) )
57 7 56 sylan9eqr 
 |-  ( ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) /\ z = X ) -> sum_ k e. ( 0 ... 1 ) ( ( C ` k ) x. ( z ^ k ) ) = ( ( C ` 0 ) + ( ( C ` 1 ) x. X ) ) )
58 simp3 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> X e. CC )
59 ovexd 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( ( C ` 0 ) + ( ( C ` 1 ) x. X ) ) e. _V )
60 2 57 58 59 fvmptd 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) /\ X e. CC ) -> ( P ` X ) = ( ( C ` 0 ) + ( ( C ` 1 ) x. X ) ) )