q1peqb

Description: Characterizing property of the polynomial quotient. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	q1pval.q	$⊢ Q = {quot}_{1p} (R)$
	q1pval.p	$⊢ P = {Poly}_{1} (R)$
	q1pval.b	$⊢ B = {Base}_{P}$
	q1pval.d	$⊢ D = \deg_{1} (R)$
	q1pval.m	$⊢ \underset{˙}{-} = -_{P}$
	q1pval.t	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	q1peqb.c	$⊢ C = {Unic}_{1p} (R)$
Assertion	q1peqb	$⊢ (R \in Ring \land F \in B \land G \in C) \to ((X \in B \land D (F \underset{˙}{-} (X \underset{˙}{\cdot} G)) < D (G)) \leftrightarrow F Q G = X)$

Proof

Step	Hyp	Ref	Expression
1		q1pval.q	$⊢ Q = {quot}_{1p} (R)$
2		q1pval.p	$⊢ P = {Poly}_{1} (R)$
3		q1pval.b	$⊢ B = {Base}_{P}$
4		q1pval.d	$⊢ D = \deg_{1} (R)$
5		q1pval.m	$⊢ \underset{˙}{-} = -_{P}$
6		q1pval.t	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
7		q1peqb.c	$⊢ C = {Unic}_{1p} (R)$
8		elex	$⊢ X \in B \to X \in V$
9	8	adantr	$⊢ (X \in B \land D (F \underset{˙}{-} (X \underset{˙}{\cdot} G)) < D (G)) \to X \in V$
10	9	a1i	$⊢ (R \in Ring \land F \in B \land G \in C) \to ((X \in B \land D (F \underset{˙}{-} (X \underset{˙}{\cdot} G)) < D (G)) \to X \in V)$
11		ovex	$⊢ F Q G \in V$
12		eleq1	$⊢ F Q G = X \to (F Q G \in V \leftrightarrow X \in V)$
13	11 12	mpbii	$⊢ F Q G = X \to X \in V$
14	13	a1i	$⊢ (R \in Ring \land F \in B \land G \in C) \to (F Q G = X \to X \in V)$
15		simpr	$⊢ ((R \in Ring \land F \in B \land G \in C) \land X \in V) \to X \in V$
16		eqid	$⊢ 0_{P} = 0_{P}$
17		simp1	$⊢ (R \in Ring \land F \in B \land G \in C) \to R \in Ring$
18		simp2	$⊢ (R \in Ring \land F \in B \land G \in C) \to F \in B$
19	2 3 7	uc1pcl	$⊢ G \in C \to G \in B$
20	19	3ad2ant3	$⊢ (R \in Ring \land F \in B \land G \in C) \to G \in B$
21	2 16 7	uc1pn0	$⊢ G \in C \to G \neq 0_{P}$
22	21	3ad2ant3	$⊢ (R \in Ring \land F \in B \land G \in C) \to G \neq 0_{P}$
23		eqid	$⊢ Unit (R) = Unit (R)$
24	4 23 7	uc1pldg	$⊢ G \in C \to {coe}_{1} (G) (D (G)) \in Unit (R)$
25	24	3ad2ant3	$⊢ (R \in Ring \land F \in B \land G \in C) \to {coe}_{1} (G) (D (G)) \in Unit (R)$
26	2 4 3 5 16 6 17 18 20 22 25 23	ply1divalg2	$⊢ (R \in Ring \land F \in B \land G \in C) \to \exists! q \in B D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G)$
27		df-reu	$⊢ \exists! q \in B D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G) \leftrightarrow \exists! q (q \in B \land D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G))$
28	26 27	sylib	$⊢ (R \in Ring \land F \in B \land G \in C) \to \exists! q (q \in B \land D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G))$
29	28	adantr	$⊢ ((R \in Ring \land F \in B \land G \in C) \land X \in V) \to \exists! q (q \in B \land D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G))$
30		eleq1	$⊢ q = X \to (q \in B \leftrightarrow X \in B)$
31		oveq1	$⊢ q = X \to q \underset{˙}{\cdot} G = X \underset{˙}{\cdot} G$
32	31	oveq2d	$⊢ q = X \to F \underset{˙}{-} (q \underset{˙}{\cdot} G) = F \underset{˙}{-} (X \underset{˙}{\cdot} G)$
33	32	fveq2d	$⊢ q = X \to D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) = D (F \underset{˙}{-} (X \underset{˙}{\cdot} G))$
34	33	breq1d	$⊢ q = X \to (D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G) \leftrightarrow D (F \underset{˙}{-} (X \underset{˙}{\cdot} G)) < D (G))$
35	30 34	anbi12d	$⊢ q = X \to ((q \in B \land D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G)) \leftrightarrow (X \in B \land D (F \underset{˙}{-} (X \underset{˙}{\cdot} G)) < D (G)))$
36	35	adantl	$⊢ (((R \in Ring \land F \in B \land G \in C) \land X \in V) \land q = X) \to ((q \in B \land D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G)) \leftrightarrow (X \in B \land D (F \underset{˙}{-} (X \underset{˙}{\cdot} G)) < D (G)))$
37	15 29 36	iota2d	$⊢ ((R \in Ring \land F \in B \land G \in C) \land X \in V) \to ((X \in B \land D (F \underset{˙}{-} (X \underset{˙}{\cdot} G)) < D (G)) \leftrightarrow (ι q \| (q \in B \land D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G))) = X)$
38	1 2 3 4 5 6	q1pval	$⊢ (F \in B \land G \in B) \to F Q G = (ι q \in B \| D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G))$
39	18 20 38	syl2anc	$⊢ (R \in Ring \land F \in B \land G \in C) \to F Q G = (ι q \in B \| D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G))$
40		df-riota	$⊢ (ι q \in B \| D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G)) = (ι q \| (q \in B \land D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G)))$
41	39 40	syl6eq	$⊢ (R \in Ring \land F \in B \land G \in C) \to F Q G = (ι q \| (q \in B \land D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G)))$
42	41	adantr	$⊢ ((R \in Ring \land F \in B \land G \in C) \land X \in V) \to F Q G = (ι q \| (q \in B \land D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G)))$
43	42	eqeq1d	$⊢ ((R \in Ring \land F \in B \land G \in C) \land X \in V) \to (F Q G = X \leftrightarrow (ι q \| (q \in B \land D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G))) = X)$
44	37 43	bitr4d	$⊢ ((R \in Ring \land F \in B \land G \in C) \land X \in V) \to ((X \in B \land D (F \underset{˙}{-} (X \underset{˙}{\cdot} G)) < D (G)) \leftrightarrow F Q G = X)$
45	44	ex	$⊢ (R \in Ring \land F \in B \land G \in C) \to (X \in V \to ((X \in B \land D (F \underset{˙}{-} (X \underset{˙}{\cdot} G)) < D (G)) \leftrightarrow F Q G = X))$
46	10 14 45	pm5.21ndd	$⊢ (R \in Ring \land F \in B \land G \in C) \to ((X \in B \land D (F \underset{˙}{-} (X \underset{˙}{\cdot} G)) < D (G)) \leftrightarrow F Q G = X)$

Metamath Proof Explorer

Theorem q1peqb

Proof