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

Definition df-q1p 19518
Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 19523. We actually use the reversed version for better harmony with our divisibility df-dvdsr 15423. (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 19513 . 2  class quot1p
2 vr . . 3  set  r
3 cvv 2788 . . 3  class  _V
4 vp . . . 4  set  p
52cv 1622 . . . . 5  class  r
6 cpl1 16252 . . . . 5  class Poly1
75, 6cfv 5255 . . . 4  class  (Poly1 `  r
)
8 vb . . . . 5  set  b
94cv 1622 . . . . . 6  class  p
10 cbs 13148 . . . . . 6  class  Base
119, 10cfv 5255 . . . . 5  class  ( Base `  p )
12 vf . . . . . 6  set  f
13 vg . . . . . 6  set  g
148cv 1622 . . . . . 6  class  b
1512cv 1622 . . . . . . . . . 10  class  f
16 vq . . . . . . . . . . . 12  set  q
1716cv 1622 . . . . . . . . . . 11  class  q
1813cv 1622 . . . . . . . . . . 11  class  g
19 cmulr 13209 . . . . . . . . . . . 12  class  .r
209, 19cfv 5255 . . . . . . . . . . 11  class  ( .r
`  p )
2117, 18, 20co 5858 . . . . . . . . . 10  class  ( q ( .r `  p
) g )
22 csg 14365 . . . . . . . . . . 11  class  -g
239, 22cfv 5255 . . . . . . . . . 10  class  ( -g `  p )
2415, 21, 23co 5858 . . . . . . . . 9  class  ( f ( -g `  p
) ( q ( .r `  p ) g ) )
25 cdg1 19440 . . . . . . . . . 10  class deg1
265, 25cfv 5255 . . . . . . . . 9  class  ( deg1  `  r
)
2724, 26cfv 5255 . . . . . . . 8  class  ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )
2818, 26cfv 5255 . . . . . . . 8  class  ( ( deg1  `  r ) `  g
)
29 clt 8867 . . . . . . . 8  class  <
3027, 28, 29wbr 4023 . . . . . . 7  wff  ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )  <  ( ( deg1  `  r
) `  g )
3130, 16, 14crio 6297 . . . . . 6  class  ( iota_ q  e.  b ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )  <  ( ( deg1  `  r
) `  g )
)
3212, 13, 14, 14, 31cmpt2 5860 . . . . 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 3081 . . . 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 3081 . . 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 4077 . 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 1623 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  19539
  Copyright terms: Public domain W3C validator