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 = quot 1p R
q1pval.p P = Poly 1 R
q1pval.b B = Base P
q1pval.d D = deg 1 R
q1pval.m - ˙ = - P
q1pval.t · ˙ = P
Assertion q1pval F B G B F Q G = ι q B | D F - ˙ q · ˙ G < D G

Proof

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