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

Metamath Proof Explorer

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