Metamath Proof Explorer


Theorem deg1propd

Description: Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses deg1propd.b1 ( 𝜑𝐵 = ( Base ‘ 𝑅 ) )
deg1propd.b2 ( 𝜑𝐵 = ( Base ‘ 𝑆 ) )
deg1propd.p ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝑅 ) 𝑦 ) = ( 𝑥 ( +g𝑆 ) 𝑦 ) )
Assertion deg1propd ( 𝜑 → ( deg1𝑅 ) = ( deg1𝑆 ) )

Proof

Step Hyp Ref Expression
1 deg1propd.b1 ( 𝜑𝐵 = ( Base ‘ 𝑅 ) )
2 deg1propd.b2 ( 𝜑𝐵 = ( Base ‘ 𝑆 ) )
3 deg1propd.p ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝑅 ) 𝑦 ) = ( 𝑥 ( +g𝑆 ) 𝑦 ) )
4 1 2 3 mdegpropd ( 𝜑 → ( 1o mDeg 𝑅 ) = ( 1o mDeg 𝑆 ) )
5 eqid ( deg1𝑅 ) = ( deg1𝑅 )
6 5 deg1fval ( deg1𝑅 ) = ( 1o mDeg 𝑅 )
7 eqid ( deg1𝑆 ) = ( deg1𝑆 )
8 7 deg1fval ( deg1𝑆 ) = ( 1o mDeg 𝑆 )
9 4 6 8 3eqtr4g ( 𝜑 → ( deg1𝑅 ) = ( deg1𝑆 ) )