Metamath Proof Explorer

Definition df-r1p

Description: Define the remainder after dividing two univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Assertion df-r1p 
|- rem1p = ( r e. _V |-> [_ ( Base ` ( Poly1 ` r ) ) / b ]_ ( f e. b , g e. b |-> ( f ( -g ` ( Poly1 ` r ) ) ( ( f ( quot1p ` r ) g ) ( .r ` ( Poly1 ` r ) ) g ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cr1p 
 |-  rem1p
1 vr 
 |-  r
2 cvv 
 |-  _V
3 cbs 
 |-  Base
4 cpl1 
 |-  Poly1
5 1 cv 
 |-  r
6 5 4 cfv 
 |-  ( Poly1 ` r )
7 6 3 cfv 
 |-  ( Base ` ( Poly1 ` r ) )
8 vb 
 |-  b
9 vf 
 |-  f
10 8 cv 
 |-  b
11 vg 
 |-  g
12 9 cv 
 |-  f
13 csg 
 |-  -g
14 6 13 cfv 
 |-  ( -g ` ( Poly1 ` r ) )
15 cq1p 
 |-  quot1p
16 5 15 cfv 
 |-  ( quot1p ` r )
17 11 cv 
 |-  g
18 12 17 16 co 
 |-  ( f ( quot1p ` r ) g )
19 cmulr 
 |-  .r
20 6 19 cfv 
 |-  ( .r ` ( Poly1 ` r ) )
21 18 17 20 co 
 |-  ( ( f ( quot1p ` r ) g ) ( .r ` ( Poly1 ` r ) ) g )
22 12 21 14 co 
 |-  ( f ( -g ` ( Poly1 ` r ) ) ( ( f ( quot1p ` r ) g ) ( .r ` ( Poly1 ` r ) ) g ) )
23 9 11 10 10 22 cmpo 
 |-  ( f e. b , g e. b |-> ( f ( -g ` ( Poly1 ` r ) ) ( ( f ( quot1p ` r ) g ) ( .r ` ( Poly1 ` r ) ) g ) ) )
24 8 7 23 csb 
 |-  [_ ( Base ` ( Poly1 ` r ) ) / b ]_ ( f e. b , g e. b |-> ( f ( -g ` ( Poly1 ` r ) ) ( ( f ( quot1p ` r ) g ) ( .r ` ( Poly1 ` r ) ) g ) ) )
25 1 2 24 cmpt 
 |-  ( r e. _V |-> [_ ( Base ` ( Poly1 ` r ) ) / b ]_ ( f e. b , g e. b |-> ( f ( -g ` ( Poly1 ` r ) ) ( ( f ( quot1p ` r ) g ) ( .r ` ( Poly1 ` r ) ) g ) ) ) )
26 0 25 wceq 
 |-  rem1p = ( r e. _V |-> [_ ( Base ` ( Poly1 ` r ) ) / b ]_ ( f e. b , g e. b |-> ( f ( -g ` ( Poly1 ` r ) ) ( ( f ( quot1p ` r ) g ) ( .r ` ( Poly1 ` r ) ) g ) ) ) )