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 ⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
ressdeg1.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
ressdeg1.u ⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
ressdeg1.b ⊢ 𝐵 = ( Base ‘ 𝑈 )
ressdeg1.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
ressdeg1.t ⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
Assertion ressdeg1 ( 𝜑 → ( 𝐷 ‘ 𝑃 ) = ( ( deg1 ‘ 𝐻 ) ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 ressdeg1.h ⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
2 ressdeg1.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3 ressdeg1.u ⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
4 ressdeg1.b ⊢ 𝐵 = ( Base ‘ 𝑈 )
5 ressdeg1.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
6 ressdeg1.t ⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
7 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
8 1 7 subrg0 ⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝐻 ) )
9 6 8 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝐻 ) )
10 9 oveq2d ⊢ ( 𝜑 → ( ( coe1 ‘ 𝑃 ) supp ( 0g ‘ 𝑅 ) ) = ( ( coe1 ‘ 𝑃 ) supp ( 0g ‘ 𝐻 ) ) )
11 10 supeq1d ⊢ ( 𝜑 → sup ( ( ( coe1 ‘ 𝑃 ) supp ( 0g ‘ 𝑅 ) ) , ℝ* , < ) = sup ( ( ( coe1 ‘ 𝑃 ) supp ( 0g ‘ 𝐻 ) ) , ℝ* , < ) )
12 eqid ⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
13 eqid ⊢ ( PwSer1 ‘ 𝐻 ) = ( PwSer1 ‘ 𝐻 )
14 eqid ⊢ ( Base ‘ ( PwSer1 ‘ 𝐻 ) ) = ( Base ‘ ( PwSer1 ‘ 𝐻 ) )
15 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
16 12 1 3 4 6 13 14 15 ressply1bas2 ⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ ( PwSer1 ‘ 𝐻 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) )
17 5 16 eleqtrd ⊢ ( 𝜑 → 𝑃 ∈ ( ( Base ‘ ( PwSer1 ‘ 𝐻 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) )
18 17 elin2d ⊢ ( 𝜑 → 𝑃 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
19 eqid ⊢ ( coe1 ‘ 𝑃 ) = ( coe1 ‘ 𝑃 )
20 2 12 15 7 19 deg1val ⊢ ( 𝑃 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) → ( 𝐷 ‘ 𝑃 ) = sup ( ( ( coe1 ‘ 𝑃 ) supp ( 0g ‘ 𝑅 ) ) , ℝ* , < ) )
21 18 20 syl ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑃 ) = sup ( ( ( coe1 ‘ 𝑃 ) supp ( 0g ‘ 𝑅 ) ) , ℝ* , < ) )
22 eqid ⊢ ( deg1 ‘ 𝐻 ) = ( deg1 ‘ 𝐻 )
23 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
24 22 3 4 23 19 deg1val ⊢ ( 𝑃 ∈ 𝐵 → ( ( deg1 ‘ 𝐻 ) ‘ 𝑃 ) = sup ( ( ( coe1 ‘ 𝑃 ) supp ( 0g ‘ 𝐻 ) ) , ℝ* , < ) )
25 5 24 syl ⊢ ( 𝜑 → ( ( deg1 ‘ 𝐻 ) ‘ 𝑃 ) = sup ( ( ( coe1 ‘ 𝑃 ) supp ( 0g ‘ 𝐻 ) ) , ℝ* , < ) )
26 11 21 25 3eqtr4d ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑃 ) = ( ( deg1 ‘ 𝐻 ) ‘ 𝑃 ) )