Metamath Proof Explorer

Definition df-q1p

Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg . We actually use the reversed version for better harmony with our divisibility df-dvdsr . (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Assertion 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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cq1p class quot 1p
1 vr setvar r
2 cvv class V
3 cpl1 class Poly 1
4 1 cv setvar r
5 4 3 cfv class Poly 1 ⁡ r
6 vp setvar p
7 cbs class Base
8 6 cv setvar p
9 8 7 cfv class Base p
10 vb setvar b
11 vf setvar f
12 10 cv setvar b
13 vg setvar g
14 vq setvar q
15 cdg1 class deg 1
16 4 15 cfv class deg 1 ⁡ r
17 11 cv setvar f
18 csg class - 𝑔
19 8 18 cfv class - p
20 14 cv setvar q
21 cmulr class ⋅ 𝑟
22 8 21 cfv class ⋅ p
23 13 cv setvar g
24 20 23 22 co class q ⋅ p g
25 17 24 19 co class f - p q ⋅ p g
26 25 16 cfv class deg 1 ⁡ r ⁡ f - p q ⋅ p g
27 clt class <
28 23 16 cfv class deg 1 ⁡ r ⁡ g
29 26 28 27 wbr wff deg 1 ⁡ r ⁡ f - p q ⋅ p g < deg 1 ⁡ r ⁡ g
30 29 14 12 crio class ι q ∈ b | deg 1 ⁡ r ⁡ f - p q ⋅ p g < deg 1 ⁡ r ⁡ g
31 11 13 12 12 30 cmpo class f ∈ b , g ∈ b ⟼ ι q ∈ b | deg 1 ⁡ r ⁡ f - p q ⋅ p g < deg 1 ⁡ r ⁡ g
32 10 9 31 csb class ⦋ Base p / b⦌ f ∈ b , g ∈ b ⟼ ι q ∈ b | deg 1 ⁡ r ⁡ f - p q ⋅ p g < deg 1 ⁡ r ⁡ g
33 6 5 32 csb class ⦋ 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
34 1 2 33 cmpt class 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
35 0 34 wceq wff 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