Definition df-q1p

Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg . We actually use the reversed version for better harmony with our divisibility df-dvdsr . (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Assertion	df-q1p	⊢ quot1p = ( 𝑟 ∈ V ↦ ⦋ ( Poly1 ‘ 𝑟 ) / 𝑝 ⦌ ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cq1p	⊢ quot1p
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		cpl1	⊢ Poly1
4	1	cv	⊢ 𝑟
5	4 3	cfv	⊢ ( Poly1 ‘ 𝑟 )
6		vp	⊢ 𝑝
7		cbs	⊢ Base
8	6	cv	⊢ 𝑝
9	8 7	cfv	⊢ ( Base ‘ 𝑝 )
10		vb	⊢ 𝑏
11		vf	⊢ 𝑓
12	10	cv	⊢ 𝑏
13		vg	⊢ 𝑔
14		vq	⊢ 𝑞
15		cdg1	⊢ deg1
16	4 15	cfv	⊢ ( deg1 ‘ 𝑟 )
17	11	cv	⊢ 𝑓
18		csg	⊢ -g
19	8 18	cfv	⊢ ( -g ‘ 𝑝 )
20	14	cv	⊢ 𝑞
21		cmulr	⊢ .r
22	8 21	cfv	⊢ ( .r ‘ 𝑝 )
23	13	cv	⊢ 𝑔
24	20 23 22	co	⊢ ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 )
25	17 24 19	co	⊢ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) )
26	25 16	cfv	⊢ ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) )
27		clt	⊢ <
28	23 16	cfv	⊢ ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 )
29	26 28 27	wbr	⊢ ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 )
30	29 14 12	crio	⊢ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) )
31	11 13 12 12 30	cmpo	⊢ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) )
32	10 9 31	csb	⊢ ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) )
33	6 5 32	csb	⊢ ⦋ ( Poly1 ‘ 𝑟 ) / 𝑝 ⦌ ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) )
34	1 2 33	cmpt	⊢ ( 𝑟 ∈ V ↦ ⦋ ( Poly1 ‘ 𝑟 ) / 𝑝 ⦌ ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) )
35	0 34	wceq	⊢ quot1p = ( 𝑟 ∈ V ↦ ⦋ ( Poly1 ‘ 𝑟 ) / 𝑝 ⦌ ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) )