r1pid

Description: Express the original polynomial F as F = ( q x. G ) + r using the quotient and remainder functions for q and r . (Contributed by Mario Carneiro, 5-Jun-2015)

	Ref	Expression
Hypotheses	r1pid.p	$⊢ P = {Poly}_{1} (R)$
	r1pid.b	$⊢ B = {Base}_{P}$
	r1pid.c	$⊢ C = {Unic}_{1p} (R)$
	r1pid.q	$⊢ Q = {quot}_{1p} (R)$
	r1pid.e	$⊢ E = {rem}_{1p} (R)$
	r1pid.t	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	r1pid.m	$⊢ \underset{˙}{+} = +_{P}$
Assertion	r1pid	$⊢ (R \in Ring \land F \in B \land G \in C) \to F = ((F Q G) \underset{˙}{\cdot} G) \underset{˙}{+} (F E G)$

Proof

Step	Hyp	Ref	Expression
1		r1pid.p	$⊢ P = {Poly}_{1} (R)$
2		r1pid.b	$⊢ B = {Base}_{P}$
3		r1pid.c	$⊢ C = {Unic}_{1p} (R)$
4		r1pid.q	$⊢ Q = {quot}_{1p} (R)$
5		r1pid.e	$⊢ E = {rem}_{1p} (R)$
6		r1pid.t	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
7		r1pid.m	$⊢ \underset{˙}{+} = +_{P}$
8	1 2 3	uc1pcl	$⊢ G \in C \to G \in B$
9		eqid	$⊢ -_{P} = -_{P}$
10	5 1 2 4 6 9	r1pval	$⊢ (F \in B \land G \in B) \to F E G = F -_{P} ((F Q G) \underset{˙}{\cdot} G)$
11	8 10	sylan2	$⊢ (F \in B \land G \in C) \to F E G = F -_{P} ((F Q G) \underset{˙}{\cdot} G)$
12	11	3adant1	$⊢ (R \in Ring \land F \in B \land G \in C) \to F E G = F -_{P} ((F Q G) \underset{˙}{\cdot} G)$
13	12	oveq2d	$⊢ (R \in Ring \land F \in B \land G \in C) \to ((F Q G) \underset{˙}{\cdot} G) \underset{˙}{+} (F E G) = ((F Q G) \underset{˙}{\cdot} G) \underset{˙}{+} (F -_{P} ((F Q G) \underset{˙}{\cdot} G))$
14	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
15	14	3ad2ant1	$⊢ (R \in Ring \land F \in B \land G \in C) \to P \in Ring$
16		ringabl	$⊢ P \in Ring \to P \in Abel$
17	15 16	syl	$⊢ (R \in Ring \land F \in B \land G \in C) \to P \in Abel$
18	4 1 2 3	q1pcl	$⊢ (R \in Ring \land F \in B \land G \in C) \to F Q G \in B$
19	8	3ad2ant3	$⊢ (R \in Ring \land F \in B \land G \in C) \to G \in B$
20	2 6	ringcl	$⊢ (P \in Ring \land F Q G \in B \land G \in B) \to (F Q G) \underset{˙}{\cdot} G \in B$
21	15 18 19 20	syl3anc	$⊢ (R \in Ring \land F \in B \land G \in C) \to (F Q G) \underset{˙}{\cdot} G \in B$
22		ringgrp	$⊢ P \in Ring \to P \in Grp$
23	15 22	syl	$⊢ (R \in Ring \land F \in B \land G \in C) \to P \in Grp$
24		simp2	$⊢ (R \in Ring \land F \in B \land G \in C) \to F \in B$
25	2 9	grpsubcl	$⊢ (P \in Grp \land F \in B \land (F Q G) \underset{˙}{\cdot} G \in B) \to F -_{P} ((F Q G) \underset{˙}{\cdot} G) \in B$
26	23 24 21 25	syl3anc	$⊢ (R \in Ring \land F \in B \land G \in C) \to F -_{P} ((F Q G) \underset{˙}{\cdot} G) \in B$
27	2 7	ablcom	$⊢ (P \in Abel \land (F Q G) \underset{˙}{\cdot} G \in B \land F -_{P} ((F Q G) \underset{˙}{\cdot} G) \in B) \to ((F Q G) \underset{˙}{\cdot} G) \underset{˙}{+} (F -_{P} ((F Q G) \underset{˙}{\cdot} G)) = (F -_{P} ((F Q G) \underset{˙}{\cdot} G)) \underset{˙}{+} ((F Q G) \underset{˙}{\cdot} G)$
28	17 21 26 27	syl3anc	$⊢ (R \in Ring \land F \in B \land G \in C) \to ((F Q G) \underset{˙}{\cdot} G) \underset{˙}{+} (F -_{P} ((F Q G) \underset{˙}{\cdot} G)) = (F -_{P} ((F Q G) \underset{˙}{\cdot} G)) \underset{˙}{+} ((F Q G) \underset{˙}{\cdot} G)$
29	2 7 9	grpnpcan	$⊢ (P \in Grp \land F \in B \land (F Q G) \underset{˙}{\cdot} G \in B) \to (F -_{P} ((F Q G) \underset{˙}{\cdot} G)) \underset{˙}{+} ((F Q G) \underset{˙}{\cdot} G) = F$
30	23 24 21 29	syl3anc	$⊢ (R \in Ring \land F \in B \land G \in C) \to (F -_{P} ((F Q G) \underset{˙}{\cdot} G)) \underset{˙}{+} ((F Q G) \underset{˙}{\cdot} G) = F$
31	13 28 30	3eqtrrd	$⊢ (R \in Ring \land F \in B \land G \in C) \to F = ((F Q G) \underset{˙}{\cdot} G) \underset{˙}{+} (F E G)$

Metamath Proof Explorer

Theorem r1pid

Proof