Step | Hyp | Ref
| Expression |
1 | | r1pval.p |
. . . . 5
⊢ 𝑃 = (Poly1‘𝑅) |
2 | | r1pval.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑃) |
3 | 1, 2 | elbasfv 15748 |
. . . 4
⊢ (𝐹 ∈ 𝐵 → 𝑅 ∈ V) |
4 | 3 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑅 ∈ V) |
5 | | r1pval.e |
. . . 4
⊢ 𝐸 = (rem1p‘𝑅) |
6 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) =
(Poly1‘𝑅)) |
7 | 6, 1 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) = 𝑃) |
8 | 7 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 →
(Base‘(Poly1‘𝑟)) = (Base‘𝑃)) |
9 | 8, 2 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑟 = 𝑅 →
(Base‘(Poly1‘𝑟)) = 𝐵) |
10 | 9 | csbeq1d 3506 |
. . . . . 6
⊢ (𝑟 = 𝑅 →
⦋(Base‘(Poly1‘𝑟)) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔))) = ⦋𝐵 / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔)))) |
11 | | fvex 6113 |
. . . . . . . . 9
⊢
(Base‘𝑃)
∈ V |
12 | 2, 11 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
13 | 12 | a1i 11 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → 𝐵 ∈ V) |
14 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
15 | 7 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 →
(-g‘(Poly1‘𝑟)) = (-g‘𝑃)) |
16 | | r1pval.m |
. . . . . . . . . . 11
⊢ − =
(-g‘𝑃) |
17 | 15, 16 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 →
(-g‘(Poly1‘𝑟)) = − ) |
18 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → 𝑓 = 𝑓) |
19 | 7 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 →
(.r‘(Poly1‘𝑟)) = (.r‘𝑃)) |
20 | | r1pval.t |
. . . . . . . . . . . 12
⊢ · =
(.r‘𝑃) |
21 | 19, 20 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 →
(.r‘(Poly1‘𝑟)) = · ) |
22 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑅 → (quot1p‘𝑟) =
(quot1p‘𝑅)) |
23 | | r1pval.q |
. . . . . . . . . . . . 13
⊢ 𝑄 =
(quot1p‘𝑅) |
24 | 22, 23 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (quot1p‘𝑟) = 𝑄) |
25 | 24 | oveqd 6566 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (𝑓(quot1p‘𝑟)𝑔) = (𝑓𝑄𝑔)) |
26 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → 𝑔 = 𝑔) |
27 | 21, 25, 26 | oveq123d 6570 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → ((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔) = ((𝑓𝑄𝑔) · 𝑔)) |
28 | 17, 18, 27 | oveq123d 6570 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔)) = (𝑓 − ((𝑓𝑄𝑔) · 𝑔))) |
29 | 28 | adantr 480 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔)) = (𝑓 − ((𝑓𝑄𝑔) · 𝑔))) |
30 | 14, 14, 29 | mpt2eq123dv 6615 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 − ((𝑓𝑄𝑔) · 𝑔)))) |
31 | 13, 30 | csbied 3526 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ⦋𝐵 / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 − ((𝑓𝑄𝑔) · 𝑔)))) |
32 | 10, 31 | eqtrd 2644 |
. . . . 5
⊢ (𝑟 = 𝑅 →
⦋(Base‘(Poly1‘𝑟)) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 − ((𝑓𝑄𝑔) · 𝑔)))) |
33 | | df-r1p 23697 |
. . . . 5
⊢
rem1p = (𝑟 ∈ V ↦
⦋(Base‘(Poly1‘𝑟)) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔)))) |
34 | 12, 12 | mpt2ex 7136 |
. . . . 5
⊢ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 − ((𝑓𝑄𝑔) · 𝑔))) ∈ V |
35 | 32, 33, 34 | fvmpt 6191 |
. . . 4
⊢ (𝑅 ∈ V →
(rem1p‘𝑅)
= (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 − ((𝑓𝑄𝑔) · 𝑔)))) |
36 | 5, 35 | syl5eq 2656 |
. . 3
⊢ (𝑅 ∈ V → 𝐸 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 − ((𝑓𝑄𝑔) · 𝑔)))) |
37 | 4, 36 | syl 17 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐸 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 − ((𝑓𝑄𝑔) · 𝑔)))) |
38 | | simpl 472 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹) |
39 | | oveq12 6558 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓𝑄𝑔) = (𝐹𝑄𝐺)) |
40 | | simpr 476 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
41 | 39, 40 | oveq12d 6567 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓𝑄𝑔) · 𝑔) = ((𝐹𝑄𝐺) · 𝐺)) |
42 | 38, 41 | oveq12d 6567 |
. . 3
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓 − ((𝑓𝑄𝑔) · 𝑔)) = (𝐹 − ((𝐹𝑄𝐺) · 𝐺))) |
43 | 42 | adantl 481 |
. 2
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → (𝑓 − ((𝑓𝑄𝑔) · 𝑔)) = (𝐹 − ((𝐹𝑄𝐺) · 𝐺))) |
44 | | simpl 472 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ 𝐵) |
45 | | simpr 476 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ 𝐵) |
46 | | ovex 6577 |
. . 3
⊢ (𝐹 − ((𝐹𝑄𝐺) · 𝐺)) ∈ V |
47 | 46 | a1i 11 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 − ((𝐹𝑄𝐺) · 𝐺)) ∈ V) |
48 | 37, 43, 44, 45, 47 | ovmpt2d 6686 |
1
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹𝐸𝐺) = (𝐹 − ((𝐹𝑄𝐺) · 𝐺))) |