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 
|- E = ( rem1p ` R )
r1pval.p 
|- P = ( Poly1 ` R )
r1pval.b 
|- B = ( Base ` P )
r1pval.q 
|- Q = ( quot1p ` R )
r1pval.t 
|- .x. = ( .r ` P )
r1pval.m 
|- .- = ( -g ` P )
Assertion r1pval 
|- ( ( F e. B /\ G e. B ) -> ( F E G ) = ( F .- ( ( F Q G ) .x. G ) ) )

Proof

Step Hyp Ref Expression
1 r1pval.e 
 |-  E = ( rem1p ` R )
2 r1pval.p 
 |-  P = ( Poly1 ` R )
3 r1pval.b 
 |-  B = ( Base ` P )
4 r1pval.q 
 |-  Q = ( quot1p ` R )
5 r1pval.t 
 |-  .x. = ( .r ` P )
6 r1pval.m 
 |-  .- = ( -g ` P )
7 2 3 elbasfv 
 |-  ( F e. B -> R e. _V )
8 7 adantr 
 |-  ( ( F e. B /\ G e. B ) -> R e. _V )
9 fveq2 
 |-  ( r = R -> ( Poly1 ` r ) = ( Poly1 ` R ) )
10 9 2 eqtr4di 
 |-  ( r = R -> ( Poly1 ` r ) = P )
11 10 fveq2d 
 |-  ( r = R -> ( Base ` ( Poly1 ` r ) ) = ( Base ` P ) )
12 11 3 eqtr4di 
 |-  ( r = R -> ( Base ` ( Poly1 ` r ) ) = B )
13 12 csbeq1d 
 |-  ( r = R -> [_ ( Base ` ( Poly1 ` r ) ) / b ]_ ( f e. b , g e. b |-> ( f ( -g ` ( Poly1 ` r ) ) ( ( f ( quot1p ` r ) g ) ( .r ` ( Poly1 ` r ) ) g ) ) ) = [_ B / b ]_ ( f e. b , g e. b |-> ( f ( -g ` ( Poly1 ` r ) ) ( ( f ( quot1p ` r ) g ) ( .r ` ( Poly1 ` r ) ) g ) ) ) )
14 3 fvexi 
 |-  B e. _V
15 14 a1i 
 |-  ( r = R -> B e. _V )
16 simpr 
 |-  ( ( r = R /\ b = B ) -> b = B )
17 10 fveq2d 
 |-  ( r = R -> ( -g ` ( Poly1 ` r ) ) = ( -g ` P ) )
18 17 6 eqtr4di 
 |-  ( r = R -> ( -g ` ( Poly1 ` r ) ) = .- )
19 eqidd 
 |-  ( r = R -> f = f )
20 10 fveq2d 
 |-  ( r = R -> ( .r ` ( Poly1 ` r ) ) = ( .r ` P ) )
21 20 5 eqtr4di 
 |-  ( r = R -> ( .r ` ( Poly1 ` r ) ) = .x. )
22 fveq2 
 |-  ( r = R -> ( quot1p ` r ) = ( quot1p ` R ) )
23 22 4 eqtr4di 
 |-  ( r = R -> ( quot1p ` r ) = Q )
24 23 oveqd 
 |-  ( r = R -> ( f ( quot1p ` r ) g ) = ( f Q g ) )
25 eqidd 
 |-  ( r = R -> g = g )
26 21 24 25 oveq123d 
 |-  ( r = R -> ( ( f ( quot1p ` r ) g ) ( .r ` ( Poly1 ` r ) ) g ) = ( ( f Q g ) .x. g ) )
27 18 19 26 oveq123d 
 |-  ( r = R -> ( f ( -g ` ( Poly1 ` r ) ) ( ( f ( quot1p ` r ) g ) ( .r ` ( Poly1 ` r ) ) g ) ) = ( f .- ( ( f Q g ) .x. g ) ) )
