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 
|- quot1p = ( r e. _V |-> [_ ( Poly1 ` r ) / p ]_ [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cq1p 
 |-  quot1p
1 vr 
 |-  r
2 cvv 
 |-  _V
3 cpl1 
 |-  Poly1
4 1 cv 
 |-  r
5 4 3 cfv 
 |-  ( Poly1 ` r )
6 vp 
 |-  p
7 cbs 
 |-  Base
8 6 cv 
 |-  p
9 8 7 cfv 
 |-  ( Base ` p )
10 vb 
 |-  b
11 vf 
 |-  f
12 10 cv 
 |-  b
13 vg 
 |-  g
14 vq 
 |-  q
15 cdg1 
 |-  deg1
16 4 15 cfv 
 |-  ( deg1 ` r )
17 11 cv 
 |-  f
18 csg 
 |-  -g
19 8 18 cfv 
 |-  ( -g ` p )
20 14 cv 
 |-  q
21 cmulr 
 |-  .r
22 8 21 cfv 
 |-  ( .r ` p )
23 13 cv 
 |-  g
24 20 23 22 co 
 |-  ( q ( .r ` p ) g )
25 17 24 19 co 
 |-  ( f ( -g ` p ) ( q ( .r ` p ) g ) )
26 25 16 cfv 
 |-  ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) )
27 clt 
 |-  <
28 23 16 cfv 
 |-  ( ( deg1 ` r ) ` g )
29 26 28 27 wbr 
 |-  ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g )
30 29 14 12 crio 
 |-  ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) )
31 11 13 12 12 30 cmpo 
 |-  ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) )
32 10 9 31 csb 
 |-  [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) )
33 6 5 32 csb 
 |-  [_ ( Poly1 ` r ) / p ]_ [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) )
34 1 2 33 cmpt 
 |-  ( r e. _V |-> [_ ( Poly1 ` r ) / p ]_ [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) )
35 0 34 wceq 
 |-  quot1p = ( r e. _V |-> [_ ( Poly1 ` r ) / p ]_ [_ ( Base ` p ) / b ]_ ( f e. b , g e. b |-> ( iota_ q e. b ( ( deg1 ` r ) ` ( f ( -g ` p ) ( q ( .r ` p ) g ) ) ) < ( ( deg1 ` r ) ` g ) ) ) )