dvdsr1p

Description: Divisibility in a polynomial ring in terms of the remainder. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	dvdsq1p.p	$⊢ P = {Poly}_{1} (R)$
	dvdsq1p.d	$⊢ \underset{˙}{∥} = ∥_{r} (P)$
	dvdsq1p.b	$⊢ B = {Base}_{P}$
	dvdsq1p.c	$⊢ C = {Unic}_{1p} (R)$
	dvdsr1p.z	$⊢ \underset{˙}{0} = 0_{P}$
	dvdsr1p.e	$⊢ E = {rem}_{1p} (R)$
Assertion	dvdsr1p	$⊢ (R \in Ring \land F \in B \land G \in C) \to (G \underset{˙}{∥} F \leftrightarrow F E G = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		dvdsq1p.p	$⊢ P = {Poly}_{1} (R)$
2		dvdsq1p.d	$⊢ \underset{˙}{∥} = ∥_{r} (P)$
3		dvdsq1p.b	$⊢ B = {Base}_{P}$
4		dvdsq1p.c	$⊢ C = {Unic}_{1p} (R)$
5		dvdsr1p.z	$⊢ \underset{˙}{0} = 0_{P}$
6		dvdsr1p.e	$⊢ E = {rem}_{1p} (R)$
7	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
8	7	3ad2ant1	$⊢ (R \in Ring \land F \in B \land G \in C) \to P \in Ring$
9		ringgrp	$⊢ P \in Ring \to P \in Grp$
10	8 9	syl	$⊢ (R \in Ring \land F \in B \land G \in C) \to P \in Grp$
11		simp2	$⊢ (R \in Ring \land F \in B \land G \in C) \to F \in B$
12		eqid	$⊢ {quot}_{1p} (R) = {quot}_{1p} (R)$
13	12 1 3 4	q1pcl	$⊢ (R \in Ring \land F \in B \land G \in C) \to F {quot}_{1p} (R) G \in B$
14	1 3 4	uc1pcl	$⊢ G \in C \to G \in B$
15	14	3ad2ant3	$⊢ (R \in Ring \land F \in B \land G \in C) \to G \in B$
16		eqid	$⊢ \cdot_{P} = \cdot_{P}$
17	3 16	ringcl	$⊢ (P \in Ring \land F {quot}_{1p} (R) G \in B \land G \in B) \to (F {quot}_{1p} (R) G) \cdot_{P} G \in B$
18	8 13 15 17	syl3anc	$⊢ (R \in Ring \land F \in B \land G \in C) \to (F {quot}_{1p} (R) G) \cdot_{P} G \in B$
19		eqid	$⊢ -_{P} = -_{P}$
20	3 5 19	grpsubeq0	$⊢ (P \in Grp \land F \in B \land (F {quot}_{1p} (R) G) \cdot_{P} G \in B) \to (F -_{P} ((F {quot}_{1p} (R) G) \cdot_{P} G) = \underset{˙}{0} \leftrightarrow F = (F {quot}_{1p} (R) G) \cdot_{P} G)$
21	10 11 18 20	syl3anc	$⊢ (R \in Ring \land F \in B \land G \in C) \to (F -_{P} ((F {quot}_{1p} (R) G) \cdot_{P} G) = \underset{˙}{0} \leftrightarrow F = (F {quot}_{1p} (R) G) \cdot_{P} G)$
22	6 1 3 12 16 19	r1pval	$⊢ (F \in B \land G \in B) \to F E G = F -_{P} ((F {quot}_{1p} (R) G) \cdot_{P} G)$
23	11 15 22	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)$
24	23	eqeq1d	$⊢ (R \in Ring \land F \in B \land G \in C) \to (F E G = \underset{˙}{0} \leftrightarrow F -_{P} ((F {quot}_{1p} (R) G) \cdot_{P} G) = \underset{˙}{0})$
25	1 2 3 4 16 12	dvdsq1p	$⊢ (R \in Ring \land F \in B \land G \in C) \to (G \underset{˙}{∥} F \leftrightarrow F = (F {quot}_{1p} (R) G) \cdot_{P} G)$
26	21 24 25	3bitr4rd	$⊢ (R \in Ring \land F \in B \land G \in C) \to (G \underset{˙}{∥} F \leftrightarrow F E G = \underset{˙}{0})$

Metamath Proof Explorer

Theorem dvdsr1p

Proof