Metamath Proof Explorer

Theorem q1pval

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

Ref Expression
Hypotheses q1pval.q 
|- Q = ( quot1p ` R )
q1pval.p 
|- P = ( Poly1 ` R )
q1pval.b 
|- B = ( Base ` P )
q1pval.d 
|- D = ( deg1 ` R )
q1pval.m 
|- .- = ( -g ` P )
q1pval.t 
|- .x. = ( .r ` P )
Assertion q1pval 
|- ( ( F e. B /\ G e. B ) -> ( F Q G ) = ( iota_ q e. B ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) )

Proof

Step Hyp Ref Expression
1 q1pval.q 
 |-  Q = ( quot1p ` R )
2 q1pval.p 
 |-  P = ( Poly1 ` R )
3 q1pval.b 
 |-  B = ( Base ` P )
4 q1pval.d 
 |-  D = ( deg1 ` R )
5 q1pval.m 
 |-  .- = ( -g ` P )
6 q1pval.t 
 |-  .x. = ( .r ` P )
7 2 3 elbasfv 
 |-  ( G e. B -> R e. _V )
8 fveq2 
 |-  ( r = R -> ( Poly1 ` r ) = ( Poly1 ` R ) )
9 8 2 eqtr4di 
 |-  ( r = R -> ( Poly1 ` r ) = P )
10 9 csbeq1d 
 |-  ( r = R -> [_ ( Poly1 ` r ) / p ]_ [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) = [_ P / p ]_ [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) )
11 2 fvexi 
 |-  P e. _V
12 11 a1i 
 |-  ( r = R -> P e. _V )
13 fveq2 
 |-  ( p = P -> ( Base ` p ) = ( Base ` P ) )
14 13 adantl 
 |-  ( ( r = R /\ p = P ) -> ( Base ` p ) = ( Base ` P ) )
15 14 3 eqtr4di 
 |-  ( ( r = R /\ p = P ) -> ( Base ` p ) = B )
16 15 csbeq1d 
 |-  ( ( r = R /\ p = P ) -> [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) = [_ B / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) )
17 3 fvexi 
 |-  B e. _V
18 17 a1i 
 |-  ( ( r = R /\ p = P ) -> B e. _V )
19 simpr 
 |-  ( ( ( r = R /\ p = P ) /\ b = B ) -> b = B )
20 fveq2 
 |-  ( r = R -> ( deg1 ` r ) = ( deg1 ` R ) )
21 20 ad2antrr 
 |-  ( ( ( r = R /\ p = P ) /\ b = B ) -> ( deg1 ` r ) = ( deg1 ` R ) )
22 21 4 eqtr4di 
 |-  ( ( ( r = R /\ p = P ) /\ b = B ) -> ( deg1 ` r ) = D )
23 fveq2 
 |-  ( p = P -> ( -g ` p ) = ( -g ` P ) )
24 23 ad2antlr 
 |-  ( ( ( r = R /\ p = P ) /\ b = B ) -> ( -g ` p ) = ( -g ` P ) )
25 24 5 eqtr4di 
 |-  ( ( ( r = R /\ p = P ) /\ b = B ) -> ( -g ` p ) = .- )
26 eqidd 
 |-  ( ( ( r = R /\ p = P ) /\ b = B ) -> f = f )
27 fveq2 
 |-  ( p = P -> ( .r ` p ) = ( .r ` P ) )
28 27 ad2antlr 
 |-  ( ( ( r = R /\ p = P ) /\ b = B ) -> ( .r ` p ) = ( .r ` P ) )
29 28 6 eqtr4di 
 |-  ( ( ( r = R /\ p = P ) /\ b = B ) -> ( .r ` p ) = .x. )
