r1pval

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

	Ref	Expression
Hypotheses	r1pval.e	⊢ 𝐸 = ( rem_1p ‘ 𝑅 )
	r1pval.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	r1pval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	r1pval.q	⊢ 𝑄 = ( quot_1p ‘ 𝑅 )
	r1pval.t	⊢ · = ( ._r ‘ 𝑃 )
	r1pval.m	⊢ − = ( -_g ‘ 𝑃 )
Assertion	r1pval	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 𝐸 𝐺 ) = ( 𝐹 − ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		r1pval.e	⊢ 𝐸 = ( rem_1p ‘ 𝑅 )
2		r1pval.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
3		r1pval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		r1pval.q	⊢ 𝑄 = ( quot_1p ‘ 𝑅 )
5		r1pval.t	⊢ · = ( ._r ‘ 𝑃 )
6		r1pval.m	⊢ − = ( -_g ‘ 𝑃 )
7	2 3	elbasfv	⊢ ( 𝐹 ∈ 𝐵 → 𝑅 ∈ V )
8	7	adantr	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝑅 ∈ V )
9		fveq2	⊢ ( 𝑟 = 𝑅 → ( Poly₁ ‘ 𝑟 ) = ( Poly₁ ‘ 𝑅 ) )
10	9 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( Poly₁ ‘ 𝑟 ) = 𝑃 )
11	10	fveq2d	⊢ ( 𝑟 = 𝑅 → ( Base ‘ ( Poly₁ ‘ 𝑟 ) ) = ( Base ‘ 𝑃 ) )
12	11 3	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( Base ‘ ( Poly₁ ‘ 𝑟 ) ) = 𝐵 )
13	12	csbeq1d	⊢ ( 𝑟 = 𝑅 → ⦋ ( Base ‘ ( Poly₁ ‘ 𝑟 ) ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ( -_g ‘ ( Poly₁ ‘ 𝑟 ) ) ( ( 𝑓 ( quot_1p ‘ 𝑟 ) 𝑔 ) ( ._r ‘ ( Poly₁ ‘ 𝑟 ) ) 𝑔 ) ) ) = ⦋ 𝐵 / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ( -_g ‘ ( Poly₁ ‘ 𝑟 ) ) ( ( 𝑓 ( quot_1p ‘ 𝑟 ) 𝑔 ) ( ._r ‘ ( Poly₁ ‘ 𝑟 ) ) 𝑔 ) ) ) )
14	3	fvexi	⊢ 𝐵 ∈ V
15	14	a1i	⊢ ( 𝑟 = 𝑅 → 𝐵 ∈ V )
16		simpr	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
17	10	fveq2d	⊢ ( 𝑟 = 𝑅 → ( -_g ‘ ( Poly₁ ‘ 𝑟 ) ) = ( -_g ‘ 𝑃 ) )
18	17 6	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( -_g ‘ ( Poly₁ ‘ 𝑟 ) ) = − )
19		eqidd	⊢ ( 𝑟 = 𝑅 → 𝑓 = 𝑓 )
20	10	fveq2d	⊢ ( 𝑟 = 𝑅 → ( ._r ‘ ( Poly₁ ‘ 𝑟 ) ) = ( ._r ‘ 𝑃 ) )
21	20 5	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( ._r ‘ ( Poly₁ ‘ 𝑟 ) ) = · )
22		fveq2	⊢ ( 𝑟 = 𝑅 → ( quot_1p ‘ 𝑟 ) = ( quot_1p ‘ 𝑅 ) )
23	22 4	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( quot_1p ‘ 𝑟 ) = 𝑄 )
24	23	oveqd	⊢ ( 𝑟 = 𝑅 → ( 𝑓 ( quot_1p ‘ 𝑟 ) 𝑔 ) = ( 𝑓 𝑄 𝑔 ) )
25		eqidd	⊢ ( 𝑟 = 𝑅 → 𝑔 = 𝑔 )
26	21 24 25	oveq123d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑓 ( quot_1p ‘ 𝑟 ) 𝑔 ) ( ._r ‘ ( Poly₁ ‘ 𝑟 ) ) 𝑔 ) = ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) )
27	18 19 26	oveq123d	⊢ ( 𝑟 = 𝑅 → ( 𝑓 ( -_g ‘ ( Poly₁ ‘ 𝑟 ) ) ( ( 𝑓 ( quot_1p ‘ 𝑟 ) 𝑔 ) ( ._r ‘ ( Poly₁ ‘ 𝑟 ) ) 𝑔 ) ) = ( 𝑓 − ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) )
28	27	adantr	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( 𝑓 ( -_g ‘ ( Poly₁ ‘ 𝑟 ) ) ( ( 𝑓 ( quot_1p ‘ 𝑟 ) 𝑔 ) ( ._r ‘ ( Poly₁ ‘ 𝑟 ) ) 𝑔 ) ) = ( 𝑓 − ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) )
29	16 16 28	mpoeq123dv	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ( -_g ‘ ( Poly₁ ‘ 𝑟 ) ) ( ( 𝑓 ( quot_1p ‘ 𝑟 ) 𝑔 ) ( ._r ‘ ( Poly₁ ‘ 𝑟 ) ) 𝑔 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 − ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) ) )
30	15 29	csbied	⊢ ( 𝑟 = 𝑅 → ⦋ 𝐵 / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ( -_g ‘ ( Poly₁ ‘ 𝑟 ) ) ( ( 𝑓 ( quot_1p ‘ 𝑟 ) 𝑔 ) ( ._r ‘ ( Poly₁ ‘ 𝑟 ) ) 𝑔 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 − ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) ) )
31	13 30	eqtrd	⊢ ( 𝑟 = 𝑅 → ⦋ ( Base ‘ ( Poly₁ ‘ 𝑟 ) ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ( -_g ‘ ( Poly₁ ‘ 𝑟 ) ) ( ( 𝑓 ( quot_1p ‘ 𝑟 ) 𝑔 ) ( ._r ‘ ( Poly₁ ‘ 𝑟 ) ) 𝑔 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 − ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) ) )
32		df-r1p	⊢ rem_1p = ( 𝑟 ∈ V ↦ ⦋ ( Base ‘ ( Poly₁ ‘ 𝑟 ) ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ( -_g ‘ ( Poly₁ ‘ 𝑟 ) ) ( ( 𝑓 ( quot_1p ‘ 𝑟 ) 𝑔 ) ( ._r ‘ ( Poly₁ ‘ 𝑟 ) ) 𝑔 ) ) ) )
33	14 14	mpoex	⊢ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 − ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) ) ∈ V
34	31 32 33	fvmpt	⊢ ( 𝑅 ∈ V → ( rem_1p ‘ 𝑅 ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 − ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) ) )
35	1 34	eqtrid	⊢ ( 𝑅 ∈ V → 𝐸 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 − ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) ) )
36	8 35	syl	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐸 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 − ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) ) )
37		simpl	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → 𝑓 = 𝐹 )
38		oveq12	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 𝑄 𝑔 ) = ( 𝐹 𝑄 𝐺 ) )
39		simpr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
40	38 39	oveq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) = ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) )
41	37 40	oveq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 − ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) = ( 𝐹 − ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )
42	41	adantl	⊢ ( ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( 𝑓 − ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) = ( 𝐹 − ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )
43		simpl	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐹 ∈ 𝐵 )
44		simpr	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
45		ovexd	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 − ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) ∈ V )
46	36 42 43 44 45	ovmpod	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 𝐸 𝐺 ) = ( 𝐹 − ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )

Metamath Proof Explorer

Theorem r1pval

Proof