28 27 adantr 
 |-  ( ( r = R /\ b = B ) -> ( f ( -g ` ( Poly1 ` r ) ) ( ( f ( quot1p ` r ) g ) ( .r ` ( Poly1 ` r ) ) g ) ) = ( f .- ( ( f Q g ) .x. g ) ) )
29 16 16 28 mpoeq123dv 
 |-  ( ( r = R /\ b = B ) -> ( f e. b , g e. b |-> ( f ( -g ` ( Poly1 ` r ) ) ( ( f ( quot1p ` r ) g ) ( .r ` ( Poly1 ` r ) ) g ) ) ) = ( f e. B , g e. B |-> ( f .- ( ( f Q g ) .x. g ) ) ) )
30 15 29 csbied 
 |-  ( r = R -> [_ B / b ]_ ( f e. b , g e. b |-> ( f ( -g ` ( Poly1 ` r ) ) ( ( f ( quot1p ` r ) g ) ( .r ` ( Poly1 ` r ) ) g ) ) ) = ( f e. B , g e. B |-> ( f .- ( ( f Q g ) .x. g ) ) ) )
31 13 30 eqtrd 
 |-  ( r = R -> [_ ( Base ` ( Poly1 ` r ) ) / b ]_ ( f e. b , g e. b |-> ( f ( -g ` ( Poly1 ` r ) ) ( ( f ( quot1p ` r ) g ) ( .r ` ( Poly1 ` r ) ) g ) ) ) = ( f e. B , g e. B |-> ( f .- ( ( f Q g ) .x. g ) ) ) )
32 df-r1p 
 |-  rem1p = ( r e. _V |-> [_ ( Base ` ( Poly1 ` r ) ) / b ]_ ( f e. b , g e. b |-> ( f ( -g ` ( Poly1 ` r ) ) ( ( f ( quot1p ` r ) g ) ( .r ` ( Poly1 ` r ) ) g ) ) ) )
33 14 14 mpoex 
 |-  ( f e. B , g e. B |-> ( f .- ( ( f Q g ) .x. g ) ) ) e. _V
34 31 32 33 fvmpt 
 |-  ( R e. _V -> ( rem1p ` R ) = ( f e. B , g e. B |-> ( f .- ( ( f Q g ) .x. g ) ) ) )
35 1 34 syl5eq 
 |-  ( R e. _V -> E = ( f e. B , g e. B |-> ( f .- ( ( f Q g ) .x. g ) ) ) )
36 8 35 syl 
 |-  ( ( F e. B /\ G e. B ) -> E = ( f e. B , g e. B |-> ( f .- ( ( f Q g ) .x. g ) ) ) )
37 simpl 
 |-  ( ( f = F /\ g = G ) -> f = F )
38 oveq12 
 |-  ( ( f = F /\ g = G ) -> ( f Q g ) = ( F Q G ) )
39 simpr 
 |-  ( ( f = F /\ g = G ) -> g = G )
40 38 39 oveq12d 
 |-  ( ( f = F /\ g = G ) -> ( ( f Q g ) .x. g ) = ( ( F Q G ) .x. G ) )
41 37 40 oveq12d 
 |-  ( ( f = F /\ g = G ) -> ( f .- ( ( f Q g ) .x. g ) ) = ( F .- ( ( F Q G ) .x. G ) ) )
42 41 adantl 
 |-  ( ( ( F e. B /\ G e. B ) /\ ( f = F /\ g = G ) ) -> ( f .- ( ( f Q g ) .x. g ) ) = ( F .- ( ( F Q G ) .x. G ) ) )
43 simpl 
 |-  ( ( F e. B /\ G e. B ) -> F e. B )
44 simpr 
 |-  ( ( F e. B /\ G e. B ) -> G e. B )
45 ovexd 
 |-  ( ( F e. B /\ G e. B ) -> ( F .- ( ( F Q G ) .x. G ) ) e. _V )
46 36 42 43 44 45 ovmpod 
 |-  ( ( F e. B /\ G e. B ) -> ( F E G ) = ( F .- ( ( F Q G ) .x. G ) ) )