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

Definition df-q1p 21720
Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 21725. We actually use the reversed version for better harmony with our divisibility df-dvdsr 16839. (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 21715 . 2  class quot1p
2 vr . . 3  setvar  r
3 cvv 3068 . . 3  class  _V
4 vp . . . 4  setvar  p
52cv 1369 . . . . 5  class  r
6 cpl1 17740 . . . . 5  class Poly1
75, 6cfv 5516 . . . 4  class  (Poly1 `  r
)
8 vb . . . . 5  setvar  b
94cv 1369 . . . . . 6  class  p
10 cbs 14276 . . . . . 6  class  Base
119, 10cfv 5516 . . . . 5  class  ( Base `  p )
12 vf . . . . . 6  setvar  f
13 vg . . . . . 6  setvar  g
148cv 1369 . . . . . 6  class  b
1512cv 1369 . . . . . . . . . 10  class  f
16 vq . . . . . . . . . . . 12  setvar  q
1716cv 1369 . . . . . . . . . . 11  class  q
1813cv 1369 . . . . . . . . . . 11  class  g
19 cmulr 14341 . . . . . . . . . . . 12  class  .r
209, 19cfv 5516 . . . . . . . . . . 11  class  ( .r
`  p )
2117, 18, 20co 6190 . . . . . . . . . 10  class  ( q ( .r `  p
) g )
22 csg 15515 . . . . . . . . . . 11  class  -g
239, 22cfv 5516 . . . . . . . . . 10  class  ( -g `  p )
2415, 21, 23co 6190 . . . . . . . . 9  class  ( f ( -g `  p
) ( q ( .r `  p ) g ) )
25 cdg1 21639 . . . . . . . . . 10  class deg1
265, 25cfv 5516 . . . . . . . . 9  class  ( deg1  `  r
)
2724, 26cfv 5516 . . . . . . . 8  class  ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )
2818, 26cfv 5516 . . . . . . . 8  class  ( ( deg1  `  r ) `  g
)
29 clt 9519 . . . . . . . 8  class  <
3027, 28, 29wbr 4390 . . . . . . 7  wff  ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )  <  ( ( deg1  `  r
) `  g )
3130, 16, 14crio 6150 . . . . . 6  class  ( iota_ q  e.  b  ( ( deg1  `  r ) `  (
f ( -g `  p
) ( q ( .r `  p ) g ) ) )  <  ( ( deg1  `  r
) `  g )
)
3212, 13, 14, 14, 31cmpt2 6192 . . . . 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 3386 . . . 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 3386 . . 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 4448 . 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 1370 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  21741
  Copyright terms: Public domain W3C validator