This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑟 ∈ V ↦ ⦋ ( Base ‘ ( Poly1 ‘ 𝑟 ) ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ( -g ‘ ( Poly1 ‘ 𝑟 ) ) ( ( 𝑓 ( quot1p ‘ 𝑟 ) 𝑔 ) ( .r ‘ ( Poly1 ‘ 𝑟 ) ) 𝑔 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cr1p ⊢ rem1p
1 vr ⊢ 𝑟
2 cvv ⊢ V
3 cbs ⊢ Base
4 cpl1 ⊢ Poly1
5 1 cv ⊢ 𝑟
6 5 4 cfv ⊢ ( Poly1 ‘ 𝑟 )
7 6 3 cfv ⊢ ( Base ‘ ( Poly1 ‘ 𝑟 ) )
8 vb ⊢ 𝑏
9 vf ⊢ 𝑓
10 8 cv ⊢ 𝑏
11 vg ⊢ 𝑔
12 9 cv ⊢ 𝑓
13 csg ⊢ -g
14 6 13 cfv ⊢ ( -g ‘ ( Poly1 ‘ 𝑟 ) )
15 cq1p ⊢ quot1p
16 5 15 cfv ⊢ ( quot1p ‘ 𝑟 )
17 11 cv ⊢ 𝑔
18 12 17 16 co ⊢ ( 𝑓 ( quot1p ‘ 𝑟 ) 𝑔 )
19 cmulr ⊢ .r
20 6 19 cfv ⊢ ( .r ‘ ( Poly1 ‘ 𝑟 ) )
21 18 17 20 co ⊢ ( ( 𝑓 ( quot1p ‘ 𝑟 ) 𝑔 ) ( .r ‘ ( Poly1 ‘ 𝑟 ) ) 𝑔 )
22 12 21 14 co ⊢ ( 𝑓 ( -g ‘ ( Poly1 ‘ 𝑟 ) ) ( ( 𝑓 ( quot1p ‘ 𝑟 ) 𝑔 ) ( .r ‘ ( Poly1 ‘ 𝑟 ) ) 𝑔 ) )
23 9 11 10 10 22 cmpo ⊢ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ( -g ‘ ( Poly1 ‘ 𝑟 ) ) ( ( 𝑓 ( quot1p ‘ 𝑟 ) 𝑔 ) ( .r ‘ ( Poly1 ‘ 𝑟 ) ) 𝑔 ) ) )
24 8 7 23 csb ⊢ ⦋ ( Base ‘ ( Poly1 ‘ 𝑟 ) ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ( -g ‘ ( Poly1 ‘ 𝑟 ) ) ( ( 𝑓 ( quot1p ‘ 𝑟 ) 𝑔 ) ( .r ‘ ( Poly1 ‘ 𝑟 ) ) 𝑔 ) ) )
25 1 2 24 cmpt ⊢ ( 𝑟 ∈ V ↦ ⦋ ( Base ‘ ( Poly1 ‘ 𝑟 ) ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ( -g ‘ ( Poly1 ‘ 𝑟 ) ) ( ( 𝑓 ( quot1p ‘ 𝑟 ) 𝑔 ) ( .r ‘ ( Poly1 ‘ 𝑟 ) ) 𝑔 ) ) ) )
26 0 25 wceq ⊢ rem1p = ( 𝑟 ∈ V ↦ ⦋ ( Base ‘ ( Poly1 ‘ 𝑟 ) ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ( -g ‘ ( Poly1 ‘ 𝑟 ) ) ( ( 𝑓 ( quot1p ‘ 𝑟 ) 𝑔 ) ( .r ‘ ( Poly1 ‘ 𝑟 ) ) 𝑔 ) ) ) )