q1pval

Description: Value of the univariate polynomial quotient function. (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}$
Assertion	q1pval	$⊢ (F \in B \land G \in B) \to F Q G = (ι q \in B \| D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G))$

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	2 3	elbasfv	$⊢ G \in B \to R \in V$
8		fveq2	$⊢ r = R \to {Poly}_{1} (r) = {Poly}_{1} (R)$
9	8 2	eqtr4di	$⊢ r = R \to {Poly}_{1} (r) = P$
10	9	csbeq1d	$⊢ r = R \to ⦋ {Poly}_{1} (r) / p ⦌ ⦋ {Base}_{p} / b ⦌ (f \in b, g \in b ⟼ (ι q \in b \| \deg_{1} (r) (f -_{p} (q \cdot_{p} g)) < \deg_{1} (r) (g))) = ⦋ P / p ⦌ ⦋ {Base}_{p} / b ⦌ (f \in b, g \in b ⟼ (ι q \in b \| \deg_{1} (r) (f -_{p} (q \cdot_{p} g)) < \deg_{1} (r) (g)))$
11	2	fvexi	$⊢ P \in V$
12	11	a1i	$⊢ r = R \to P \in V$
13		fveq2	$⊢ p = P \to {Base}_{p} = {Base}_{P}$
14	13	adantl	$⊢ (r = R \land p = P) \to {Base}_{p} = {Base}_{P}$
15	14 3	eqtr4di	$⊢ (r = R \land p = P) \to {Base}_{p} = B$
16	15	csbeq1d	$⊢ (r = R \land p = P) \to ⦋ {Base}_{p} / b ⦌ (f \in b, g \in b ⟼ (ι q \in b \| \deg_{1} (r) (f -_{p} (q \cdot_{p} g)) < \deg_{1} (r) (g))) = ⦋ B / b ⦌ (f \in b, g \in b ⟼ (ι q \in b \| \deg_{1} (r) (f -_{p} (q \cdot_{p} g)) < \deg_{1} (r) (g)))$
17	3	fvexi	$⊢ B \in V$
18	17	a1i	$⊢ (r = R \land p = P) \to B \in V$
19		simpr	$⊢ ((r = R \land p = P) \land b = B) \to b = B$
20		fveq2	$⊢ r = R \to \deg_{1} (r) = \deg_{1} (R)$
21	20	ad2antrr	$⊢ ((r = R \land p = P) \land b = B) \to \deg_{1} (r) = \deg_{1} (R)$
22	21 4	eqtr4di	$⊢ ((r = R \land p = P) \land b = B) \to \deg_{1} (r) = D$
23		fveq2	$⊢ p = P \to -_{p} = -_{P}$
24	23	ad2antlr	$⊢ ((r = R \land p = P) \land b = B) \to -_{p} = -_{P}$
25	24 5	eqtr4di	$⊢ ((r = R \land p = P) \land b = B) \to -_{p} = \underset{˙}{-}$
26		eqidd	$⊢ ((r = R \land p = P) \land b = B) \to f = f$
27		fveq2	$⊢ p = P \to \cdot_{p} = \cdot_{P}$
28	27	ad2antlr	$⊢ ((r = R \land p = P) \land b = B) \to \cdot_{p} = \cdot_{P}$
29	28 6	eqtr4di	$⊢ ((r = R \land p = P) \land b = B) \to \cdot_{p} = \underset{˙}{\cdot}$
30	29	oveqd	$⊢ ((r = R \land p = P) \land b = B) \to q \cdot_{p} g = q \underset{˙}{\cdot} g$
31	25 26 30	oveq123d	$⊢ ((r = R \land p = P) \land b = B) \to f -_{p} (q \cdot_{p} g) = f \underset{˙}{-} (q \underset{˙}{\cdot} g)$
32	22 31	fveq12d	$⊢ ((r = R \land p = P) \land b = B) \to \deg_{1} (r) (f -_{p} (q \cdot_{p} g)) = D (f \underset{˙}{-} (q \underset{˙}{\cdot} g))$
33	22	fveq1d	$⊢ ((r = R \land p = P) \land b = B) \to \deg_{1} (r) (g) = D (g)$
34	32 33	breq12d	$⊢ ((r = R \land p = P) \land b = B) \to (\deg_{1} (r) (f -_{p} (q \cdot_{p} g)) < \deg_{1} (r) (g) \leftrightarrow D (f \underset{˙}{-} (q \underset{˙}{\cdot} g)) < D (g))$
35	19 34	riotaeqbidv	$⊢ ((r = R \land p = P) \land b = B) \to (ι q \in b \| \deg_{1} (r) (f -_{p} (q \cdot_{p} g)) < \deg_{1} (r) (g)) = (ι q \in B \| D (f \underset{˙}{-} (q \underset{˙}{\cdot} g)) < D (g))$
36	19 19 35	mpoeq123dv	$⊢ ((r = R \land p = P) \land b = B) \to (f \in b, g \in b ⟼ (ι q \in b \| \deg_{1} (r) (f -_{p} (q \cdot_{p} g)) < \deg_{1} (r) (g))) = (f \in B, g \in B ⟼ (ι q \in B \| D (f \underset{˙}{-} (q \underset{˙}{\cdot} g)) < D (g)))$
37	18 36	csbied	$⊢ (r = R \land p = P) \to ⦋ B / b ⦌ (f \in b, g \in b ⟼ (ι q \in b \| \deg_{1} (r) (f -_{p} (q \cdot_{p} g)) < \deg_{1} (r) (g))) = (f \in B, g \in B ⟼ (ι q \in B \| D (f \underset{˙}{-} (q \underset{˙}{\cdot} g)) < D (g)))$
38	16 37	eqtrd	$⊢ (r = R \land p = P) \to ⦋ {Base}_{p} / b ⦌ (f \in b, g \in b ⟼ (ι q \in b \| \deg_{1} (r) (f -_{p} (q \cdot_{p} g)) < \deg_{1} (r) (g))) = (f \in B, g \in B ⟼ (ι q \in B \| D (f \underset{˙}{-} (q \underset{˙}{\cdot} g)) < D (g)))$
39	12 38	csbied	$⊢ r = R \to ⦋ P / p ⦌ ⦋ {Base}_{p} / b ⦌ (f \in b, g \in b ⟼ (ι q \in b \| \deg_{1} (r) (f -_{p} (q \cdot_{p} g)) < \deg_{1} (r) (g))) = (f \in B, g \in B ⟼ (ι q \in B \| D (f \underset{˙}{-} (q \underset{˙}{\cdot} g)) < D (g)))$
40	10 39	eqtrd	$⊢ r = R \to ⦋ {Poly}_{1} (r) / p ⦌ ⦋ {Base}_{p} / b ⦌ (f \in b, g \in b ⟼ (ι q \in b \| \deg_{1} (r) (f -_{p} (q \cdot_{p} g)) < \deg_{1} (r) (g))) = (f \in B, g \in B ⟼ (ι q \in B \| D (f \underset{˙}{-} (q \underset{˙}{\cdot} g)) < D (g)))$
41		df-q1p	$⊢ {quot}_{1p} = (r \in V ⟼ ⦋ {Poly}_{1} (r) / p ⦌ ⦋ {Base}_{p} / b ⦌ (f \in b, g \in b ⟼ (ι q \in b \| \deg_{1} (r) (f -_{p} (q \cdot_{p} g)) < \deg_{1} (r) (g))))$
42	17 17	mpoex	$⊢ (f \in B, g \in B ⟼ (ι q \in B \| D (f \underset{˙}{-} (q \underset{˙}{\cdot} g)) < D (g))) \in V$
43	40 41 42	fvmpt	$⊢ R \in V \to {quot}_{1p} (R) = (f \in B, g \in B ⟼ (ι q \in B \| D (f \underset{˙}{-} (q \underset{˙}{\cdot} g)) < D (g)))$
44	1 43	syl5eq	$⊢ R \in V \to Q = (f \in B, g \in B ⟼ (ι q \in B \| D (f \underset{˙}{-} (q \underset{˙}{\cdot} g)) < D (g)))$
45	7 44	syl	$⊢ G \in B \to Q = (f \in B, g \in B ⟼ (ι q \in B \| D (f \underset{˙}{-} (q \underset{˙}{\cdot} g)) < D (g)))$
46	45	adantl	$⊢ (F \in B \land G \in B) \to Q = (f \in B, g \in B ⟼ (ι q \in B \| D (f \underset{˙}{-} (q \underset{˙}{\cdot} g)) < D (g)))$
47		id	$⊢ f = F \to f = F$
48		oveq2	$⊢ g = G \to q \underset{˙}{\cdot} g = q \underset{˙}{\cdot} G$
49	47 48	oveqan12d	$⊢ (f = F \land g = G) \to f \underset{˙}{-} (q \underset{˙}{\cdot} g) = F \underset{˙}{-} (q \underset{˙}{\cdot} G)$
50	49	fveq2d	$⊢ (f = F \land g = G) \to D (f \underset{˙}{-} (q \underset{˙}{\cdot} g)) = D (F \underset{˙}{-} (q \underset{˙}{\cdot} G))$
51		fveq2	$⊢ g = G \to D (g) = D (G)$
52	51	adantl	$⊢ (f = F \land g = G) \to D (g) = D (G)$
53	50 52	breq12d	$⊢ (f = F \land g = G) \to (D (f \underset{˙}{-} (q \underset{˙}{\cdot} g)) < D (g) \leftrightarrow D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G))$
54	53	riotabidv	$⊢ (f = F \land g = G) \to (ι q \in B \| D (f \underset{˙}{-} (q \underset{˙}{\cdot} g)) < D (g)) = (ι q \in B \| D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G))$
55	54	adantl	$⊢ ((F \in B \land G \in B) \land (f = F \land g = G)) \to (ι q \in B \| D (f \underset{˙}{-} (q \underset{˙}{\cdot} g)) < D (g)) = (ι q \in B \| D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G))$
56		simpl	$⊢ (F \in B \land G \in B) \to F \in B$
57		simpr	$⊢ (F \in B \land G \in B) \to G \in B$
58		riotaex	$⊢ (ι q \in B \| D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G)) \in V$
59	58	a1i	$⊢ (F \in B \land G \in B) \to (ι q \in B \| D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G)) \in V$
60	46 55 56 57 59	ovmpod	$⊢ (F \in B \land G \in B) \to F Q G = (ι q \in B \| D (F \underset{˙}{-} (q \underset{˙}{\cdot} G)) < D (G))$

Metamath Proof Explorer

Theorem q1pval

Proof