Theorem deg1propd

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

	Ref	Expression
Hypotheses	deg1propd.b1	$$⊢\phi \to B={\mathrm{Base}}_R$$
	deg1propd.b2	$$⊢\phi \to B={\mathrm{Base}}_S$$
	deg1propd.p	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{R}y=x{+}_{S}y$$
Assertion	deg1propd	$$⊢\phi \to {\mathrm{deg}}_1\left(R\right)={\mathrm{deg}}_1\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		deg1propd.b1	$$⊢\phi \to B={\mathrm{Base}}_R$$
2		deg1propd.b2	$$⊢\phi \to B={\mathrm{Base}}_S$$
3		deg1propd.p	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{R}y=x{+}_{S}y$$
4	1 2 3	mdegpropd	$$⊢\phi \to 1_{𝑜}\mathrm{mDeg}R=1_{𝑜}\mathrm{mDeg}S$$
5		eqid	$$⊢{\mathrm{deg}}_1\left(R\right)={\mathrm{deg}}_1\left(R\right)$$
6	5	deg1fval	$$⊢{\mathrm{deg}}_1\left(R\right)=1_{𝑜}\mathrm{mDeg}R$$
7		eqid	$$⊢{\mathrm{deg}}_1\left(S\right)={\mathrm{deg}}_1\left(S\right)$$
8	7	deg1fval	$$⊢{\mathrm{deg}}_1\left(S\right)=1_{𝑜}\mathrm{mDeg}S$$
9	4 6 8	3eqtr4g	$$⊢\phi \to {\mathrm{deg}}_1\left(R\right)={\mathrm{deg}}_1\left(S\right)$$