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 = ( 𝑓 ∈ ( Poly ‘ ℂ ) , 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ↦ ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) [ ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cquot	⊢ quot
1		vf	⊢ 𝑓
2		cply	⊢ Poly
3		cc	⊢ ℂ
4	3 2	cfv	⊢ ( Poly ‘ ℂ )
5		vg	⊢ 𝑔
6		c0p	⊢ 0𝑝
7	6	csn	⊢ { 0𝑝 }
8	4 7	cdif	⊢ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } )
9		vq	⊢ 𝑞
10	1	cv	⊢ 𝑓
11		cmin	⊢ −
12	11	cof	⊢ ∘f −
13	5	cv	⊢ 𝑔
14		cmul	⊢ ·
15	14	cof	⊢ ∘f ·
16	9	cv	⊢ 𝑞
17	13 16 15	co	⊢ ( 𝑔 ∘f · 𝑞 )
18	10 17 12	co	⊢ ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) )
19		vr	⊢ 𝑟
20	19	cv	⊢ 𝑟
21	20 6	wceq	⊢ 𝑟 = 0𝑝
22		cdgr	⊢ deg
23	20 22	cfv	⊢ ( deg ‘ 𝑟 )
24		clt	⊢ <
25	13 22	cfv	⊢ ( deg ‘ 𝑔 )
26	23 25 24	wbr	⊢ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 )
27	21 26	wo	⊢ ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) )
28	27 19 18	wsbc	⊢ [ ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) )
29	28 9 4	crio	⊢ ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) [ ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) )
30	1 5 4 8 29	cmpo	⊢ ( 𝑓 ∈ ( Poly ‘ ℂ ) , 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ↦ ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) [ ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ) )
31	0 30	wceq	⊢ quot = ( 𝑓 ∈ ( Poly ‘ ℂ ) , 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ↦ ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) [ ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ) )