This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ressdeg1

Description: The degree of a univariate polynomial in a structure restriction. (Contributed by Thierry Arnoux, 20-Jan-2025)

Ref Expression
Hypotheses ressdeg1.h 
|- H = ( R |`s T )
ressdeg1.d 
|- D = ( deg1 ` R )
ressdeg1.u 
|- U = ( Poly1 ` H )
ressdeg1.b 
|- B = ( Base ` U )
ressdeg1.p 
|- ( ph -> P e. B )
ressdeg1.t 
|- ( ph -> T e. ( SubRing ` R ) )
Assertion ressdeg1 
|- ( ph -> ( D ` P ) = ( ( deg1 ` H ) ` P ) )

Proof

Step Hyp Ref Expression
1 ressdeg1.h 
 |-  H = ( R |`s T )
2 ressdeg1.d 
 |-  D = ( deg1 ` R )
3 ressdeg1.u 
 |-  U = ( Poly1 ` H )
4 ressdeg1.b 
 |-  B = ( Base ` U )
5 ressdeg1.p 
 |-  ( ph -> P e. B )
6 ressdeg1.t 
 |-  ( ph -> T e. ( SubRing ` R ) )
7 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
8 1 7 subrg0 
 |-  ( T e. ( SubRing ` R ) -> ( 0g ` R ) = ( 0g ` H ) )
9 6 8 syl 
 |-  ( ph -> ( 0g ` R ) = ( 0g ` H ) )
10 9 oveq2d 
 |-  ( ph -> ( ( coe1 ` P ) supp ( 0g ` R ) ) = ( ( coe1 ` P ) supp ( 0g ` H ) ) )
11 10 supeq1d 
 |-  ( ph -> sup ( ( ( coe1 ` P ) supp ( 0g ` R ) ) , RR* , < ) = sup ( ( ( coe1 ` P ) supp ( 0g ` H ) ) , RR* , < ) )
12 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
13 eqid 
 |-  ( PwSer1 ` H ) = ( PwSer1 ` H )
14 eqid 
 |-  ( Base ` ( PwSer1 ` H ) ) = ( Base ` ( PwSer1 ` H ) )
15 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
16 12 1 3 4 6 13 14 15 ressply1bas2 
 |-  ( ph -> B = ( ( Base ` ( PwSer1 ` H ) ) i^i ( Base ` ( Poly1 ` R ) ) ) )
17 5 16 eleqtrd 
 |-  ( ph -> P e. ( ( Base ` ( PwSer1 ` H ) ) i^i ( Base ` ( Poly1 ` R ) ) ) )
18 17 elin2d 
 |-  ( ph -> P e. ( Base ` ( Poly1 ` R ) ) )
19 eqid 
 |-  ( coe1 ` P ) = ( coe1 ` P )
20 2 12 15 7 19 deg1val 
 |-  ( P e. ( Base ` ( Poly1 ` R ) ) -> ( D ` P ) = sup ( ( ( coe1 ` P ) supp ( 0g ` R ) ) , RR* , < ) )
21 18 20 syl 
 |-  ( ph -> ( D ` P ) = sup ( ( ( coe1 ` P ) supp ( 0g ` R ) ) , RR* , < ) )
22 eqid 
 |-  ( deg1 ` H ) = ( deg1 ` H )
23 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
24 22 3 4 23 19 deg1val 
 |-  ( P e. B -> ( ( deg1 ` H ) ` P ) = sup ( ( ( coe1 ` P ) supp ( 0g ` H ) ) , RR* , < ) )
25 5 24 syl 
 |-  ( ph -> ( ( deg1 ` H ) ` P ) = sup ( ( ( coe1 ` P ) supp ( 0g ` H ) ) , RR* , < ) )
26 11 21 25 3eqtr4d 
 |-  ( ph -> ( D ` P ) = ( ( deg1 ` H ) ` P ) )