Metamath Proof Explorer

Theorem linply

Description: A linear polynomial over a subset of the complex numbers is a polynomial over the subset of the complex numbers. (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 linply 
|- ( ( S C_ CC /\ C e. ( S ^m NN0 ) ) -> P e. ( Poly ` S ) )

Proof

Step Hyp Ref Expression
1 linplyfv.p 
 |-  P = ( z e. CC |-> sum_ k e. ( 0 ... 1 ) ( ( C ` k ) x. ( z ^ k ) ) )
2 simpl 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) ) -> S C_ CC )
3 oveq2 
 |-  ( n = 1 -> ( 0 ... n ) = ( 0 ... 1 ) )
4 3 sumeq1d 
 |-  ( n = 1 -> sum_ k e. ( 0 ... n ) ( ( c ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... 1 ) ( ( c ` k ) x. ( z ^ k ) ) )
5 4 mpteq2dv 
 |-  ( n = 1 -> ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( c ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... 1 ) ( ( c ` k ) x. ( z ^ k ) ) ) )
6 5 eqeq2d 
 |-  ( n = 1 -> ( P = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( c ` k ) x. ( z ^ k ) ) ) <-> P = ( z e. CC |-> sum_ k e. ( 0 ... 1 ) ( ( c ` k ) x. ( z ^ k ) ) ) ) )
7 fveq1 
 |-  ( c = C -> ( c ` k ) = ( C ` k ) )
8 7 oveq1d 
 |-  ( c = C -> ( ( c ` k ) x. ( z ^ k ) ) = ( ( C ` k ) x. ( z ^ k ) ) )
9 8 a1d 
 |-  ( c = C -> ( k e. ( 0 ... 1 ) -> ( ( c ` k ) x. ( z ^ k ) ) = ( ( C ` k ) x. ( z ^ k ) ) ) )
10 9 ralrimiv 
 |-  ( c = C -> A. k e. ( 0 ... 1 ) ( ( c ` k ) x. ( z ^ k ) ) = ( ( C ` k ) x. ( z ^ k ) ) )
11 10 sumeq2d 
 |-  ( c = C -> sum_ k e. ( 0 ... 1 ) ( ( c ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... 1 ) ( ( C ` k ) x. ( z ^ k ) ) )
12 11 mpteq2dv 
 |-  ( c = C -> ( z e. CC |-> sum_ k e. ( 0 ... 1 ) ( ( c ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... 1 ) ( ( C ` k ) x. ( z ^ k ) ) ) )
13 12 eqeq2d 
 |-  ( c = C -> ( P = ( z e. CC |-> sum_ k e. ( 0 ... 1 ) ( ( c ` k ) x. ( z ^ k ) ) ) <-> P = ( z e. CC |-> sum_ k e. ( 0 ... 1 ) ( ( C ` k ) x. ( z ^ k ) ) ) ) )
14 1nn0 
 |-  1 e. NN0
15 14 a1i 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) ) -> 1 e. NN0 )
16 cnex 
 |-  CC e. _V
17 16 ssex 
 |-  ( S C_ CC -> S e. _V )
18 snex 
 |-  { 0 } e. _V
19 18 a1i 
 |-  ( S C_ CC -> { 0 } e. _V )
20 17 19 unexd 
 |-  ( S C_ CC -> ( S u. { 0 } ) e. _V )
21 ssun1 
 |-  S C_ ( S u. { 0 } )
22 mapss 
 |-  ( ( ( S u. { 0 } ) e. _V /\ S C_ ( S u. { 0 } ) ) -> ( S ^m NN0 ) C_ ( ( S u. { 0 } ) ^m NN0 ) )
23 20 21 22 sylancl 
 |-  ( S C_ CC -> ( S ^m NN0 ) C_ ( ( S u. { 0 } ) ^m NN0 ) )
24 23 sselda 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) ) -> C e. ( ( S u. { 0 } ) ^m NN0 ) )
25 1 a1i 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) ) -> P = ( z e. CC |-> sum_ k e. ( 0 ... 1 ) ( ( C ` k ) x. ( z ^ k ) ) ) )
26 6 13 15 24 25 2rspcedvdw 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) ) -> E. n e. NN0 E. c e. ( ( S u. { 0 } ) ^m NN0 ) P = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( c ` k ) x. ( z ^ k ) ) ) )
27 elply 
 |-  ( P e. ( Poly ` S ) <-> ( S C_ CC /\ E. n e. NN0 E. c e. ( ( S u. { 0 } ) ^m NN0 ) P = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( c ` k ) x. ( z ^ k ) ) ) ) )
28 2 26 27 sylanbrc 
 |-  ( ( S C_ CC /\ C e. ( S ^m NN0 ) ) -> P e. ( Poly ` S ) )