Step | Hyp | Ref
| Expression |
1 | | ovex 6678 |
. . . . . 6
⊢
((2nd ‘𝑢)𝐻𝑧) ∈ V |
2 | | fvex 6201 |
. . . . . 6
⊢ (𝐻‘𝑢) ∈ V |
3 | 1, 2 | mpt2ex 7247 |
. . . . 5
⊢ (𝑔 ∈ ((2nd
‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) ∈ V |
4 | 3 | rgen2w 2925 |
. . . 4
⊢
∀𝑢 ∈
(𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) ∈ V |
5 | | mpt22eqb 6769 |
. . . 4
⊢
(∀𝑢 ∈
(𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) ∈ V → ((𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) ↔ ∀𝑢 ∈ (𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)))) |
6 | 4, 5 | ax-mp 5 |
. . 3
⊢ ((𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) ↔ ∀𝑢 ∈ (𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) |
7 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
8 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
9 | 7, 8 | op2ndd 7179 |
. . . . . . . 8
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (2nd ‘𝑢) = 𝑦) |
10 | 9 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑢 = 〈𝑥, 𝑦〉 → ((2nd ‘𝑢)𝐻𝑧) = (𝑦𝐻𝑧)) |
11 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝐻‘𝑢) = (𝐻‘〈𝑥, 𝑦〉)) |
12 | | df-ov 6653 |
. . . . . . . . 9
⊢ (𝑥𝐻𝑦) = (𝐻‘〈𝑥, 𝑦〉) |
13 | 11, 12 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝐻‘𝑢) = (𝑥𝐻𝑦)) |
14 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝑢 · 𝑧) = (〈𝑥, 𝑦〉 · 𝑧)) |
15 | 14 | oveqd 6667 |
. . . . . . . . 9
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝑔(𝑢 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) |
16 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝑢 ∙ 𝑧) = (〈𝑥, 𝑦〉 ∙ 𝑧)) |
17 | 16 | oveqd 6667 |
. . . . . . . . 9
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝑔(𝑢 ∙ 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓)) |
18 | 15, 17 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑢 = 〈𝑥, 𝑦〉 → ((𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓) ↔ (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |
19 | 13, 18 | raleqbidv 3152 |
. . . . . . 7
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓) ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |
20 | 10, 19 | raleqbidv 3152 |
. . . . . 6
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (∀𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)∀𝑓 ∈ (𝑥𝐻𝑦)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |
21 | | ovex 6678 |
. . . . . . . 8
⊢ (𝑔(𝑢 · 𝑧)𝑓) ∈ V |
22 | 21 | rgen2w 2925 |
. . . . . . 7
⊢
∀𝑔 ∈
((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) ∈ V |
23 | | mpt22eqb 6769 |
. . . . . . 7
⊢
(∀𝑔 ∈
((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) ∈ V → ((𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓))) |
24 | 22, 23 | ax-mp 5 |
. . . . . 6
⊢ ((𝑔 ∈ ((2nd
‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓)) |
25 | | ralcom 3098 |
. . . . . 6
⊢
(∀𝑓 ∈
(𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)∀𝑓 ∈ (𝑥𝐻𝑦)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓)) |
26 | 20, 24, 25 | 3bitr4g 303 |
. . . . 5
⊢ (𝑢 = 〈𝑥, 𝑦〉 → ((𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |
27 | 26 | ralbidv 2986 |
. . . 4
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |
28 | 27 | ralxp 5263 |
. . 3
⊢
(∀𝑢 ∈
(𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓)) |
29 | 6, 28 | bitri 264 |
. 2
⊢ ((𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓)) |
30 | | comfeq.3 |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) |
31 | 30 | sqxpeqd 5141 |
. . . . 5
⊢ (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐶) × (Base‘𝐶))) |
32 | | eqidd 2623 |
. . . . 5
⊢ (𝜑 → (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) |
33 | 31, 30, 32 | mpt2eq123dv 6717 |
. . . 4
⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)))) |
34 | | eqid 2622 |
. . . . 5
⊢
(compf‘𝐶) = (compf‘𝐶) |
35 | | eqid 2622 |
. . . . 5
⊢
(Base‘𝐶) =
(Base‘𝐶) |
36 | | comfeq.h |
. . . . 5
⊢ 𝐻 = (Hom ‘𝐶) |
37 | | comfeq.1 |
. . . . 5
⊢ · =
(comp‘𝐶) |
38 | 34, 35, 36, 37 | comfffval 16358 |
. . . 4
⊢
(compf‘𝐶) = (𝑢 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) |
39 | 33, 38 | syl6eqr 2674 |
. . 3
⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (compf‘𝐶)) |
40 | | eqid 2622 |
. . . . . . . 8
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
41 | | comfeq.5 |
. . . . . . . . 9
⊢ (𝜑 → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
42 | 41 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
43 | | xp2nd 7199 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (𝐵 × 𝐵) → (2nd ‘𝑢) ∈ 𝐵) |
44 | 43 | 3ad2ant2 1083 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (2nd ‘𝑢) ∈ 𝐵) |
45 | 30 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝐵 = (Base‘𝐶)) |
46 | 44, 45 | eleqtrd 2703 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (2nd ‘𝑢) ∈ (Base‘𝐶)) |
47 | | simp3 1063 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵) |
48 | 47, 45 | eleqtrd 2703 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ (Base‘𝐶)) |
49 | 35, 36, 40, 42, 46, 48 | homfeqval 16357 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → ((2nd ‘𝑢)𝐻𝑧) = ((2nd ‘𝑢)(Hom ‘𝐷)𝑧)) |
50 | | xp1st 7198 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (𝐵 × 𝐵) → (1st ‘𝑢) ∈ 𝐵) |
51 | 50 | 3ad2ant2 1083 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (1st ‘𝑢) ∈ 𝐵) |
52 | 51, 45 | eleqtrd 2703 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (1st ‘𝑢) ∈ (Base‘𝐶)) |
53 | 35, 36, 40, 42, 52, 46 | homfeqval 16357 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → ((1st ‘𝑢)𝐻(2nd ‘𝑢)) = ((1st ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑢))) |
54 | | df-ov 6653 |
. . . . . . . . 9
⊢
((1st ‘𝑢)𝐻(2nd ‘𝑢)) = (𝐻‘〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
55 | | df-ov 6653 |
. . . . . . . . 9
⊢
((1st ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑢)) = ((Hom ‘𝐷)‘〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
56 | 53, 54, 55 | 3eqtr3g 2679 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝐻‘〈(1st ‘𝑢), (2nd ‘𝑢)〉) = ((Hom ‘𝐷)‘〈(1st
‘𝑢), (2nd
‘𝑢)〉)) |
57 | | 1st2nd2 7205 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (𝐵 × 𝐵) → 𝑢 = 〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
58 | 57 | 3ad2ant2 1083 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑢 = 〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
59 | 58 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝐻‘𝑢) = (𝐻‘〈(1st ‘𝑢), (2nd ‘𝑢)〉)) |
60 | 58 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → ((Hom ‘𝐷)‘𝑢) = ((Hom ‘𝐷)‘〈(1st ‘𝑢), (2nd ‘𝑢)〉)) |
61 | 56, 59, 60 | 3eqtr4d 2666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝐻‘𝑢) = ((Hom ‘𝐷)‘𝑢)) |
62 | | eqidd 2623 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝑔(𝑢 ∙ 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓)) |
63 | 49, 61, 62 | mpt2eq123dv 6717 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) |
64 | 63 | mpt2eq3dva 6719 |
. . . . 5
⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)))) |
65 | | comfeq.4 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (Base‘𝐷)) |
66 | 65 | sqxpeqd 5141 |
. . . . . 6
⊢ (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐷) × (Base‘𝐷))) |
67 | | eqidd 2623 |
. . . . . 6
⊢ (𝜑 → (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) |
68 | 66, 65, 67 | mpt2eq123dv 6717 |
. . . . 5
⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)))) |
69 | 64, 68 | eqtrd 2656 |
. . . 4
⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)))) |
70 | | eqid 2622 |
. . . . 5
⊢
(compf‘𝐷) = (compf‘𝐷) |
71 | | eqid 2622 |
. . . . 5
⊢
(Base‘𝐷) =
(Base‘𝐷) |
72 | | comfeq.2 |
. . . . 5
⊢ ∙ =
(comp‘𝐷) |
73 | 70, 71, 40, 72 | comfffval 16358 |
. . . 4
⊢
(compf‘𝐷) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) |
74 | 69, 73 | syl6eqr 2674 |
. . 3
⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) = (compf‘𝐷)) |
75 | 39, 74 | eqeq12d 2637 |
. 2
⊢ (𝜑 → ((𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) ↔
(compf‘𝐶) = (compf‘𝐷))) |
76 | 29, 75 | syl5rbbr 275 |
1
⊢ (𝜑 →
((compf‘𝐶) = (compf‘𝐷) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |