deg1propd

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

	Ref	Expression
Hypotheses	deg1propd.b1	$⊢ φ \to B = {Base}_{R}$
	deg1propd.b2	$⊢ φ \to B = {Base}_{S}$
	deg1propd.p	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{R} y = x +_{S} y$
Assertion	deg1propd	$⊢ φ \to \deg_{1} (R) = \deg_{1} (S)$

Step	Hyp	Ref	Expression
1		deg1propd.b1	$⊢ φ \to B = {Base}_{R}$
2		deg1propd.b2	$⊢ φ \to B = {Base}_{S}$
3		deg1propd.p	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{R} y = x +_{S} y$
4	1 2 3	mdegpropd	$⊢ φ \to 1_{𝑜} mDeg R = 1_{𝑜} mDeg S$
5		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
6	5	deg1fval	$⊢ \deg_{1} (R) = 1_{𝑜} mDeg R$
7		eqid	$⊢ \deg_{1} (S) = \deg_{1} (S)$
8	7	deg1fval	$⊢ \deg_{1} (S) = 1_{𝑜} mDeg S$
9	4 6 8	3eqtr4g	$⊢ φ \to \deg_{1} (R) = \deg_{1} (S)$

Metamath Proof Explorer