Step | Hyp | Ref
| Expression |
1 | | inss2 3348 |
. . . . . 6
⊢ ((dom
𝐹 ∩ dom 𝐺) ∩ 𝐷) ⊆ 𝐷 |
2 | 1 | sseli 3143 |
. . . . 5
⊢ (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) → 𝑥 ∈ 𝐷) |
3 | | fvres 5520 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((𝐹 ↾ 𝐷)‘𝑥) = (𝐹‘𝑥)) |
4 | | fvres 5520 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((𝐺 ↾ 𝐷)‘𝑥) = (𝐺‘𝑥)) |
5 | 3, 4 | oveq12d 5871 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥)) = ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) |
6 | 2, 5 | syl 14 |
. . . 4
⊢ (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) → (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥)) = ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) |
7 | 6 | mpteq2ia 4075 |
. . 3
⊢ (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) ↦ (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥))) = (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) |
8 | | inindi 3344 |
. . . . 5
⊢ (𝐷 ∩ (dom 𝐹 ∩ dom 𝐺)) = ((𝐷 ∩ dom 𝐹) ∩ (𝐷 ∩ dom 𝐺)) |
9 | | incom 3319 |
. . . . 5
⊢ ((dom
𝐹 ∩ dom 𝐺) ∩ 𝐷) = (𝐷 ∩ (dom 𝐹 ∩ dom 𝐺)) |
10 | | dmres 4912 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝐷) = (𝐷 ∩ dom 𝐹) |
11 | | dmres 4912 |
. . . . . 6
⊢ dom
(𝐺 ↾ 𝐷) = (𝐷 ∩ dom 𝐺) |
12 | 10, 11 | ineq12i 3326 |
. . . . 5
⊢ (dom
(𝐹 ↾ 𝐷) ∩ dom (𝐺 ↾ 𝐷)) = ((𝐷 ∩ dom 𝐹) ∩ (𝐷 ∩ dom 𝐺)) |
13 | 8, 9, 12 | 3eqtr4ri 2202 |
. . . 4
⊢ (dom
(𝐹 ↾ 𝐷) ∩ dom (𝐺 ↾ 𝐷)) = ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) |
14 | | eqid 2170 |
. . . 4
⊢ (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥)) = (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥)) |
15 | 13, 14 | mpteq12i 4077 |
. . 3
⊢ (𝑥 ∈ (dom (𝐹 ↾ 𝐷) ∩ dom (𝐺 ↾ 𝐷)) ↦ (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥))) = (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) ↦ (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥))) |
16 | | resmpt3 4940 |
. . 3
⊢ ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) ↾ 𝐷) = (𝑥 ∈ ((dom 𝐹 ∩ dom 𝐺) ∩ 𝐷) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) |
17 | 7, 15, 16 | 3eqtr4ri 2202 |
. 2
⊢ ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) ↾ 𝐷) = (𝑥 ∈ (dom (𝐹 ↾ 𝐷) ∩ dom (𝐺 ↾ 𝐷)) ↦ (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥))) |
18 | | offval3 6113 |
. . 3
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) |
19 | 18 | reseq1d 4890 |
. 2
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘𝑓 𝑅𝐺) ↾ 𝐷) = ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) ↾ 𝐷)) |
20 | | resexg 4931 |
. . 3
⊢ (𝐹 ∈ 𝑉 → (𝐹 ↾ 𝐷) ∈ V) |
21 | | resexg 4931 |
. . 3
⊢ (𝐺 ∈ 𝑊 → (𝐺 ↾ 𝐷) ∈ V) |
22 | | offval3 6113 |
. . 3
⊢ (((𝐹 ↾ 𝐷) ∈ V ∧ (𝐺 ↾ 𝐷) ∈ V) → ((𝐹 ↾ 𝐷) ∘𝑓 𝑅(𝐺 ↾ 𝐷)) = (𝑥 ∈ (dom (𝐹 ↾ 𝐷) ∩ dom (𝐺 ↾ 𝐷)) ↦ (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥)))) |
23 | 20, 21, 22 | syl2an 287 |
. 2
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ↾ 𝐷) ∘𝑓 𝑅(𝐺 ↾ 𝐷)) = (𝑥 ∈ (dom (𝐹 ↾ 𝐷) ∩ dom (𝐺 ↾ 𝐷)) ↦ (((𝐹 ↾ 𝐷)‘𝑥)𝑅((𝐺 ↾ 𝐷)‘𝑥)))) |
24 | 17, 19, 23 | 3eqtr4a 2229 |
1
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘𝑓 𝑅𝐺) ↾ 𝐷) = ((𝐹 ↾ 𝐷) ∘𝑓 𝑅(𝐺 ↾ 𝐷))) |