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 ‘ 𝑟 ) ) 𝑔 ) ) ) )