This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑓 ∈ ( 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 ‘ 𝑔 ) ) ) )