Metamath Proof Explorer

Definition df-quot

Description: Define the quotient function on polynomials. This is the q of the expression f = g x. q + r in the division algorithm. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Assertion df-quot ⊢ quot = f ∈ Poly ⁡ ℂ , g ∈ Poly ⁡ ℂ ∖ 0 𝑝 ⟼ ι q ∈ Poly ⁡ ℂ | [˙f − f g × f q / r]˙ r = 0 𝑝 ∨ deg ⁡ r < deg ⁡ g

Detailed syntax breakdown

Step Hyp Ref Expression
0 cquot class quot
1 vf setvar f
2 cply class Poly
3 cc class ℂ
4 3 2 cfv class Poly ⁡ ℂ
5 vg setvar g
6 c0p class 0 𝑝
7 6 csn class 0 𝑝
8 4 7 cdif class Poly ⁡ ℂ ∖ 0 𝑝
9 vq setvar q
10 1 cv setvar f
11 cmin class −
12 11 cof class ∘ f ⁡ −
13 5 cv setvar g
14 cmul class ×
15 14 cof class ∘ f ⁡ ×
16 9 cv setvar q
17 13 16 15 co class g × f q
18 10 17 12 co class f − f g × f q
19 vr setvar r
20 19 cv setvar r
21 20 6 wceq wff r = 0 𝑝
22 cdgr class deg
23 20 22 cfv class deg ⁡ r
24 clt class <
25 13 22 cfv class deg ⁡ g
26 23 25 24 wbr wff deg ⁡ r < deg ⁡ g
27 21 26 wo wff r = 0 𝑝 ∨ deg ⁡ r < deg ⁡ g
28 27 19 18 wsbc wff [˙f − f g × f q / r]˙ r = 0 𝑝 ∨ deg ⁡ r < deg ⁡ g
29 28 9 4 crio class ι q ∈ Poly ⁡ ℂ | [˙f − f g × f q / r]˙ r = 0 𝑝 ∨ deg ⁡ r < deg ⁡ g
30 1 5 4 8 29 cmpo class f ∈ Poly ⁡ ℂ , g ∈ Poly ⁡ ℂ ∖ 0 𝑝 ⟼ ι q ∈ Poly ⁡ ℂ | [˙f − f g × f q / r]˙ r = 0 𝑝 ∨ deg ⁡ r < deg ⁡ g
31 0 30 wceq wff quot = f ∈ Poly ⁡ ℂ , g ∈ Poly ⁡ ℂ ∖ 0 𝑝 ⟼ ι q ∈ Poly ⁡ ℂ | [˙f − f g × f q / r]˙ r = 0 𝑝 ∨ deg ⁡ r < deg ⁡ g