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

Metamath Proof Explorer

Theorem q1pval

Description: Value of the univariate polynomial quotient function. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses q1pval.q ⊢ 𝑄 = ( quot1p ‘ 𝑅 )
q1pval.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
q1pval.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
q1pval.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
q1pval.m ⊢ − = ( -g ‘ 𝑃 )
q1pval.t ⊢ · = ( .r ‘ 𝑃 )
Assertion q1pval ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 𝑄 𝐺 ) = ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 q1pval.q ⊢ 𝑄 = ( quot1p ‘ 𝑅 )
2 q1pval.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 q1pval.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
4 q1pval.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
5 q1pval.m ⊢ − = ( -g ‘ 𝑃 )
6 q1pval.t ⊢ · = ( .r ‘ 𝑃 )
7 2 3 elbasfv ⊢ ( 𝐺 ∈ 𝐵 → 𝑅 ∈ V )
8 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Poly1 ‘ 𝑟 ) = ( Poly1 ‘ 𝑅 ) )
9 8 2 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( Poly1 ‘ 𝑟 ) = 𝑃 )
10 9 csbeq1d ⊢ ( 𝑟 = 𝑅 → ⦋ ( Poly1 ‘ 𝑟 ) / 𝑝 ⦌ ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) = ⦋ 𝑃 / 𝑝 ⦌ ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) )
11 2 fvexi ⊢ 𝑃 ∈ V
12 11 a1i ⊢ ( 𝑟 = 𝑅 → 𝑃 ∈ V )
13 fveq2 ⊢ ( 𝑝 = 𝑃 → ( Base ‘ 𝑝 ) = ( Base ‘ 𝑃 ) )
14 13 adantl ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) → ( Base ‘ 𝑝 ) = ( Base ‘ 𝑃 ) )
15 14 3 eqtr4di ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) → ( Base ‘ 𝑝 ) = 𝐵 )
16 15 csbeq1d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) → ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) = ⦋ 𝐵 / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) )
17 3 fvexi ⊢ 𝐵 ∈ V
18 17 a1i ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) → 𝐵 ∈ V )
19 simpr ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
20 fveq2 ⊢ ( 𝑟 = 𝑅 → ( deg1 ‘ 𝑟 ) = ( deg1 ‘ 𝑅 ) )
21 20 ad2antrr ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( deg1 ‘ 𝑟 ) = ( deg1 ‘ 𝑅 ) )
22 21 4 eqtr4di ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( deg1 ‘ 𝑟 ) = 𝐷 )
23 fveq2 ⊢ ( 𝑝 = 𝑃 → ( -g ‘ 𝑝 ) = ( -g ‘ 𝑃 ) )
24 23 ad2antlr ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( -g ‘ 𝑝 ) = ( -g ‘ 𝑃 ) )
25 24 5 eqtr4di ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( -g ‘ 𝑝 ) = − )
26 eqidd ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → 𝑓 = 𝑓 )
27 fveq2 ⊢ ( 𝑝 = 𝑃 → ( .r ‘ 𝑝 ) = ( .r ‘ 𝑃 ) )
28 27 ad2antlr ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( .r ‘ 𝑝 ) = ( .r ‘ 𝑃 ) )
29 28 6 eqtr4di ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( .r ‘ 𝑝 ) = · )
30 29 oveqd ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) = ( 𝑞 · 𝑔 ) )
31 25 26 30 oveq123d ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) = ( 𝑓 − ( 𝑞 · 𝑔 ) ) )
32 22 31 fveq12d ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) = ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) )
33 22 fveq1d ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) = ( 𝐷 ‘ 𝑔 ) )
34 32 33 breq12d ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ↔ ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) )
35 19 34 riotaeqbidv ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) = ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) )
36 19 19 35 mpoeq123dv ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
37 18 36 csbied ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) → ⦋ 𝐵 / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
38 16 37 eqtrd ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) → ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
39 12 38 csbied ⊢ ( 𝑟 = 𝑅 → ⦋ 𝑃 / 𝑝 ⦌ ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
40 10 39 eqtrd ⊢ ( 𝑟 = 𝑅 → ⦋ ( Poly1 ‘ 𝑟 ) / 𝑝 ⦌ ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
41 df-q1p ⊢ quot1p = ( 𝑟 ∈ V ↦ ⦋ ( Poly1 ‘ 𝑟 ) / 𝑝 ⦌ ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) )
42 17 17 mpoex ⊢ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) ∈ V
43 40 41 42 fvmpt ⊢ ( 𝑅 ∈ V → ( quot1p ‘ 𝑅 ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
44 1 43 eqtrid ⊢ ( 𝑅 ∈ V → 𝑄 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
45 7 44 syl ⊢ ( 𝐺 ∈ 𝐵 → 𝑄 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
46 45 adantl ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝑄 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
47 id ⊢ ( 𝑓 = 𝐹 → 𝑓 = 𝐹 )
48 oveq2 ⊢ ( 𝑔 = 𝐺 → ( 𝑞 · 𝑔 ) = ( 𝑞 · 𝐺 ) )
49 47 48 oveqan12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 − ( 𝑞 · 𝑔 ) ) = ( 𝐹 − ( 𝑞 · 𝐺 ) ) )
50 49 fveq2d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) = ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) )
51 fveq2 ⊢ ( 𝑔 = 𝐺 → ( 𝐷 ‘ 𝑔 ) = ( 𝐷 ‘ 𝐺 ) )
52 51 adantl ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝐷 ‘ 𝑔 ) = ( 𝐷 ‘ 𝐺 ) )
53 50 52 breq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ↔ ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
54 53 riotabidv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) = ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
55 54 adantl ⊢ ( ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) = ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
56 simpl ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐹 ∈ 𝐵 )
57 simpr ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
58 riotaex ⊢ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ∈ V
59 58 a1i ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ∈ V )
60 46 55 56 57 59 ovmpod ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 𝑄 𝐺 ) = ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )