Step | Hyp | Ref
| Expression |
1 | | q1pval.p |
. . . . 5
⊢ 𝑃 = (Poly1‘𝑅) |
2 | | q1pval.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑃) |
3 | 1, 2 | elbasfv 15748 |
. . . 4
⊢ (𝐺 ∈ 𝐵 → 𝑅 ∈ V) |
4 | | q1pval.q |
. . . . 5
⊢ 𝑄 =
(quot1p‘𝑅) |
5 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) =
(Poly1‘𝑅)) |
6 | 5, 1 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) = 𝑃) |
7 | 6 | csbeq1d 3506 |
. . . . . . 7
⊢ (𝑟 = 𝑅 →
⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔))) = ⦋𝑃 / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)))) |
8 | | fvex 6113 |
. . . . . . . . . 10
⊢
(Poly1‘𝑅) ∈ V |
9 | 1, 8 | eqeltri 2684 |
. . . . . . . . 9
⊢ 𝑃 ∈ V |
10 | 9 | a1i 11 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → 𝑃 ∈ V) |
11 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑃 → (Base‘𝑝) = (Base‘𝑃)) |
12 | 11 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) → (Base‘𝑝) = (Base‘𝑃)) |
13 | 12, 2 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) → (Base‘𝑝) = 𝐵) |
14 | 13 | csbeq1d 3506 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) → ⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔))) = ⦋𝐵 / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)))) |
15 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(Base‘𝑃)
∈ V |
16 | 2, 15 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ V |
17 | 16 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) → 𝐵 ∈ V) |
18 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
19 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑅 → ( deg1 ‘𝑟) = ( deg1
‘𝑅)) |
20 | 19 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) ∧ 𝑏 = 𝐵) → ( deg1 ‘𝑟) = ( deg1
‘𝑅)) |
21 | | q1pval.d |
. . . . . . . . . . . . . . 15
⊢ 𝐷 = ( deg1
‘𝑅) |
22 | 20, 21 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) ∧ 𝑏 = 𝐵) → ( deg1 ‘𝑟) = 𝐷) |
23 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 𝑃 → (-g‘𝑝) = (-g‘𝑃)) |
24 | 23 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) ∧ 𝑏 = 𝐵) → (-g‘𝑝) = (-g‘𝑃)) |
25 | | q1pval.m |
. . . . . . . . . . . . . . . 16
⊢ − =
(-g‘𝑃) |
26 | 24, 25 | syl6eqr 2662 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) ∧ 𝑏 = 𝐵) → (-g‘𝑝) = − ) |
27 | | eqidd 2611 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) ∧ 𝑏 = 𝐵) → 𝑓 = 𝑓) |
28 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 𝑃 → (.r‘𝑝) = (.r‘𝑃)) |
29 | 28 | ad2antlr 759 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) ∧ 𝑏 = 𝐵) → (.r‘𝑝) = (.r‘𝑃)) |
30 | | q1pval.t |
. . . . . . . . . . . . . . . . 17
⊢ · =
(.r‘𝑃) |
31 | 29, 30 | syl6eqr 2662 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) ∧ 𝑏 = 𝐵) → (.r‘𝑝) = · ) |
32 | 31 | oveqd 6566 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) ∧ 𝑏 = 𝐵) → (𝑞(.r‘𝑝)𝑔) = (𝑞 · 𝑔)) |
33 | 26, 27, 32 | oveq123d 6570 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) ∧ 𝑏 = 𝐵) → (𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔)) = (𝑓 − (𝑞 · 𝑔))) |
34 | 22, 33 | fveq12d 6109 |
. . . . . . . . . . . . 13
⊢ (((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) ∧ 𝑏 = 𝐵) → (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) = (𝐷‘(𝑓 − (𝑞 · 𝑔)))) |
35 | 22 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ (((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) ∧ 𝑏 = 𝐵) → (( deg1 ‘𝑟)‘𝑔) = (𝐷‘𝑔)) |
36 | 34, 35 | breq12d 4596 |
. . . . . . . . . . . 12
⊢ (((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) ∧ 𝑏 = 𝐵) → ((( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔) ↔ (𝐷‘(𝑓 − (𝑞 · 𝑔))) < (𝐷‘𝑔))) |
37 | 18, 36 | riotaeqbidv 6514 |
. . . . . . . . . . 11
⊢ (((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) ∧ 𝑏 = 𝐵) → (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)) = (℩𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝑞 · 𝑔))) < (𝐷‘𝑔))) |
38 | 18, 18, 37 | mpt2eq123dv 6615 |
. . . . . . . . . 10
⊢ (((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) ∧ 𝑏 = 𝐵) → (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (℩𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝑞 · 𝑔))) < (𝐷‘𝑔)))) |
39 | 17, 38 | csbied 3526 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) → ⦋𝐵 / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (℩𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝑞 · 𝑔))) < (𝐷‘𝑔)))) |
40 | 14, 39 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑝 = 𝑃) → ⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (℩𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝑞 · 𝑔))) < (𝐷‘𝑔)))) |
41 | 10, 40 | csbied 3526 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ⦋𝑃 / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (℩𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝑞 · 𝑔))) < (𝐷‘𝑔)))) |
42 | 7, 41 | eqtrd 2644 |
. . . . . 6
⊢ (𝑟 = 𝑅 →
⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (℩𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝑞 · 𝑔))) < (𝐷‘𝑔)))) |
43 | | df-q1p 23696 |
. . . . . 6
⊢
quot1p = (𝑟 ∈ V ↦
⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)))) |
44 | 16, 16 | mpt2ex 7136 |
. . . . . 6
⊢ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (℩𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝑞 · 𝑔))) < (𝐷‘𝑔))) ∈ V |
45 | 42, 43, 44 | fvmpt 6191 |
. . . . 5
⊢ (𝑅 ∈ V →
(quot1p‘𝑅)
= (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (℩𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝑞 · 𝑔))) < (𝐷‘𝑔)))) |
46 | 4, 45 | syl5eq 2656 |
. . . 4
⊢ (𝑅 ∈ V → 𝑄 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (℩𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝑞 · 𝑔))) < (𝐷‘𝑔)))) |
47 | 3, 46 | syl 17 |
. . 3
⊢ (𝐺 ∈ 𝐵 → 𝑄 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (℩𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝑞 · 𝑔))) < (𝐷‘𝑔)))) |
48 | 47 | adantl 481 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑄 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (℩𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝑞 · 𝑔))) < (𝐷‘𝑔)))) |
49 | | id 22 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → 𝑓 = 𝐹) |
50 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑞 · 𝑔) = (𝑞 · 𝐺)) |
51 | 49, 50 | oveqan12d 6568 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓 − (𝑞 · 𝑔)) = (𝐹 − (𝑞 · 𝐺))) |
52 | 51 | fveq2d 6107 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝐷‘(𝑓 − (𝑞 · 𝑔))) = (𝐷‘(𝐹 − (𝑞 · 𝐺)))) |
53 | | fveq2 6103 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (𝐷‘𝑔) = (𝐷‘𝐺)) |
54 | 53 | adantl 481 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝐷‘𝑔) = (𝐷‘𝐺)) |
55 | 52, 54 | breq12d 4596 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝐷‘(𝑓 − (𝑞 · 𝑔))) < (𝐷‘𝑔) ↔ (𝐷‘(𝐹 − (𝑞 · 𝐺))) < (𝐷‘𝐺))) |
56 | 55 | riotabidv 6513 |
. . 3
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (℩𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝑞 · 𝑔))) < (𝐷‘𝑔)) = (℩𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝑞 · 𝐺))) < (𝐷‘𝐺))) |
57 | 56 | adantl 481 |
. 2
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → (℩𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝑞 · 𝑔))) < (𝐷‘𝑔)) = (℩𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝑞 · 𝐺))) < (𝐷‘𝐺))) |
58 | | simpl 472 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ 𝐵) |
59 | | simpr 476 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ 𝐵) |
60 | | riotaex 6515 |
. . 3
⊢
(℩𝑞
∈ 𝐵 (𝐷‘(𝐹 − (𝑞 · 𝐺))) < (𝐷‘𝐺)) ∈ V |
61 | 60 | a1i 11 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (℩𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝑞 · 𝐺))) < (𝐷‘𝐺)) ∈ V) |
62 | 48, 57, 58, 59, 61 | ovmpt2d 6686 |
1
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹𝑄𝐺) = (℩𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝑞 · 𝐺))) < (𝐷‘𝐺))) |