30 29 oveqd 
 |-  ( ( ( r = R /\ p = P ) /\ b = B ) -> ( q ( .r ` p ) g ) = ( q .x. g ) )
31 25 26 30 oveq123d 
 |-  ( ( ( r = R /\ p = P ) /\ b = B ) -> ( f ( -g ` p ) ( q ( .r ` p ) g ) ) = ( f .- ( q .x. g ) ) )
32 22 31 fveq12d 
 |-  ( ( ( r = R /\ p = P ) /\ b = B ) -> ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) = ( D ` ( f .- ( q .x. g ) ) ) )
33 22 fveq1d 
 |-  ( ( ( r = R /\ p = P ) /\ b = B ) -> ( ( deg1 ` r ) ` g ) = ( D ` g ) )
34 32 33 breq12d 
 |-  ( ( ( r = R /\ p = P ) /\ b = B ) -> ( ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) <-> ( D ` ( f .- ( q .x. g ) ) ) < ( D ` g ) ) )
35 19 34 riotaeqbidv 
 |-  ( ( ( r = R /\ p = P ) /\ b = B ) -> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) = ( iota_ q e. B ( D ` ( f .- ( q .x. g ) ) ) < ( D ` g ) ) )
36 19 19 35 mpoeq123dv 
 |-  ( ( ( r = R /\ p = P ) /\ b = B ) -> ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) = ( f e. B , g e. B |-> ( iota_ q e. B ( D ` ( f .- ( q .x. g ) ) ) < ( D ` g ) ) ) )
37 18 36 csbied 
 |-  ( ( r = R /\ p = P ) -> [_ B / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) = ( f e. B , g e. B |-> ( iota_ q e. B ( D ` ( f .- ( q .x. g ) ) ) < ( D ` g ) ) ) )
38 16 37 eqtrd 
 |-  ( ( r = R /\ p = P ) -> [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) = ( f e. B , g e. B |-> ( iota_ q e. B ( D ` ( f .- ( q .x. g ) ) ) < ( D ` g ) ) ) )
39 12 38 csbied 
 |-  ( r = R -> [_ P / p ]_ [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) = ( f e. B , g e. B |-> ( iota_ q e. B ( D ` ( f .- ( q .x. g ) ) ) < ( D ` g ) ) ) )
40 10 39 eqtrd 
 |-  ( r = R -> [_ ( Poly1 ` r ) / p ]_ [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) = ( f e. B , g e. B |-> ( iota_ q e. B ( D ` ( f .- ( q .x. g ) ) ) < ( D ` g ) ) ) )
41 df-q1p 
 |-  quot1p = ( r e. _V |-> [_ ( Poly1 ` r ) / p ]_ [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) )
42 17 17 mpoex 
 |-  ( f e. B , g e. B |-> ( iota_ q e. B ( D ` ( f .- ( q .x. g ) ) ) < ( D ` g ) ) ) e. _V
43 40 41 42 fvmpt 
 |-  ( R e. _V -> ( quot1p ` R ) = ( f e. B , g e. B |-> ( iota_ q e. B ( D ` ( f .- ( q .x. g ) ) ) < ( D ` g ) ) ) )
44 1 43 syl5eq 
 |-  ( R e. _V -> Q = ( f e. B , g e. B |-> ( iota_ q e. B ( D ` ( f .- ( q .x. g ) ) ) < ( D ` g ) ) ) )
45 7 44 syl 
 |-  ( G e. B -> Q = ( f e. B , g e. B |-> ( iota_ q e. B ( D ` ( f .- ( q .x. g ) ) ) < ( D ` g ) ) ) )
46 45 adantl 
 |-  ( ( F e. B /\ G e. B ) -> Q = ( f e. B , g e. B |-> ( iota_ q e. B ( D ` ( f .- ( q .x. g ) ) ) < ( D ` g ) ) ) )
47 id 
 |-  ( f = F -> f = F )
48 oveq2 
 |-  ( g = G -> ( q .x. g ) = ( q .x. G ) )
49 47 48 oveqan12d 
 |-  ( ( f = F /\ g = G ) -> ( f .- ( q .x. g ) ) = ( F .- ( q .x. G ) ) )
50 49 fveq2d 
 |-  ( ( f = F /\ g = G ) -> ( D ` ( f .- ( q .x. g ) ) ) = ( D ` ( F .- ( q .x. G ) ) ) )
51 fveq2 
 |-  ( g = G -> ( D ` g ) = ( D ` G ) )
52 51 adantl 
 |-  ( ( f = F /\ g = G ) -> ( D ` g ) = ( D ` G ) )
53 50 52 breq12d 
 |-  ( ( f = F /\ g = G ) -> ( ( D ` ( f .- ( q .x. g ) ) ) < ( D ` g ) <-> ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) )
54 53 riotabidv 
 |-  ( ( f = F /\ g = G ) -> ( iota_ q e. B ( D ` ( f .- ( q .x. g ) ) ) < ( D ` g ) ) = ( iota_ q e. B ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) )
55 54 adantl 
 |-  ( ( ( F e. B /\ G e. B ) /\ ( f = F /\ g = G ) ) -> ( iota_ q e. B ( D ` ( f .- ( q .x. g ) ) ) < ( D ` g ) ) = ( iota_ q e. B ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) )
56 simpl 
 |-  ( ( F e. B /\ G e. B ) -> F e. B )
57 simpr 
 |-  ( ( F e. B /\ G e. B ) -> G e. B )
58 riotaex 
 |-  ( iota_ q e. B ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) e. _V
59 58 a1i 
 |-  ( ( F e. B /\ G e. B ) -> ( iota_ q e. B ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) e. _V )
60 46 55 56 57 59 ovmpod 
 |-  ( ( F e. B /\ G e. B ) -> ( F Q G ) = ( iota_ q e. B ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) )