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{\upharpoonright }_{𝑠}T$$
	ressdeg1.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	ressdeg1.u	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
	ressdeg1.b	$$⊢B={\mathrm{Base}}_U$$
	ressdeg1.p	$$⊢\phi \to P\in B$$
	ressdeg1.t	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
Assertion	ressdeg1	$$⊢\phi \to D\left(P\right)={\mathrm{deg}}_1\left(H\right)\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		ressdeg1.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
2		ressdeg1.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
3		ressdeg1.u	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
4		ressdeg1.b	$$⊢B={\mathrm{Base}}_U$$
5		ressdeg1.p	$$⊢\phi \to P\in B$$
6		ressdeg1.t	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
7		eqid	$$⊢0_R=0_R$$
8	1 7	subrg0	$$⊢T\in \mathrm{SubRing}\left(R\right)\to 0_R=0_H$$
9	6 8	syl	$$⊢\phi \to 0_R=0_H$$
10	9	oveq2d	$$⊢\phi \to {\mathrm{coe}}_1\left(P\right)\mathrm{supp}{0}_R={\mathrm{coe}}_1\left(P\right)\mathrm{supp}{0}_H$$
11	10	supeq1d	$$⊢\phi \to sup\left({\mathrm{coe}}_1\left(P\right)\mathrm{supp}{0}_R,{ℝ}^{*},<\right)=sup\left({\mathrm{coe}}_1\left(P\right)\mathrm{supp}{0}_H,{ℝ}^{*},<\right)$$
12		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
13		eqid	$$⊢{\mathrm{PwSer}}_1\left(H\right)={\mathrm{PwSer}}_1\left(H\right)$$
14		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(H\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(H\right)}$$
15		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
16	12 1 3 4 6 13 14 15	ressply1bas2	$$⊢\phi \to B={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(H\right)}\cap {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
17	5 16	eleqtrd	$$⊢\phi \to P\in \left({\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(H\right)}\cap {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right)$$
18	17	elin2d	$$⊢\phi \to P\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
19		eqid	$$⊢{\mathrm{coe}}_1\left(P\right)={\mathrm{coe}}_1\left(P\right)$$
20	2 12 15 7 19	deg1val	$$⊢P\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\to D\left(P\right)=sup\left({\mathrm{coe}}_1\left(P\right)\mathrm{supp}{0}_R,{ℝ}^{*},<\right)$$
21	18 20	syl	$$⊢\phi \to D\left(P\right)=sup\left({\mathrm{coe}}_1\left(P\right)\mathrm{supp}{0}_R,{ℝ}^{*},<\right)$$
22		eqid	$$⊢{\mathrm{deg}}_1\left(H\right)={\mathrm{deg}}_1\left(H\right)$$
23		eqid	$$⊢0_H=0_H$$
24	22 3 4 23 19	deg1val	$$⊢P\in B\to {\mathrm{deg}}_1\left(H\right)\left(P\right)=sup\left({\mathrm{coe}}_1\left(P\right)\mathrm{supp}{0}_H,{ℝ}^{*},<\right)$$
25	5 24	syl	$$⊢\phi \to {\mathrm{deg}}_1\left(H\right)\left(P\right)=sup\left({\mathrm{coe}}_1\left(P\right)\mathrm{supp}{0}_H,{ℝ}^{*},<\right)$$
26	11 21 25	3eqtr4d	$$⊢\phi \to D\left(P\right)={\mathrm{deg}}_1\left(H\right)\left(P\right)$$