MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-q1p Unicode version

Definition df-q1p 19534
Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 19539. We actually use the reversed version for better harmony with our divisibility df-dvdsr 15439. (Contributed by Stefan O'Rear, 28-Mar-2015.)
Assertion
Ref Expression
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
) ) ) )
Distinct variable group:    f, r, g, b, p, q

Detailed syntax breakdown of Definition df-q1p
StepHypRef Expression
1 cq1p 19529 . 2  class quot1p
2 vr . . 3  set  r
3 cvv 2801 . . 3  class  _V
4 vp . . . 4  set  p
52cv 1631 . . . . 5  class  r
6 cpl1 16268 . . . . 5  class Poly1
75, 6cfv 5271 . . . 4  class  (Poly1 `  r
)
8 vb . . . . 5  set  b
94cv 1631 . . . . . 6  class  p
10 cbs 13164 . . . . . 6  class  Base
119, 10cfv 5271 . . . . 5  class  ( Base `  p )
12 vf . . . . . 6  set  f
13 vg . . . . . 6  set  g
148cv 1631 . . . . . 6  class  b
1512cv 1631 . . . . . . . . . 10  class  f
16 vq . . . . . . . . . . . 12  set  q
1716cv 1631 . . . . . . . . . . 11  class  q
1813cv 1631 . . . . . . . . . . 11  class  g
19 cmulr 13225 . . . . . . . . . . . 12  class  .r
209, 19cfv 5271 . . . . . . . . . . 11  class  ( .r
`  p )
2117, 18, 20co 5874 . . . . . . . . . 10  class  ( q ( .r `  p
) g )
22 csg 14381 . . . . . . . . . . 11  class  -g
239, 22cfv 5271 . . . . . . . . . 10  class  ( -g `  p )
2415, 21, 23co 5874 . . . . . . . . 9  class  ( f ( -g `  p
) ( q ( .r `  p ) g ) )
25 cdg1 19456 . . . . . . . . . 10  class deg1
265, 25cfv 5271 . . . . . . . . 9  class  ( deg1  `  r
)
2724, 26cfv 5271 . . . . . . . 8  class  ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )
2818, 26cfv 5271 . . . . . . . 8  class  ( ( deg1  `  r ) `  g
)
29 clt 8883 . . . . . . . 8  class  <
3027, 28, 29wbr 4039 . . . . . . 7  wff  ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )  <  ( ( deg1  `  r
) `  g )
3130, 16, 14crio 6313 . . . . . 6  class  ( iota_ q  e.  b ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )  <  ( ( deg1  `  r
) `  g )
)
3212, 13, 14, 14, 31cmpt2 5876 . . . . 5  class  ( f  e.  b ,  g  e.  b  |->  ( iota_ q  e.  b ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )  <  ( ( deg1  `  r
) `  g )
) )
338, 11, 32csb 3094 . . . 4  class  [_ ( 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 ) ) )
344, 7, 33csb 3094 . . 3  class  [_ (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
) ) )
352, 3, 34cmpt 4093 . 2  class  ( 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
) ) ) )
361, 35wceq 1632 1  wff 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
) ) ) )
Colors of variables: wff set class
This definition is referenced by:  q1pval  19555
  Copyright terms: Public domain W3C validator