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

Definition df-q1p 20055
Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 20060. We actually use the reversed version for better harmony with our divisibility df-dvdsr 15746. (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 20050 . 2  class quot1p
2 vr . . 3  set  r
3 cvv 2956 . . 3  class  _V
4 vp . . . 4  set  p
52cv 1651 . . . . 5  class  r
6 cpl1 16571 . . . . 5  class Poly1
75, 6cfv 5454 . . . 4  class  (Poly1 `  r
)
8 vb . . . . 5  set  b
94cv 1651 . . . . . 6  class  p
10 cbs 13469 . . . . . 6  class  Base
119, 10cfv 5454 . . . . 5  class  ( Base `  p )
12 vf . . . . . 6  set  f
13 vg . . . . . 6  set  g
148cv 1651 . . . . . 6  class  b
1512cv 1651 . . . . . . . . . 10  class  f
16 vq . . . . . . . . . . . 12  set  q
1716cv 1651 . . . . . . . . . . 11  class  q
1813cv 1651 . . . . . . . . . . 11  class  g
19 cmulr 13530 . . . . . . . . . . . 12  class  .r
209, 19cfv 5454 . . . . . . . . . . 11  class  ( .r
`  p )
2117, 18, 20co 6081 . . . . . . . . . 10  class  ( q ( .r `  p
) g )
22 csg 14688 . . . . . . . . . . 11  class  -g
239, 22cfv 5454 . . . . . . . . . 10  class  ( -g `  p )
2415, 21, 23co 6081 . . . . . . . . 9  class  ( f ( -g `  p
) ( q ( .r `  p ) g ) )
25 cdg1 19977 . . . . . . . . . 10  class deg1
265, 25cfv 5454 . . . . . . . . 9  class  ( deg1  `  r
)
2724, 26cfv 5454 . . . . . . . 8  class  ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )
2818, 26cfv 5454 . . . . . . . 8  class  ( ( deg1  `  r ) `  g
)
29 clt 9120 . . . . . . . 8  class  <
3027, 28, 29wbr 4212 . . . . . . 7  wff  ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )  <  ( ( deg1  `  r
) `  g )
3130, 16, 14crio 6542 . . . . . 6  class  ( iota_ q  e.  b ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )  <  ( ( deg1  `  r
) `  g )
)
3212, 13, 14, 14, 31cmpt2 6083 . . . . 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 3251 . . . 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 3251 . . 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 4266 . 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 1652 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  20076
  Copyright terms: Public domain W3C validator