Detailed syntax breakdown of Definition df-q1p
| Step | Hyp | Ref
| Expression |
| 1 | | cq1p 26167 |
. 2
class
quot1p |
| 2 | | vr |
. . 3
setvar 𝑟 |
| 3 | | cvv 3480 |
. . 3
class
V |
| 4 | | vp |
. . . 4
setvar 𝑝 |
| 5 | 2 | cv 1539 |
. . . . 5
class 𝑟 |
| 6 | | cpl1 22178 |
. . . . 5
class
Poly1 |
| 7 | 5, 6 | cfv 6561 |
. . . 4
class
(Poly1‘𝑟) |
| 8 | | vb |
. . . . 5
setvar 𝑏 |
| 9 | 4 | cv 1539 |
. . . . . 6
class 𝑝 |
| 10 | | cbs 17247 |
. . . . . 6
class
Base |
| 11 | 9, 10 | cfv 6561 |
. . . . 5
class
(Base‘𝑝) |
| 12 | | vf |
. . . . . 6
setvar 𝑓 |
| 13 | | vg |
. . . . . 6
setvar 𝑔 |
| 14 | 8 | cv 1539 |
. . . . . 6
class 𝑏 |
| 15 | 12 | cv 1539 |
. . . . . . . . . 10
class 𝑓 |
| 16 | | vq |
. . . . . . . . . . . 12
setvar 𝑞 |
| 17 | 16 | cv 1539 |
. . . . . . . . . . 11
class 𝑞 |
| 18 | 13 | cv 1539 |
. . . . . . . . . . 11
class 𝑔 |
| 19 | | cmulr 17298 |
. . . . . . . . . . . 12
class
.r |
| 20 | 9, 19 | cfv 6561 |
. . . . . . . . . . 11
class
(.r‘𝑝) |
| 21 | 17, 18, 20 | co 7431 |
. . . . . . . . . 10
class (𝑞(.r‘𝑝)𝑔) |
| 22 | | csg 18953 |
. . . . . . . . . . 11
class
-g |
| 23 | 9, 22 | cfv 6561 |
. . . . . . . . . 10
class
(-g‘𝑝) |
| 24 | 15, 21, 23 | co 7431 |
. . . . . . . . 9
class (𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔)) |
| 25 | | cdg1 26093 |
. . . . . . . . . 10
class
deg1 |
| 26 | 5, 25 | cfv 6561 |
. . . . . . . . 9
class
(deg1‘𝑟) |
| 27 | 24, 26 | cfv 6561 |
. . . . . . . 8
class
((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) |
| 28 | 18, 26 | cfv 6561 |
. . . . . . . 8
class
((deg1‘𝑟)‘𝑔) |
| 29 | | clt 11295 |
. . . . . . . 8
class
< |
| 30 | 27, 28, 29 | wbr 5143 |
. . . . . . 7
wff
((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔) |
| 31 | 30, 16, 14 | crio 7387 |
. . . . . 6
class
(℩𝑞
∈ 𝑏
((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)) |
| 32 | 12, 13, 14, 14, 31 | cmpo 7433 |
. . . . 5
class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔))) |
| 33 | 8, 11, 32 | csb 3899 |
. . . 4
class
⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔))) |
| 34 | 4, 7, 33 | csb 3899 |
. . 3
class
⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔))) |
| 35 | 2, 3, 34 | cmpt 5225 |
. 2
class (𝑟 ∈ V ↦
⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)))) |
| 36 | 1, 35 | wceq 1540 |
1
wff
quot1p = (𝑟 ∈ V ↦
⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔)))) |