deg1sub

Description: Exact degree of a difference of two polynomials of unequal degree. (Contributed by Stefan O'Rear, 28-Mar-2015)

Step	Hyp	Ref	Expression
1		deg1addle.y	$⊢ Y = {Poly}_{1} (R)$
2		deg1addle.d	$⊢ D = \deg_{1} (R)$
3		deg1addle.r	$⊢ φ \to R \in Ring$
4		deg1suble.b	$⊢ B = {Base}_{Y}$
5		deg1suble.m	$⊢ \underset{˙}{-} = -_{Y}$
6		deg1suble.f	$⊢ φ \to F \in B$
7		deg1suble.g	$⊢ φ \to G \in B$
8		deg1sub.l	$⊢ φ \to D (G) < D (F)$
9		eqid	$⊢ +_{Y} = +_{Y}$
10		eqid	$⊢ {inv}_{g} (Y) = {inv}_{g} (Y)$
11	4 9 10 5	grpsubval	$⊢ (F \in B \land G \in B) \to F \underset{˙}{-} G = F +_{Y} {inv}_{g} (Y) (G)$
12	6 7 11	syl2anc	$⊢ φ \to F \underset{˙}{-} G = F +_{Y} {inv}_{g} (Y) (G)$
13	12	fveq2d	$⊢ φ \to D (F \underset{˙}{-} G) = D (F +_{Y} {inv}_{g} (Y) (G))$
14	1	ply1ring	$⊢ R \in Ring \to Y \in Ring$
15		ringgrp	$⊢ Y \in Ring \to Y \in Grp$
16	3 14 15	3syl	$⊢ φ \to Y \in Grp$
17	4 10	grpinvcl	$⊢ (Y \in Grp \land G \in B) \to {inv}_{g} (Y) (G) \in B$
18	16 7 17	syl2anc	$⊢ φ \to {inv}_{g} (Y) (G) \in B$
19	1 2 3 4 10 7	deg1invg	$⊢ φ \to D ({inv}_{g} (Y) (G)) = D (G)$
20	19 8	eqbrtrd	$⊢ φ \to D ({inv}_{g} (Y) (G)) < D (F)$
21	1 2 3 4 9 6 18 20	deg1add	$⊢ φ \to D (F +_{Y} {inv}_{g} (Y) (G)) = D (F)$
22	13 21	eqtrd	$⊢ φ \to D (F \underset{˙}{-} G) = D (F)$

Metamath Proof Explorer