dvdsq1p

Description: Divisibility in a polynomial ring is witnessed by the quotient. (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)$
	dvdsq1p.t	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	dvdsq1p.q	$⊢ Q = {quot}_{1p} (R)$
Assertion	dvdsq1p	$⊢ (R \in Ring \land F \in B \land G \in C) \to (G \underset{˙}{∥} F \leftrightarrow F = (F Q G) \underset{˙}{\cdot} G)$

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		dvdsq1p.t	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
6		dvdsq1p.q	$⊢ Q = {quot}_{1p} (R)$
7	1 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	3 2 5	dvdsr2	$⊢ G \in B \to (G \underset{˙}{∥} F \leftrightarrow \exists q \in B q \underset{˙}{\cdot} G = F)$
10	8 9	syl	$⊢ (R \in Ring \land F \in B \land G \in C) \to (G \underset{˙}{∥} F \leftrightarrow \exists q \in B q \underset{˙}{\cdot} G = F)$
11		eqcom	$⊢ q \underset{˙}{\cdot} G = F \leftrightarrow F = q \underset{˙}{\cdot} G$
12		simprr	$⊢ ((R \in Ring \land F \in B \land G \in C) \land (q \in B \land F = q \underset{˙}{\cdot} G)) \to F = q \underset{˙}{\cdot} G$
13		simprl	$⊢ ((R \in Ring \land F \in B \land G \in C) \land (q \in B \land F = q \underset{˙}{\cdot} G)) \to q \in B$
14		simpl1	$⊢ ((R \in Ring \land F \in B \land G \in C) \land q \in B) \to R \in Ring$
15	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
16	14 15	syl	$⊢ ((R \in Ring \land F \in B \land G \in C) \land q \in B) \to P \in Ring$
17		ringgrp	$⊢ P \in Ring \to P \in Grp$
18	16 17	syl	$⊢ ((R \in Ring \land F \in B \land G \in C) \land q \in B) \to P \in Grp$
19		simpl2	$⊢ ((R \in Ring \land F \in B \land G \in C) \land q \in B) \to F \in B$
20		simpr	$⊢ ((R \in Ring \land F \in B \land G \in C) \land q \in B) \to q \in B$
21	8	adantr	$⊢ ((R \in Ring \land F \in B \land G \in C) \land q \in B) \to G \in B$
22	3 5	ringcl	$⊢ (P \in Ring \land q \in B \land G \in B) \to q \underset{˙}{\cdot} G \in B$
23	16 20 21 22	syl3anc	$⊢ ((R \in Ring \land F \in B \land G \in C) \land q \in B) \to q \underset{˙}{\cdot} G \in B$
24		eqid	$⊢ 0_{P} = 0_{P}$
25		eqid	$⊢ -_{P} = -_{P}$
26	3 24 25	grpsubeq0	$⊢ (P \in Grp \land F \in B \land q \underset{˙}{\cdot} G \in B) \to (F -_{P} (q \underset{˙}{\cdot} G) = 0_{P} \leftrightarrow F = q \underset{˙}{\cdot} G)$
27	18 19 23 26	syl3anc	$⊢ ((R \in Ring \land F \in B \land G \in C) \land q \in B) \to (F -_{P} (q \underset{˙}{\cdot} G) = 0_{P} \leftrightarrow F = q \underset{˙}{\cdot} G)$
28	27	biimprd	$⊢ ((R \in Ring \land F \in B \land G \in C) \land q \in B) \to (F = q \underset{˙}{\cdot} G \to F -_{P} (q \underset{˙}{\cdot} G) = 0_{P})$
29	28	impr	$⊢ ((R \in Ring \land F \in B \land G \in C) \land (q \in B \land F = q \underset{˙}{\cdot} G)) \to F -_{P} (q \underset{˙}{\cdot} G) = 0_{P}$
30	29	fveq2d	$⊢ ((R \in Ring \land F \in B \land G \in C) \land (q \in B \land F = q \underset{˙}{\cdot} G)) \to \deg_{1} (R) (F -_{P} (q \underset{˙}{\cdot} G)) = \deg_{1} (R) (0_{P})$
31		simpl1	$⊢ ((R \in Ring \land F \in B \land G \in C) \land (q \in B \land F = q \underset{˙}{\cdot} G)) \to R \in Ring$
32		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
33	32 1 24	deg1z	$⊢ R \in Ring \to \deg_{1} (R) (0_{P}) = −∞$
34	31 33	syl	$⊢ ((R \in Ring \land F \in B \land G \in C) \land (q \in B \land F = q \underset{˙}{\cdot} G)) \to \deg_{1} (R) (0_{P}) = −∞$
35	30 34	eqtrd	$⊢ ((R \in Ring \land F \in B \land G \in C) \land (q \in B \land F = q \underset{˙}{\cdot} G)) \to \deg_{1} (R) (F -_{P} (q \underset{˙}{\cdot} G)) = −∞$
36	32 4	uc1pdeg	$⊢ (R \in Ring \land G \in C) \to \deg_{1} (R) (G) \in ℕ_{0}$
37	36	3adant2	$⊢ (R \in Ring \land F \in B \land G \in C) \to \deg_{1} (R) (G) \in ℕ_{0}$
38	37	nn0red	$⊢ (R \in Ring \land F \in B \land G \in C) \to \deg_{1} (R) (G) \in ℝ$
39	38	adantr	$⊢ ((R \in Ring \land F \in B \land G \in C) \land (q \in B \land F = q \underset{˙}{\cdot} G)) \to \deg_{1} (R) (G) \in ℝ$
40	39	mnfltd	$⊢ ((R \in Ring \land F \in B \land G \in C) \land (q \in B \land F = q \underset{˙}{\cdot} G)) \to −∞ < \deg_{1} (R) (G)$
41	35 40	eqbrtrd	$⊢ ((R \in Ring \land F \in B \land G \in C) \land (q \in B \land F = q \underset{˙}{\cdot} G)) \to \deg_{1} (R) (F -_{P} (q \underset{˙}{\cdot} G)) < \deg_{1} (R) (G)$
42	6 1 3 32 25 5 4	q1peqb	$⊢ (R \in Ring \land F \in B \land G \in C) \to ((q \in B \land \deg_{1} (R) (F -_{P} (q \underset{˙}{\cdot} G)) < \deg_{1} (R) (G)) \leftrightarrow F Q G = q)$
43	42	adantr	$⊢ ((R \in Ring \land F \in B \land G \in C) \land (q \in B \land F = q \underset{˙}{\cdot} G)) \to ((q \in B \land \deg_{1} (R) (F -_{P} (q \underset{˙}{\cdot} G)) < \deg_{1} (R) (G)) \leftrightarrow F Q G = q)$
44	13 41 43	mpbi2and	$⊢ ((R \in Ring \land F \in B \land G \in C) \land (q \in B \land F = q \underset{˙}{\cdot} G)) \to F Q G = q$
45	44	oveq1d	$⊢ ((R \in Ring \land F \in B \land G \in C) \land (q \in B \land F = q \underset{˙}{\cdot} G)) \to (F Q G) \underset{˙}{\cdot} G = q \underset{˙}{\cdot} G$
46	12 45	eqtr4d	$⊢ ((R \in Ring \land F \in B \land G \in C) \land (q \in B \land F = q \underset{˙}{\cdot} G)) \to F = (F Q G) \underset{˙}{\cdot} G$
47	46	expr	$⊢ ((R \in Ring \land F \in B \land G \in C) \land q \in B) \to (F = q \underset{˙}{\cdot} G \to F = (F Q G) \underset{˙}{\cdot} G)$
48	11 47	syl5bi	$⊢ ((R \in Ring \land F \in B \land G \in C) \land q \in B) \to (q \underset{˙}{\cdot} G = F \to F = (F Q G) \underset{˙}{\cdot} G)$
49	48	rexlimdva	$⊢ (R \in Ring \land F \in B \land G \in C) \to (\exists q \in B q \underset{˙}{\cdot} G = F \to F = (F Q G) \underset{˙}{\cdot} G)$
50	10 49	sylbid	$⊢ (R \in Ring \land F \in B \land G \in C) \to (G \underset{˙}{∥} F \to F = (F Q G) \underset{˙}{\cdot} G)$
51	6 1 3 4	q1pcl	$⊢ (R \in Ring \land F \in B \land G \in C) \to F Q G \in B$
52	3 2 5	dvdsrmul	$⊢ (G \in B \land F Q G \in B) \to G \underset{˙}{∥} ((F Q G) \underset{˙}{\cdot} G)$
53	8 51 52	syl2anc	$⊢ (R \in Ring \land F \in B \land G \in C) \to G \underset{˙}{∥} ((F Q G) \underset{˙}{\cdot} G)$
54		breq2	$⊢ F = (F Q G) \underset{˙}{\cdot} G \to (G \underset{˙}{∥} F \leftrightarrow G \underset{˙}{∥} ((F Q G) \underset{˙}{\cdot} G))$
55	53 54	syl5ibrcom	$⊢ (R \in Ring \land F \in B \land G \in C) \to (F = (F Q G) \underset{˙}{\cdot} G \to G \underset{˙}{∥} F)$
56	50 55	impbid	$⊢ (R \in Ring \land F \in B \land G \in C) \to (G \underset{˙}{∥} F \leftrightarrow F = (F Q G) \underset{˙}{\cdot} G)$

Metamath Proof Explorer

Theorem dvdsq1p

Proof