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

Definition df-q1p 22618
Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 22623. We actually use the reversed version for better harmony with our divisibility df-dvdsr 17403. (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 22613 . 2  class quot1p
2 vr . . 3  setvar  r
3 cvv 3034 . . 3  class  _V
4 vp . . . 4  setvar  p
52cv 1398 . . . . 5  class  r
6 cpl1 18329 . . . . 5  class Poly1
75, 6cfv 5496 . . . 4  class  (Poly1 `  r
)
8 vb . . . . 5  setvar  b
94cv 1398 . . . . . 6  class  p
10 cbs 14634 . . . . . 6  class  Base
119, 10cfv 5496 . . . . 5  class  ( Base `  p )
12 vf . . . . . 6  setvar  f
13 vg . . . . . 6  setvar  g
148cv 1398 . . . . . 6  class  b
1512cv 1398 . . . . . . . . . 10  class  f
16 vq . . . . . . . . . . . 12  setvar  q
1716cv 1398 . . . . . . . . . . 11  class  q
1813cv 1398 . . . . . . . . . . 11  class  g
19 cmulr 14703 . . . . . . . . . . . 12  class  .r
209, 19cfv 5496 . . . . . . . . . . 11  class  ( .r
`  p )
2117, 18, 20co 6196 . . . . . . . . . 10  class  ( q ( .r `  p
) g )
22 csg 16172 . . . . . . . . . . 11  class  -g
239, 22cfv 5496 . . . . . . . . . 10  class  ( -g `  p )
2415, 21, 23co 6196 . . . . . . . . 9  class  ( f ( -g `  p
) ( q ( .r `  p ) g ) )
25 cdg1 22537 . . . . . . . . . 10  class deg1
265, 25cfv 5496 . . . . . . . . 9  class  ( deg1  `  r
)
2724, 26cfv 5496 . . . . . . . 8  class  ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )
2818, 26cfv 5496 . . . . . . . 8  class  ( ( deg1  `  r ) `  g
)
29 clt 9539 . . . . . . . 8  class  <
3027, 28, 29wbr 4367 . . . . . . 7  wff  ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )  <  ( ( deg1  `  r
) `  g )
3130, 16, 14crio 6157 . . . . . 6  class  ( iota_ q  e.  b  ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )  <  ( ( deg1  `  r
) `  g )
)
3212, 13, 14, 14, 31cmpt2 6198 . . . . 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 3348 . . . 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 3348 . . 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 4425 . 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 1399 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  22639
  Copyright terms: Public domain W3C validator