Theorem r1pval

Description: Value of the polynomial remainder function. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	r1pval.e	$$⊢E={rem}_{\mathrm{1p}}\left(R\right)$$
	r1pval.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	r1pval.b	$$⊢B={\mathrm{Base}}_P$$
	r1pval.q	$$⊢Q={quot}_{\mathrm{1p}}\left(R\right)$$
	r1pval.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	r1pval.m	$$⊢\underset{\dot{}}{-}={-}_P$$
Assertion	r1pval	$$⊢\left(F\in B\wedge G\in B\right)\to FEG=F\underset{\dot{}}{-}\left(\left(FQG\right)\underset{\dot{}}{·}G\right)$$

Proof

Step	Hyp	Ref	Expression
1		r1pval.e	$$⊢E={rem}_{\mathrm{1p}}\left(R\right)$$
2		r1pval.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		r1pval.b	$$⊢B={\mathrm{Base}}_P$$
4		r1pval.q	$$⊢Q={quot}_{\mathrm{1p}}\left(R\right)$$
5		r1pval.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
6		r1pval.m	$$⊢\underset{\dot{}}{-}={-}_P$$
7	2 3	elbasfv	$$⊢F\in B\to R\in \mathrm{V}$$
8	7	adantr	$$⊢\left(F\in B\wedge G\in B\right)\to R\in \mathrm{V}$$
9		fveq2	$$⊢r=R\to {\mathrm{Poly}}_1\left(r\right)={\mathrm{Poly}}_1\left(R\right)$$
10	9 2	eqtr4di	$$⊢r=R\to {\mathrm{Poly}}_1\left(r\right)=P$$
11	10	fveq2d	$$⊢r=R\to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}={\mathrm{Base}}_P$$
12	11 3	eqtr4di	$$⊢r=R\to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}=B$$
13	12	csbeq1d	$$⊢r=R\to ⦋{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}/b⦌\left(f\in b,g\in b⟼f{-}_{{\mathrm{Poly}}_1\left(r\right)}\left(\left(f{quot}_{\mathrm{1p}}\left(r\right)g\right){\cdot }_{{\mathrm{Poly}}_1\left(r\right)}g\right)\right)=⦋B/b⦌\left(f\in b,g\in b⟼f{-}_{{\mathrm{Poly}}_1\left(r\right)}\left(\left(f{quot}_{\mathrm{1p}}\left(r\right)g\right){\cdot }_{{\mathrm{Poly}}_1\left(r\right)}g\right)\right)$$
14	3	fvexi	$$⊢B\in \mathrm{V}$$
15	14	a1i	$$⊢r=R\to B\in \mathrm{V}$$
16		simpr	$$⊢\left(r=R\wedge b=B\right)\to b=B$$
17	10	fveq2d	$$⊢r=R\to {-}_{{\mathrm{Poly}}_1\left(r\right)}={-}_P$$
18	17 6	eqtr4di	$$⊢r=R\to {-}_{{\mathrm{Poly}}_1\left(r\right)}=\underset{\dot{}}{-}$$
19		eqidd	$$⊢r=R\to f=f$$
20	10	fveq2d	$$⊢r=R\to {\cdot }_{{\mathrm{Poly}}_1\left(r\right)}={\cdot }_P$$
21	20 5	eqtr4di	$$⊢r=R\to {\cdot }_{{\mathrm{Poly}}_1\left(r\right)}=\underset{\dot{}}{·}$$
22		fveq2	$$⊢r=R\to {quot}_{\mathrm{1p}}\left(r\right)={quot}_{\mathrm{1p}}\left(R\right)$$
23	22 4	eqtr4di	$$⊢r=R\to {quot}_{\mathrm{1p}}\left(r\right)=Q$$
24	23	oveqd	$$⊢r=R\to f{quot}_{\mathrm{1p}}\left(r\right)g=fQg$$
25		eqidd	$$⊢r=R\to g=g$$
26	21 24 25	oveq123d	$$⊢r=R\to \left(f{quot}_{\mathrm{1p}}\left(r\right)g\right){\cdot }_{{\mathrm{Poly}}_1\left(r\right)}g=\left(fQg\right)\underset{\dot{}}{·}g$$
27	18 19 26	oveq123d	$$⊢r=R\to f{-}_{{\mathrm{Poly}}_1\left(r\right)}\left(\left(f{quot}_{\mathrm{1p}}\left(r\right)g\right){\cdot }_{{\mathrm{Poly}}_1\left(r\right)}g\right)=f\underset{\dot{}}{-}\left(\left(fQg\right)\underset{\dot{}}{·}g\right)$$
28	27	adantr	$$⊢\left(r=R\wedge b=B\right)\to f{-}_{{\mathrm{Poly}}_1\left(r\right)}\left(\left(f{quot}_{\mathrm{1p}}\left(r\right)g\right){\cdot }_{{\mathrm{Poly}}_1\left(r\right)}g\right)=f\underset{\dot{}}{-}\left(\left(fQg\right)\underset{\dot{}}{·}g\right)$$
29	16 16 28	mpoeq123dv	$$⊢\left(r=R\wedge b=B\right)\to \left(f\in b,g\in b⟼f{-}_{{\mathrm{Poly}}_1\left(r\right)}\left(\left(f{quot}_{\mathrm{1p}}\left(r\right)g\right){\cdot }_{{\mathrm{Poly}}_1\left(r\right)}g\right)\right)=\left(f\in B,g\in B⟼f\underset{\dot{}}{-}\left(\left(fQg\right)\underset{\dot{}}{·}g\right)\right)$$
30	15 29	csbied	$$⊢r=R\to ⦋B/b⦌\left(f\in b,g\in b⟼f{-}_{{\mathrm{Poly}}_1\left(r\right)}\left(\left(f{quot}_{\mathrm{1p}}\left(r\right)g\right){\cdot }_{{\mathrm{Poly}}_1\left(r\right)}g\right)\right)=\left(f\in B,g\in B⟼f\underset{\dot{}}{-}\left(\left(fQg\right)\underset{\dot{}}{·}g\right)\right)$$
31	13 30	eqtrd	$$⊢r=R\to ⦋{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}/b⦌\left(f\in b,g\in b⟼f{-}_{{\mathrm{Poly}}_1\left(r\right)}\left(\left(f{quot}_{\mathrm{1p}}\left(r\right)g\right){\cdot }_{{\mathrm{Poly}}_1\left(r\right)}g\right)\right)=\left(f\in B,g\in B⟼f\underset{\dot{}}{-}\left(\left(fQg\right)\underset{\dot{}}{·}g\right)\right)$$
32		df-r1p	$$⊢{rem}_{\mathrm{1p}}=\left(r\in \mathrm{V}⟼⦋{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(r\right)}/b⦌\left(f\in b,g\in b⟼f{-}_{{\mathrm{Poly}}_1\left(r\right)}\left(\left(f{quot}_{\mathrm{1p}}\left(r\right)g\right){\cdot }_{{\mathrm{Poly}}_1\left(r\right)}g\right)\right)\right)$$
33	14 14	mpoex	$$⊢\left(f\in B,g\in B⟼f\underset{\dot{}}{-}\left(\left(fQg\right)\underset{\dot{}}{·}g\right)\right)\in \mathrm{V}$$
34	31 32 33	fvmpt	$$⊢R\in \mathrm{V}\to {rem}_{\mathrm{1p}}\left(R\right)=\left(f\in B,g\in B⟼f\underset{\dot{}}{-}\left(\left(fQg\right)\underset{\dot{}}{·}g\right)\right)$$
35	1 34	syl5eq	$$⊢R\in \mathrm{V}\to E=\left(f\in B,g\in B⟼f\underset{\dot{}}{-}\left(\left(fQg\right)\underset{\dot{}}{·}g\right)\right)$$
36	8 35	syl	$$⊢\left(F\in B\wedge G\in B\right)\to E=\left(f\in B,g\in B⟼f\underset{\dot{}}{-}\left(\left(fQg\right)\underset{\dot{}}{·}g\right)\right)$$
37		simpl	$$⊢\left(f=F\wedge g=G\right)\to f=F$$
38		oveq12	$$⊢\left(f=F\wedge g=G\right)\to fQg=FQG$$
39		simpr	$$⊢\left(f=F\wedge g=G\right)\to g=G$$
40	38 39	oveq12d	$$⊢\left(f=F\wedge g=G\right)\to \left(fQg\right)\underset{\dot{}}{·}g=\left(FQG\right)\underset{\dot{}}{·}G$$
41	37 40	oveq12d	$$⊢\left(f=F\wedge g=G\right)\to f\underset{\dot{}}{-}\left(\left(fQg\right)\underset{\dot{}}{·}g\right)=F\underset{\dot{}}{-}\left(\left(FQG\right)\underset{\dot{}}{·}G\right)$$
42	41	adantl	$$⊢\left(\left(F\in B\wedge G\in B\right)\wedge \left(f=F\wedge g=G\right)\right)\to f\underset{\dot{}}{-}\left(\left(fQg\right)\underset{\dot{}}{·}g\right)=F\underset{\dot{}}{-}\left(\left(FQG\right)\underset{\dot{}}{·}G\right)$$
43		simpl	$$⊢\left(F\in B\wedge G\in B\right)\to F\in B$$
44		simpr	$$⊢\left(F\in B\wedge G\in B\right)\to G\in B$$
45		ovexd	$$⊢\left(F\in B\wedge G\in B\right)\to F\underset{\dot{}}{-}\left(\left(FQG\right)\underset{\dot{}}{·}G\right)\in \mathrm{V}$$
46	36 42 43 44 45	ovmpod	$$⊢\left(F\in B\wedge G\in B\right)\to FEG=F\underset{\dot{}}{-}\left(\left(FQG\right)\underset{\dot{}}{·}G\right)$$