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

Definition df-q1p 21584
Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 21589. We actually use the reversed version for better harmony with our divisibility df-dvdsr 16723. (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 21579 . 2  class quot1p
2 vr . . 3  setvar  r
3 cvv 2967 . . 3  class  _V
4 vp . . . 4  setvar  p
52cv 1368 . . . . 5  class  r
6 cpl1 17613 . . . . 5  class Poly1
75, 6cfv 5413 . . . 4  class  (Poly1 `  r
)
8 vb . . . . 5  setvar  b
94cv 1368 . . . . . 6  class  p
10 cbs 14166 . . . . . 6  class  Base
119, 10cfv 5413 . . . . 5  class  ( Base `  p )
12 vf . . . . . 6  setvar  f
13 vg . . . . . 6  setvar  g
148cv 1368 . . . . . 6  class  b
1512cv 1368 . . . . . . . . . 10  class  f
16 vq . . . . . . . . . . . 12  setvar  q
1716cv 1368 . . . . . . . . . . 11  class  q
1813cv 1368 . . . . . . . . . . 11  class  g
19 cmulr 14231 . . . . . . . . . . . 12  class  .r
209, 19cfv 5413 . . . . . . . . . . 11  class  ( .r
`  p )
2117, 18, 20co 6086 . . . . . . . . . 10  class  ( q ( .r `  p
) g )
22 csg 15405 . . . . . . . . . . 11  class  -g
239, 22cfv 5413 . . . . . . . . . 10  class  ( -g `  p )
2415, 21, 23co 6086 . . . . . . . . 9  class  ( f ( -g `  p
) ( q ( .r `  p ) g ) )
25 cdg1 21503 . . . . . . . . . 10  class deg1
265, 25cfv 5413 . . . . . . . . 9  class  ( deg1  `  r
)
2724, 26cfv 5413 . . . . . . . 8  class  ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )
2818, 26cfv 5413 . . . . . . . 8  class  ( ( deg1  `  r ) `  g
)
29 clt 9410 . . . . . . . 8  class  <
3027, 28, 29wbr 4287 . . . . . . 7  wff  ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )  <  ( ( deg1  `  r
) `  g )
3130, 16, 14crio 6046 . . . . . 6  class  ( iota_ q  e.  b  ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )  <  ( ( deg1  `  r
) `  g )
)
3212, 13, 14, 14, 31cmpt2 6088 . . . . 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 3283 . . . 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 3283 . . 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 4345 . 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 1369 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 setvar class
This definition is referenced by:  q1pval  21605
  Copyright terms: Public domain W3C validator