Theorem deg1suble

Description: The degree of a difference of polynomials is bounded by the maximum of degrees. (Contributed by Stefan O'Rear, 26-Mar-2015)

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

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		eqid	⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
9	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑌 ∈ Ring )
10		ringgrp	⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Grp )
11	3 9 10	3syl	⊢ ( 𝜑 → 𝑌 ∈ Grp )
12		eqid	⊢ ( invg ‘ 𝑌 ) = ( invg ‘ 𝑌 )
13	4 12	grpinvcl	⊢ ( ( 𝑌 ∈ Grp ∧ 𝐺 ∈ 𝐵 ) → ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ∈ 𝐵 )
14	11 7 13	syl2anc	⊢ ( 𝜑 → ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ∈ 𝐵 )
15	1 2 3 4 8 6 14	deg1addle	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 ( +g ‘ 𝑌 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) , ( 𝐷 ‘ ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) , ( 𝐷 ‘ 𝐹 ) ) )
16	4 8 12 5	grpsubval	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 − 𝐺 ) = ( 𝐹 ( +g ‘ 𝑌 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) )
17	6 7 16	syl2anc	⊢ ( 𝜑 → ( 𝐹 − 𝐺 ) = ( 𝐹 ( +g ‘ 𝑌 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) )
18	17	fveq2d	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) = ( 𝐷 ‘ ( 𝐹 ( +g ‘ 𝑌 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) ) )
19	1 2 3 4 12 7	deg1invg	⊢ ( 𝜑 → ( 𝐷 ‘ ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) = ( 𝐷 ‘ 𝐺 ) )
20	19	eqcomd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = ( 𝐷 ‘ ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) )
21	20	breq2d	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) ↔ ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) ) )
22	21 20	ifbieq1d	⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) = if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) , ( 𝐷 ‘ ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) , ( 𝐷 ‘ 𝐹 ) ) )
23	15 18 22	3brtr4d	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )