r1pdeglt

Description: The remainder has a degree smaller than the divisor. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	r1pval.e	$⊢ E = {rem}_{1p} (R)$
	r1pval.p	$⊢ P = {Poly}_{1} (R)$
	r1pval.b	$⊢ B = {Base}_{P}$
	r1pcl.c	$⊢ C = {Unic}_{1p} (R)$
	r1pdeglt.d	$⊢ D = \deg_{1} (R)$
Assertion	r1pdeglt	$⊢ (R \in Ring \land F \in B \land G \in C) \to D (F E G) < D (G)$

Step	Hyp	Ref	Expression
1		r1pval.e	$⊢ E = {rem}_{1p} (R)$
2		r1pval.p	$⊢ P = {Poly}_{1} (R)$
3		r1pval.b	$⊢ B = {Base}_{P}$
4		r1pcl.c	$⊢ C = {Unic}_{1p} (R)$
5		r1pdeglt.d	$⊢ D = \deg_{1} (R)$
6		simp2	$⊢ (R \in Ring \land F \in B \land G \in C) \to F \in B$
7	2 3 4	uc1pcl	$⊢ G \in C \to G \in B$
8	7	3ad2ant3	$⊢ (R \in Ring \land F \in B \land G \in C) \to G \in B$
9		eqid	$⊢ {quot}_{1p} (R) = {quot}_{1p} (R)$
10		eqid	$⊢ \cdot_{P} = \cdot_{P}$
11		eqid	$⊢ -_{P} = -_{P}$
12	1 2 3 9 10 11	r1pval	$⊢ (F \in B \land G \in B) \to F E G = F -_{P} ((F {quot}_{1p} (R) G) \cdot_{P} G)$
13	6 8 12	syl2anc	$⊢ (R \in Ring \land F \in B \land G \in C) \to F E G = F -_{P} ((F {quot}_{1p} (R) G) \cdot_{P} G)$
14	13	fveq2d	$⊢ (R \in Ring \land F \in B \land G \in C) \to D (F E G) = D (F -_{P} ((F {quot}_{1p} (R) G) \cdot_{P} G))$
15		eqid	$⊢ F {quot}_{1p} (R) G = F {quot}_{1p} (R) G$
16	9 2 3 5 11 10 4	q1peqb	$⊢ (R \in Ring \land F \in B \land G \in C) \to ((F {quot}_{1p} (R) G \in B \land D (F -_{P} ((F {quot}_{1p} (R) G) \cdot_{P} G)) < D (G)) \leftrightarrow F {quot}_{1p} (R) G = F {quot}_{1p} (R) G)$
17	15 16	mpbiri	$⊢ (R \in Ring \land F \in B \land G \in C) \to (F {quot}_{1p} (R) G \in B \land D (F -_{P} ((F {quot}_{1p} (R) G) \cdot_{P} G)) < D (G))$
18	17	simprd	$⊢ (R \in Ring \land F \in B \land G \in C) \to D (F -_{P} ((F {quot}_{1p} (R) G) \cdot_{P} G)) < D (G)$
19	14 18	eqbrtrd	$⊢ (R \in Ring \land F \in B \land G \in C) \to D (F E G) < D (G)$

Metamath Proof Explorer