Metamath Proof Explorer


Theorem r1pval

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

Ref Expression
Hypotheses r1pval.e 𝐸 = ( rem1p𝑅 )
r1pval.p 𝑃 = ( Poly1𝑅 )
r1pval.b 𝐵 = ( Base ‘ 𝑃 )
r1pval.q 𝑄 = ( quot1p𝑅 )
r1pval.t · = ( .r𝑃 )
r1pval.m = ( -g𝑃 )
Assertion r1pval ( ( 𝐹𝐵𝐺𝐵 ) → ( 𝐹 𝐸 𝐺 ) = ( 𝐹 ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 r1pval.e 𝐸 = ( rem1p𝑅 )
2 r1pval.p 𝑃 = ( Poly1𝑅 )
3 r1pval.b 𝐵 = ( Base ‘ 𝑃 )
4 r1pval.q 𝑄 = ( quot1p𝑅 )
5 r1pval.t · = ( .r𝑃 )
6 r1pval.m = ( -g𝑃 )
7 2 3 elbasfv ( 𝐹𝐵𝑅 ∈ V )
8 7 adantr ( ( 𝐹𝐵𝐺𝐵 ) → 𝑅 ∈ V )
9 fveq2 ( 𝑟 = 𝑅 → ( Poly1𝑟 ) = ( Poly1𝑅 ) )
10 9 2 eqtr4di ( 𝑟 = 𝑅 → ( Poly1𝑟 ) = 𝑃 )
11 10 fveq2d ( 𝑟 = 𝑅 → ( Base ‘ ( Poly1𝑟 ) ) = ( Base ‘ 𝑃 ) )
12 11 3 eqtr4di ( 𝑟 = 𝑅 → ( Base ‘ ( Poly1𝑟 ) ) = 𝐵 )
13 12 csbeq1d ( 𝑟 = 𝑅 ( Base ‘ ( Poly1𝑟 ) ) / 𝑏 ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓 ( -g ‘ ( Poly1𝑟 ) ) ( ( 𝑓 ( quot1p𝑟 ) 𝑔 ) ( .r ‘ ( Poly1𝑟 ) ) 𝑔 ) ) ) = 𝐵 / 𝑏 ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓 ( -g ‘ ( Poly1𝑟 ) ) ( ( 𝑓 ( quot1p𝑟 ) 𝑔 ) ( .r ‘ ( Poly1𝑟 ) ) 𝑔 ) ) ) )
14 3 fvexi 𝐵 ∈ V
15 14 a1i ( 𝑟 = 𝑅𝐵 ∈ V )
16 simpr ( ( 𝑟 = 𝑅𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
17 10 fveq2d ( 𝑟 = 𝑅 → ( -g ‘ ( Poly1𝑟 ) ) = ( -g𝑃 ) )
18 17 6 eqtr4di ( 𝑟 = 𝑅 → ( -g ‘ ( Poly1𝑟 ) ) = )
19 eqidd ( 𝑟 = 𝑅𝑓 = 𝑓 )
20 10 fveq2d ( 𝑟 = 𝑅 → ( .r ‘ ( Poly1𝑟 ) ) = ( .r𝑃 ) )
21 20 5 eqtr4di ( 𝑟 = 𝑅 → ( .r ‘ ( Poly1𝑟 ) ) = · )
22 fveq2 ( 𝑟 = 𝑅 → ( quot1p𝑟 ) = ( quot1p𝑅 ) )
23 22 4 eqtr4di ( 𝑟 = 𝑅 → ( quot1p𝑟 ) = 𝑄 )
24 23 oveqd ( 𝑟 = 𝑅 → ( 𝑓 ( quot1p𝑟 ) 𝑔 ) = ( 𝑓 𝑄 𝑔 ) )
25 eqidd ( 𝑟 = 𝑅𝑔 = 𝑔 )
26 21 24 25 oveq123d ( 𝑟 = 𝑅 → ( ( 𝑓 ( quot1p𝑟 ) 𝑔 ) ( .r ‘ ( Poly1𝑟 ) ) 𝑔 ) = ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) )
27 18 19 26 oveq123d ( 𝑟 = 𝑅 → ( 𝑓 ( -g ‘ ( Poly1𝑟 ) ) ( ( 𝑓 ( quot1p𝑟 ) 𝑔 ) ( .r ‘ ( Poly1𝑟 ) ) 𝑔 ) ) = ( 𝑓 ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) )
28 27 adantr ( ( 𝑟 = 𝑅𝑏 = 𝐵 ) → ( 𝑓 ( -g ‘ ( Poly1𝑟 ) ) ( ( 𝑓 ( quot1p𝑟 ) 𝑔 ) ( .r ‘ ( Poly1𝑟 ) ) 𝑔 ) ) = ( 𝑓 ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) )
29 16 16 28 mpoeq123dv ( ( 𝑟 = 𝑅𝑏 = 𝐵 ) → ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓 ( -g ‘ ( Poly1𝑟 ) ) ( ( 𝑓 ( quot1p𝑟 ) 𝑔 ) ( .r ‘ ( Poly1𝑟 ) ) 𝑔 ) ) ) = ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑓 ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) ) )
30 15 29 csbied ( 𝑟 = 𝑅 𝐵 / 𝑏 ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓 ( -g ‘ ( Poly1𝑟 ) ) ( ( 𝑓 ( quot1p𝑟 ) 𝑔 ) ( .r ‘ ( Poly1𝑟 ) ) 𝑔 ) ) ) = ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑓 ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) ) )
31 13 30 eqtrd ( 𝑟 = 𝑅 ( Base ‘ ( Poly1𝑟 ) ) / 𝑏 ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓 ( -g ‘ ( Poly1𝑟 ) ) ( ( 𝑓 ( quot1p𝑟 ) 𝑔 ) ( .r ‘ ( Poly1𝑟 ) ) 𝑔 ) ) ) = ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑓 ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) ) )
32 df-r1p rem1p = ( 𝑟 ∈ V ↦ ( Base ‘ ( Poly1𝑟 ) ) / 𝑏 ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓 ( -g ‘ ( Poly1𝑟 ) ) ( ( 𝑓 ( quot1p𝑟 ) 𝑔 ) ( .r ‘ ( Poly1𝑟 ) ) 𝑔 ) ) ) )
33 14 14 mpoex ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑓 ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) ) ∈ V
34 31 32 33 fvmpt ( 𝑅 ∈ V → ( rem1p𝑅 ) = ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑓 ( ( 𝑓 𝑄 𝑔 ) · 𝑔 ) ) ) )
35 1 34 syl5eq ( 𝑅 ∈ 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 ( ( 𝐹𝐵𝐺𝐵 ) → ( 𝐹 𝐸 𝐺 ) = ( 𝐹 ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )