# 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}_{\mathrm{1p}}\left({R}\right)$
q1pval.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
q1pval.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
q1pval.d ${⊢}{D}={\mathrm{deg}}_{1}\left({R}\right)$
q1pval.m
q1pval.t
Assertion q1pval

### Proof

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