Step |
Hyp |
Ref |
Expression |
0 |
|
cq1p |
|- quot1p |
1 |
|
vr |
|- r |
2 |
|
cvv |
|- _V |
3 |
|
cpl1 |
|- Poly1 |
4 |
1
|
cv |
|- r |
5 |
4 3
|
cfv |
|- ( Poly1 ` r ) |
6 |
|
vp |
|- p |
7 |
|
cbs |
|- Base |
8 |
6
|
cv |
|- p |
9 |
8 7
|
cfv |
|- ( Base ` p ) |
10 |
|
vb |
|- b |
11 |
|
vf |
|- f |
12 |
10
|
cv |
|- b |
13 |
|
vg |
|- g |
14 |
|
vq |
|- q |
15 |
|
cdg1 |
|- deg1 |
16 |
4 15
|
cfv |
|- ( deg1 ` r ) |
17 |
11
|
cv |
|- f |
18 |
|
csg |
|- -g |
19 |
8 18
|
cfv |
|- ( -g ` p ) |
20 |
14
|
cv |
|- q |
21 |
|
cmulr |
|- .r |
22 |
8 21
|
cfv |
|- ( .r ` p ) |
23 |
13
|
cv |
|- g |
24 |
20 23 22
|
co |
|- ( q ( .r ` p ) g ) |
25 |
17 24 19
|
co |
|- ( f ( -g ` p ) ( q ( .r ` p ) g ) ) |
26 |
25 16
|
cfv |
|- ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) |
27 |
|
clt |
|- < |
28 |
23 16
|
cfv |
|- ( ( deg1 ` r ) ` g ) |
29 |
26 28 27
|
wbr |
|- ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) |
30 |
29 14 12
|
crio |
|- ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) |
31 |
11 13 12 12 30
|
cmpo |
|- ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) |
32 |
10 9 31
|
csb |
|- [_ ( 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 ) ) ) |
33 |
6 5 32
|
csb |
|- [_ ( 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 ) ) ) |
34 |
1 2 33
|
cmpt |
|- ( 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 ) ) ) ) |
35 |
0 34
|
wceq |
|- 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 ) ) ) ) |