| Step | Hyp | Ref
| Expression |
| 1 | | elinel2 4202 |
. . . . 5
⊢ (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) → 𝑥 ∈ 𝐷) |
| 2 | | fvres 6925 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((𝐹 ↾ 𝐷)‘𝑥) = (𝐹‘𝑥)) |
| 3 | | fvres 6925 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((𝐺 ↾ 𝐷)‘𝑥) = (𝐺‘𝑥)) |
| 4 | 2, 3 | oveq12d 7449 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥)) = ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) |
| 5 | 1, 4 | syl 17 |
. . . 4
⊢ (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) → (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥)) = ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) |
| 6 | 5 | mpteq2ia 5245 |
. . 3
⊢ (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) ↦ (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥))) = (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) |
| 7 | | inindi 4235 |
. . . . 5
⊢ (𝐷 ∩ (dom 𝐹 ∩ dom 𝐺)) = ((𝐷 ∩ dom 𝐹) ∩ (𝐷 ∩ dom 𝐺)) |
| 8 | | incom 4209 |
. . . . 5
⊢ ((dom
𝐹 ∩ dom 𝐺) ∩ 𝐷) = (𝐷 ∩ (dom 𝐹 ∩ dom 𝐺)) |
| 9 | | dmres 6030 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝐷) = (𝐷 ∩ dom 𝐹) |
| 10 | | dmres 6030 |
. . . . . 6
⊢ dom
(𝐺 ↾ 𝐷) = (𝐷 ∩ dom 𝐺) |
| 11 | 9, 10 | ineq12i 4218 |
. . . . 5
⊢ (dom
(𝐹 ↾ 𝐷) ∩ dom (𝐺 ↾ 𝐷)) = ((𝐷 ∩ dom 𝐹) ∩ (𝐷 ∩ dom 𝐺)) |
| 12 | 7, 8, 11 | 3eqtr4ri 2776 |
. . . 4
⊢ (dom
(𝐹 ↾ 𝐷) ∩ dom (𝐺 ↾ 𝐷)) = ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) |
| 13 | 12 | mpteq1i 5238 |
. . 3
⊢ (𝑥 ∈ (dom (𝐹 ↾ 𝐷) ∩ dom (𝐺 ↾ 𝐷)) ↦ (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥))) = (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) ↦ (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥))) |
| 14 | | resmpt3 6056 |
. . 3
⊢ ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) ↾ 𝐷) = (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) |
| 15 | 6, 13, 14 | 3eqtr4ri 2776 |
. 2
⊢ ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) ↾ 𝐷) = (𝑥 ∈ (dom (𝐹 ↾ 𝐷) ∩ dom (𝐺 ↾ 𝐷)) ↦ (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥))) |
| 16 | | offval3 8007 |
. . 3
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) |
| 17 | 16 | reseq1d 5996 |
. 2
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘f 𝑅𝐺) ↾ 𝐷) = ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) ↾ 𝐷)) |
| 18 | | resexg 6045 |
. . 3
⊢ (𝐹 ∈ 𝑉 → (𝐹 ↾ 𝐷) ∈ V) |
| 19 | | resexg 6045 |
. . 3
⊢ (𝐺 ∈ 𝑊 → (𝐺 ↾ 𝐷) ∈ V) |
| 20 | | offval3 8007 |
. . 3
⊢ (((𝐹 ↾ 𝐷) ∈ V ∧ (𝐺 ↾ 𝐷) ∈ V) → ((𝐹 ↾ 𝐷) ∘f 𝑅(𝐺 ↾ 𝐷)) = (𝑥 ∈ (dom (𝐹 ↾ 𝐷) ∩ dom (𝐺 ↾ 𝐷)) ↦ (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥)))) |
| 21 | 18, 19, 20 | syl2an 596 |
. 2
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ↾ 𝐷) ∘f 𝑅(𝐺 ↾ 𝐷)) = (𝑥 ∈ (dom (𝐹 ↾ 𝐷) ∩ dom (𝐺 ↾ 𝐷)) ↦ (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥)))) |
| 22 | 15, 17, 21 | 3eqtr4a 2803 |
1
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘f 𝑅𝐺) ↾ 𝐷) = ((𝐹 ↾ 𝐷) ∘f 𝑅(𝐺 ↾ 𝐷))) |