| Step | Hyp | Ref
| Expression |
| 1 | | r1pval.p |
. . . . 5
⊢ 𝑃 = (Poly1‘𝑅) |
| 2 | | r1pval.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑃) |
| 3 | 1, 2 | elbasfv 17253 |
. . . 4
⊢ (𝐹 ∈ 𝐵 → 𝑅 ∈ V) |
| 4 | 3 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑅 ∈ V) |
| 5 | | r1pval.e |
. . . 4
⊢ 𝐸 = (rem1p‘𝑅) |
| 6 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) =
(Poly1‘𝑅)) |
| 7 | 6, 1 | eqtr4di 2795 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) = 𝑃) |
| 8 | 7 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 →
(Base‘(Poly1‘𝑟)) = (Base‘𝑃)) |
| 9 | 8, 2 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑟 = 𝑅 →
(Base‘(Poly1‘𝑟)) = 𝐵) |
| 10 | 9 | csbeq1d 3903 |
. . . . . 6
⊢ (𝑟 = 𝑅 →
⦋(Base‘(Poly1‘𝑟)) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔))) = ⦋𝐵 / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔)))) |
| 11 | 2 | fvexi 6920 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
| 12 | 11 | a1i 11 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → 𝐵 ∈ V) |
| 13 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
| 14 | 7 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 →
(-g‘(Poly1‘𝑟)) = (-g‘𝑃)) |
| 15 | | r1pval.m |
. . . . . . . . . . 11
⊢ − =
(-g‘𝑃) |
| 16 | 14, 15 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 →
(-g‘(Poly1‘𝑟)) = − ) |
| 17 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → 𝑓 = 𝑓) |
| 18 | 7 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 →
(.r‘(Poly1‘𝑟)) = (.r‘𝑃)) |
| 19 | | r1pval.t |
. . . . . . . . . . . 12
⊢ · =
(.r‘𝑃) |
| 20 | 18, 19 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 →
(.r‘(Poly1‘𝑟)) = · ) |
| 21 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑅 → (quot1p‘𝑟) =
(quot1p‘𝑅)) |
| 22 | | r1pval.q |
. . . . . . . . . . . . 13
⊢ 𝑄 =
(quot1p‘𝑅) |
| 23 | 21, 22 | eqtr4di 2795 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (quot1p‘𝑟) = 𝑄) |
| 24 | 23 | oveqd 7448 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (𝑓(quot1p‘𝑟)𝑔) = (𝑓𝑄𝑔)) |
| 25 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → 𝑔 = 𝑔) |
| 26 | 20, 24, 25 | oveq123d 7452 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → ((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔) = ((𝑓𝑄𝑔) · 𝑔)) |
| 27 | 16, 17, 26 | oveq123d 7452 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔)) = (𝑓 − ((𝑓𝑄𝑔) · 𝑔))) |
| 28 | 27 | adantr 480 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔)) = (𝑓 − ((𝑓𝑄𝑔) · 𝑔))) |
| 29 | 13, 13, 28 | mpoeq123dv 7508 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 − ((𝑓𝑄𝑔) · 𝑔)))) |
| 30 | 12, 29 | csbied 3935 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ⦋𝐵 / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 − ((𝑓𝑄𝑔) · 𝑔)))) |
| 31 | 10, 30 | eqtrd 2777 |
. . . . 5
⊢ (𝑟 = 𝑅 →
⦋(Base‘(Poly1‘𝑟)) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 − ((𝑓𝑄𝑔) · 𝑔)))) |
| 32 | | df-r1p 26173 |
. . . . 5
⊢
rem1p = (𝑟 ∈ V ↦
⦋(Base‘(Poly1‘𝑟)) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔)))) |
| 33 | 11, 11 | mpoex 8104 |
. . . . 5
⊢ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 − ((𝑓𝑄𝑔) · 𝑔))) ∈ V |
| 34 | 31, 32, 33 | fvmpt 7016 |
. . . 4
⊢ (𝑅 ∈ V →
(rem1p‘𝑅)
= (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 − ((𝑓𝑄𝑔) · 𝑔)))) |
| 35 | 5, 34 | eqtrid 2789 |
. . 3
⊢ (𝑅 ∈ V → 𝐸 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 − ((𝑓𝑄𝑔) · 𝑔)))) |
| 36 | 4, 35 | syl 17 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐸 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 − ((𝑓𝑄𝑔) · 𝑔)))) |
| 37 | | simpl 482 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹) |
| 38 | | oveq12 7440 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓𝑄𝑔) = (𝐹𝑄𝐺)) |
| 39 | | simpr 484 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
| 40 | 38, 39 | oveq12d 7449 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓𝑄𝑔) · 𝑔) = ((𝐹𝑄𝐺) · 𝐺)) |
| 41 | 37, 40 | oveq12d 7449 |
. . 3
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓 − ((𝑓𝑄𝑔) · 𝑔)) = (𝐹 − ((𝐹𝑄𝐺) · 𝐺))) |
| 42 | 41 | adantl 481 |
. 2
⊢ (((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → (𝑓 − ((𝑓𝑄𝑔) · 𝑔)) = (𝐹 − ((𝐹𝑄𝐺) · 𝐺))) |
| 43 | | simpl 482 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ 𝐵) |
| 44 | | simpr 484 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ 𝐵) |
| 45 | | ovexd 7466 |
. 2
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 − ((𝐹𝑄𝐺) · 𝐺)) ∈ V) |
| 46 | 36, 42, 43, 44, 45 | ovmpod 7585 |
1
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹𝐸𝐺) = (𝐹 − ((𝐹𝑄𝐺) · 𝐺))) |