Metamath Proof Explorer

Theorem coe11

Description: The coefficient function is one-to-one, so if the coefficients are equal then the functions are equal and vice-versa. (Contributed by Mario Carneiro, 24-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses coefv0.1 
|- A = ( coeff ` F )
coeadd.2 
|- B = ( coeff ` G )
Assertion coe11 
|- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F = G <-> A = B ) )

Proof

Step Hyp Ref Expression
1 coefv0.1 
 |-  A = ( coeff ` F )
2 coeadd.2 
 |-  B = ( coeff ` G )
3 fveq2 
 |-  ( F = G -> ( coeff ` F ) = ( coeff ` G ) )
4 3 1 2 3eqtr4g 
 |-  ( F = G -> A = B )
5 simp3 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ A = B ) -> A = B )
6 5 cnveqd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ A = B ) -> `' A = `' B )
7 6 imaeq1d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ A = B ) -> ( `' A " ( CC \ { 0 } ) ) = ( `' B " ( CC \ { 0 } ) ) )
8 7 supeq1d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ A = B ) -> sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) = sup ( ( `' B " ( CC \ { 0 } ) ) , NN0 , < ) )
9 1 dgrval 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) = sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) )
10 9 3ad2ant1 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ A = B ) -> ( deg ` F ) = sup ( ( `' A " ( CC \ { 0 } ) ) , NN0 , < ) )
11 2 dgrval 
 |-  ( G e. ( Poly ` S ) -> ( deg ` G ) = sup ( ( `' B " ( CC \ { 0 } ) ) , NN0 , < ) )
12 11 3ad2ant2 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ A = B ) -> ( deg ` G ) = sup ( ( `' B " ( CC \ { 0 } ) ) , NN0 , < ) )
13 8 10 12 3eqtr4d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ A = B ) -> ( deg ` F ) = ( deg ` G ) )
14 13 oveq2d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ A = B ) -> ( 0 ... ( deg ` F ) ) = ( 0 ... ( deg ` G ) ) )
15 simpl3 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ A = B ) /\ k e. ( 0 ... ( deg ` F ) ) ) -> A = B )
16 15 fveq1d 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ A = B ) /\ k e. ( 0 ... ( deg ` F ) ) ) -> ( A ` k ) = ( B ` k ) )
17 16 oveq1d 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ A = B ) /\ k e. ( 0 ... ( deg ` F ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) = ( ( B ` k ) x. ( z ^ k ) ) )
18 14 17 sumeq12dv 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ A = B ) -> sum_ k e. ( 0 ... ( deg ` F ) ) ( ( A ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... ( deg ` G ) ) ( ( B ` k ) x. ( z ^ k ) ) )
19 18 mpteq2dv 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ A = B ) -> ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` F ) ) ( ( A ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` G ) ) ( ( B ` k ) x. ( z ^ k ) ) ) )
20 eqid 
 |-  ( deg ` F ) = ( deg ` F )
21 1 20 coeid 
 |-  ( F e. ( Poly ` S ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` F ) ) ( ( A ` k ) x. ( z ^ k ) ) ) )
22 21 3ad2ant1 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ A = B ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` F ) ) ( ( A ` k ) x. ( z ^ k ) ) ) )
23 eqid 
 |-  ( deg ` G ) = ( deg ` G )
24 2 23 coeid 
 |-  ( G e. ( Poly ` S ) -> G = ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` G ) ) ( ( B ` k ) x. ( z ^ k ) ) ) )
25 24 3ad2ant2 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ A = B ) -> G = ( z e. CC |-> sum_ k e. ( 0 ... ( deg ` G ) ) ( ( B ` k ) x. ( z ^ k ) ) ) )
26 19 22 25 3eqtr4d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ A = B ) -> F = G )
27 26 3expia 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( A = B -> F = G ) )
28 4 27 impbid2 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F = G <-> A = B ) )