Theorem deg1sub

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

	Ref	Expression
Hypotheses	deg1addle.y	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
	deg1addle.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1addle.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	deg1suble.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	deg1suble.m	⊢ − = ( -g ‘ 𝑌 )
	deg1suble.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	deg1suble.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	deg1sub.l	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) < ( 𝐷 ‘ 𝐹 ) )
Assertion	deg1sub	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) = ( 𝐷 ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		deg1addle.y	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2		deg1addle.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3		deg1addle.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		deg1suble.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
5		deg1suble.m	⊢ − = ( -g ‘ 𝑌 )
6		deg1suble.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7		deg1suble.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
8		deg1sub.l	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) < ( 𝐷 ‘ 𝐹 ) )
9		eqid	⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
10		eqid	⊢ ( invg ‘ 𝑌 ) = ( invg ‘ 𝑌 )
11	4 9 10 5	grpsubval	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 − 𝐺 ) = ( 𝐹 ( +g ‘ 𝑌 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) )
12	6 7 11	syl2anc	⊢ ( 𝜑 → ( 𝐹 − 𝐺 ) = ( 𝐹 ( +g ‘ 𝑌 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) )
13	12	fveq2d	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) = ( 𝐷 ‘ ( 𝐹 ( +g ‘ 𝑌 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) ) )
14	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑌 ∈ Ring )
15		ringgrp	⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Grp )
16	3 14 15	3syl	⊢ ( 𝜑 → 𝑌 ∈ Grp )
17	4 10	grpinvcl	⊢ ( ( 𝑌 ∈ Grp ∧ 𝐺 ∈ 𝐵 ) → ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ∈ 𝐵 )
18	16 7 17	syl2anc	⊢ ( 𝜑 → ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ∈ 𝐵 )
19	1 2 3 4 10 7	deg1invg	⊢ ( 𝜑 → ( 𝐷 ‘ ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) = ( 𝐷 ‘ 𝐺 ) )
20	19 8	eqbrtrd	⊢ ( 𝜑 → ( 𝐷 ‘ ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) < ( 𝐷 ‘ 𝐹 ) )
21	1 2 3 4 9 6 18 20	deg1add	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 ( +g ‘ 𝑌 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) ) = ( 𝐷 ‘ 𝐹 ) )
22	13 21	eqtrd	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) = ( 𝐷 ‘ 𝐹 ) )