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 ) )

Metamath Proof Explorer

Theorem ressdeg1

Proof