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 ) ) ) )