Step | Hyp | Ref
| Expression |
1 | | opex 5255 |
. . . 4
⊢
〈𝐹, 𝐺〉 ∈ V |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ V) |
3 | | resfval.d |
. . 3
⊢ (𝜑 → 𝐻 ∈ 𝑊) |
4 | 2, 3 | resfval 16995 |
. 2
⊢ (𝜑 → (〈𝐹, 𝐺〉 ↾f 𝐻) = 〈((1st
‘〈𝐹, 𝐺〉) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd
‘〈𝐹, 𝐺〉)‘𝑧) ↾ (𝐻‘𝑧)))〉) |
5 | | resfval.c |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
6 | | resfval2.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ 𝑋) |
7 | | op1stg 7564 |
. . . . 5
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑋) → (1st ‘〈𝐹, 𝐺〉) = 𝐹) |
8 | 5, 6, 7 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (1st
‘〈𝐹, 𝐺〉) = 𝐹) |
9 | | resfval2.d |
. . . . . . 7
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) |
10 | | fndm 6332 |
. . . . . . 7
⊢ (𝐻 Fn (𝑆 × 𝑆) → dom 𝐻 = (𝑆 × 𝑆)) |
11 | 9, 10 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom 𝐻 = (𝑆 × 𝑆)) |
12 | 11 | dmeqd 5667 |
. . . . 5
⊢ (𝜑 → dom dom 𝐻 = dom (𝑆 × 𝑆)) |
13 | | dmxpid 5689 |
. . . . 5
⊢ dom
(𝑆 × 𝑆) = 𝑆 |
14 | 12, 13 | syl6eq 2849 |
. . . 4
⊢ (𝜑 → dom dom 𝐻 = 𝑆) |
15 | 8, 14 | reseq12d 5742 |
. . 3
⊢ (𝜑 → ((1st
‘〈𝐹, 𝐺〉) ↾ dom dom 𝐻) = (𝐹 ↾ 𝑆)) |
16 | | op2ndg 7565 |
. . . . . . . 8
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑋) → (2nd ‘〈𝐹, 𝐺〉) = 𝐺) |
17 | 5, 6, 16 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (2nd
‘〈𝐹, 𝐺〉) = 𝐺) |
18 | 17 | fveq1d 6547 |
. . . . . 6
⊢ (𝜑 → ((2nd
‘〈𝐹, 𝐺〉)‘𝑧) = (𝐺‘𝑧)) |
19 | 18 | reseq1d 5740 |
. . . . 5
⊢ (𝜑 → (((2nd
‘〈𝐹, 𝐺〉)‘𝑧) ↾ (𝐻‘𝑧)) = ((𝐺‘𝑧) ↾ (𝐻‘𝑧))) |
20 | 11, 19 | mpteq12dv 5052 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ dom 𝐻 ↦ (((2nd
‘〈𝐹, 𝐺〉)‘𝑧) ↾ (𝐻‘𝑧))) = (𝑧 ∈ (𝑆 × 𝑆) ↦ ((𝐺‘𝑧) ↾ (𝐻‘𝑧)))) |
21 | | fveq2 6545 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐺‘𝑧) = (𝐺‘〈𝑥, 𝑦〉)) |
22 | | df-ov 7026 |
. . . . . . 7
⊢ (𝑥𝐺𝑦) = (𝐺‘〈𝑥, 𝑦〉) |
23 | 21, 22 | syl6eqr 2851 |
. . . . . 6
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐺‘𝑧) = (𝑥𝐺𝑦)) |
24 | | fveq2 6545 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝐻‘〈𝑥, 𝑦〉)) |
25 | | df-ov 7026 |
. . . . . . 7
⊢ (𝑥𝐻𝑦) = (𝐻‘〈𝑥, 𝑦〉) |
26 | 24, 25 | syl6eqr 2851 |
. . . . . 6
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝑥𝐻𝑦)) |
27 | 23, 26 | reseq12d 5742 |
. . . . 5
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐺‘𝑧) ↾ (𝐻‘𝑧)) = ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦))) |
28 | 27 | mpompt 7129 |
. . . 4
⊢ (𝑧 ∈ (𝑆 × 𝑆) ↦ ((𝐺‘𝑧) ↾ (𝐻‘𝑧))) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦))) |
29 | 20, 28 | syl6eq 2849 |
. . 3
⊢ (𝜑 → (𝑧 ∈ dom 𝐻 ↦ (((2nd
‘〈𝐹, 𝐺〉)‘𝑧) ↾ (𝐻‘𝑧))) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦)))) |
30 | 15, 29 | opeq12d 4724 |
. 2
⊢ (𝜑 → 〈((1st
‘〈𝐹, 𝐺〉) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd
‘〈𝐹, 𝐺〉)‘𝑧) ↾ (𝐻‘𝑧)))〉 = 〈(𝐹 ↾ 𝑆), (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦)))〉) |
31 | 4, 30 | eqtrd 2833 |
1
⊢ (𝜑 → (〈𝐹, 𝐺〉 ↾f 𝐻) = 〈(𝐹 ↾ 𝑆), (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦)))〉) |