Theorem deg1propd

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

	Ref	Expression
Hypotheses	deg1propd.b1	|- ( ph -> B = ( Base ` R ) )
	deg1propd.b2	|- ( ph -> B = ( Base ` S ) )
	deg1propd.p	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` S ) y ) )
Assertion	deg1propd	|- ( ph -> ( deg1 ` R ) = ( deg1 ` S ) )

Proof

Step	Hyp	Ref	Expression
1		deg1propd.b1	|- ( ph -> B = ( Base ` R ) )
2		deg1propd.b2	|- ( ph -> B = ( Base ` S ) )
3		deg1propd.p	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` S ) y ) )
4	1 2 3	mdegpropd	|- ( ph -> ( 1o mDeg R ) = ( 1o mDeg S ) )
5		eqid	|- ( deg1 ` R ) = ( deg1 ` R )
6	5	deg1fval	|- ( deg1 ` R ) = ( 1o mDeg R )
7		eqid	|- ( deg1 ` S ) = ( deg1 ` S )
8	7	deg1fval	|- ( deg1 ` S ) = ( 1o mDeg S )
9	4 6 8	3eqtr4g	|- ( ph -> ( deg1 ` R ) = ( deg1 ` S ) )