Metamath Proof Explorer

Theorem deg1val

Description: Value of the univariate degree as a supremum. (Contributed by Stefan O'Rear, 29-Mar-2015) (Revised by AV, 25-Jul-2019)

Ref Expression
Hypotheses deg1leb.d 
|- D = ( deg1 ` R )
deg1leb.p 
|- P = ( Poly1 ` R )
deg1leb.b 
|- B = ( Base ` P )
deg1leb.y 
|- .0. = ( 0g ` R )
deg1leb.a 
|- A = ( coe1 ` F )
Assertion deg1val 
|- ( F e. B -> ( D ` F ) = sup ( ( A supp .0. ) , RR* , < ) )

Proof

Step Hyp Ref Expression
1 deg1leb.d 
 |-  D = ( deg1 ` R )
2 deg1leb.p 
 |-  P = ( Poly1 ` R )
3 deg1leb.b 
 |-  B = ( Base ` P )
4 deg1leb.y 
 |-  .0. = ( 0g ` R )
5 deg1leb.a 
 |-  A = ( coe1 ` F )
6 1 deg1fval 
 |-  D = ( 1o mDeg R )
7 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
8 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
9 2 8 3 ply1bas 
 |-  B = ( Base ` ( 1o mPoly R ) )
10 psr1baslem 
 |-  ( NN0 ^m 1o ) = { y e. ( NN0 ^m 1o ) | ( `' y " NN ) e. Fin }
11 tdeglem2 
 |-  ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) = ( x e. ( NN0 ^m 1o ) |-> ( CCfld gsum x ) )
12 6 7 9 4 10 11 mdegval 
 |-  ( F e. B -> ( D ` F ) = sup ( ( ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) " ( F supp .0. ) ) , RR* , < ) )
13 4 fvexi 
 |-  .0. e. _V
14 suppimacnv 
 |-  ( ( F e. B /\ .0. e. _V ) -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) )
15 13 14 mpan2 
 |-  ( F e. B -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) )
16 15 imaeq2d 
 |-  ( F e. B -> ( ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) " ( F supp .0. ) ) = ( ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) " ( `' F " ( _V \ { .0. } ) ) ) )
17 imaco 
 |-  ( ( ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) o. `' F ) " ( _V \ { .0. } ) ) = ( ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) " ( `' F " ( _V \ { .0. } ) ) )
18 16 17 eqtr4di 
 |-  ( F e. B -> ( ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) " ( F supp .0. ) ) = ( ( ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) o. `' F ) " ( _V \ { .0. } ) ) )
19 df1o2 
 |-  1o = { (/) }
20 nn0ex 
 |-  NN0 e. _V
21 0ex 
 |-  (/) e. _V
22 eqid 
 |-  ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) = ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) )
23 19 20 21 22 mapsncnv 
 |-  `' ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) = ( y e. NN0 |-> ( 1o X. { y } ) )
24 5 3 2 23 coe1fval2 
 |-  ( F e. B -> A = ( F o. `' ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) ) )
25 24 cnveqd 
 |-  ( F e. B -> `' A = `' ( F o. `' ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) ) )
26 cnvco 
 |-  `' ( F o. `' ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) ) = ( `' `' ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) o. `' F )
27 cocnvcnv1 
 |-  ( `' `' ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) o. `' F ) = ( ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) o. `' F )
28 26 27 eqtri 
 |-  `' ( F o. `' ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) ) = ( ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) o. `' F )
29 25 28 eqtr2di 
 |-  ( F e. B -> ( ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) o. `' F ) = `' A )
30 29 imaeq1d 
 |-  ( F e. B -> ( ( ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) o. `' F ) " ( _V \ { .0. } ) ) = ( `' A " ( _V \ { .0. } ) ) )
31 18 30 eqtrd 
 |-  ( F e. B -> ( ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) " ( F supp .0. ) ) = ( `' A " ( _V \ { .0. } ) ) )
32 5 fvexi 
 |-  A e. _V
33 suppimacnv 
 |-  ( ( A e. _V /\ .0. e. _V ) -> ( A supp .0. ) = ( `' A " ( _V \ { .0. } ) ) )
34 33 eqcomd 
 |-  ( ( A e. _V /\ .0. e. _V ) -> ( `' A " ( _V \ { .0. } ) ) = ( A supp .0. ) )
35 32 13 34 mp2an 
 |-  ( `' A " ( _V \ { .0. } ) ) = ( A supp .0. )
36 31 35 eqtrdi 
 |-  ( F e. B -> ( ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) " ( F supp .0. ) ) = ( A supp .0. ) )
37 36 supeq1d 
 |-  ( F e. B -> sup ( ( ( x e. ( NN0 ^m 1o ) |-> ( x ` (/) ) ) " ( F supp .0. ) ) , RR* , < ) = sup ( ( A supp .0. ) , RR* , < ) )
38 12 37 eqtrd 
 |-  ( F e. B -> ( D ` F ) = sup ( ( A supp .0. ) , RR* , < ) )