Step | Hyp | Ref
| Expression |
1 | | comfeq.3 |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) |
2 | 1 | sqxpeqd 5583 |
. . . . 5
⊢ (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐶) × (Base‘𝐶))) |
3 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) |
4 | 2, 1, 3 | mpoeq123dv 7286 |
. . . 4
⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)))) |
5 | | eqid 2737 |
. . . . 5
⊢
(compf‘𝐶) = (compf‘𝐶) |
6 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝐶) =
(Base‘𝐶) |
7 | | comfeq.h |
. . . . 5
⊢ 𝐻 = (Hom ‘𝐶) |
8 | | comfeq.1 |
. . . . 5
⊢ · =
(comp‘𝐶) |
9 | 5, 6, 7, 8 | comfffval 17201 |
. . . 4
⊢
(compf‘𝐶) = (𝑢 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) |
10 | 4, 9 | eqtr4di 2796 |
. . 3
⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (compf‘𝐶)) |
11 | | eqid 2737 |
. . . . . . . 8
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
12 | | comfeq.5 |
. . . . . . . . 9
⊢ (𝜑 → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
13 | 12 | 3ad2ant1 1135 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
14 | | xp2nd 7794 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (𝐵 × 𝐵) → (2nd ‘𝑢) ∈ 𝐵) |
15 | 14 | 3ad2ant2 1136 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (2nd ‘𝑢) ∈ 𝐵) |
16 | 1 | 3ad2ant1 1135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝐵 = (Base‘𝐶)) |
17 | 15, 16 | eleqtrd 2840 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (2nd ‘𝑢) ∈ (Base‘𝐶)) |
18 | | simp3 1140 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵) |
19 | 18, 16 | eleqtrd 2840 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ (Base‘𝐶)) |
20 | 6, 7, 11, 13, 17, 19 | homfeqval 17200 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → ((2nd ‘𝑢)𝐻𝑧) = ((2nd ‘𝑢)(Hom ‘𝐷)𝑧)) |
21 | | xp1st 7793 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (𝐵 × 𝐵) → (1st ‘𝑢) ∈ 𝐵) |
22 | 21 | 3ad2ant2 1136 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (1st ‘𝑢) ∈ 𝐵) |
23 | 22, 16 | eleqtrd 2840 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (1st ‘𝑢) ∈ (Base‘𝐶)) |
24 | 6, 7, 11, 13, 23, 17 | homfeqval 17200 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → ((1st ‘𝑢)𝐻(2nd ‘𝑢)) = ((1st ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑢))) |
25 | | df-ov 7216 |
. . . . . . . . 9
⊢
((1st ‘𝑢)𝐻(2nd ‘𝑢)) = (𝐻‘〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
26 | | df-ov 7216 |
. . . . . . . . 9
⊢
((1st ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑢)) = ((Hom ‘𝐷)‘〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
27 | 24, 25, 26 | 3eqtr3g 2801 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝐻‘〈(1st ‘𝑢), (2nd ‘𝑢)〉) = ((Hom ‘𝐷)‘〈(1st
‘𝑢), (2nd
‘𝑢)〉)) |
28 | | 1st2nd2 7800 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (𝐵 × 𝐵) → 𝑢 = 〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
29 | 28 | 3ad2ant2 1136 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑢 = 〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
30 | 29 | fveq2d 6721 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝐻‘𝑢) = (𝐻‘〈(1st ‘𝑢), (2nd ‘𝑢)〉)) |
31 | 29 | fveq2d 6721 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → ((Hom ‘𝐷)‘𝑢) = ((Hom ‘𝐷)‘〈(1st ‘𝑢), (2nd ‘𝑢)〉)) |
32 | 27, 30, 31 | 3eqtr4d 2787 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝐻‘𝑢) = ((Hom ‘𝐷)‘𝑢)) |
33 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝑔(𝑢 ∙ 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓)) |
34 | 20, 32, 33 | mpoeq123dv 7286 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) |
35 | 34 | mpoeq3dva 7288 |
. . . . 5
⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)))) |
36 | | comfeq.4 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (Base‘𝐷)) |
37 | 36 | sqxpeqd 5583 |
. . . . . 6
⊢ (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐷) × (Base‘𝐷))) |
38 | | eqidd 2738 |
. . . . . 6
⊢ (𝜑 → (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) |
39 | 37, 36, 38 | mpoeq123dv 7286 |
. . . . 5
⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)))) |
40 | 35, 39 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)))) |
41 | | eqid 2737 |
. . . . 5
⊢
(compf‘𝐷) = (compf‘𝐷) |
42 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝐷) =
(Base‘𝐷) |
43 | | comfeq.2 |
. . . . 5
⊢ ∙ =
(comp‘𝐷) |
44 | 41, 42, 11, 43 | comfffval 17201 |
. . . 4
⊢
(compf‘𝐷) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) |
45 | 40, 44 | eqtr4di 2796 |
. . 3
⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) = (compf‘𝐷)) |
46 | 10, 45 | eqeq12d 2753 |
. 2
⊢ (𝜑 → ((𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) ↔
(compf‘𝐶) = (compf‘𝐷))) |
47 | | ovex 7246 |
. . . . . 6
⊢
((2nd ‘𝑢)𝐻𝑧) ∈ V |
48 | | fvex 6730 |
. . . . . 6
⊢ (𝐻‘𝑢) ∈ V |
49 | 47, 48 | mpoex 7850 |
. . . . 5
⊢ (𝑔 ∈ ((2nd
‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) ∈ V |
50 | 49 | rgen2w 3074 |
. . . 4
⊢
∀𝑢 ∈
(𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) ∈ V |
51 | | mpo2eqb 7342 |
. . . 4
⊢
(∀𝑢 ∈
(𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) ∈ V → ((𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) ↔ ∀𝑢 ∈ (𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)))) |
52 | 50, 51 | ax-mp 5 |
. . 3
⊢ ((𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) ↔ ∀𝑢 ∈ (𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) |
53 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
54 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
55 | 53, 54 | op2ndd 7772 |
. . . . . . . 8
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (2nd ‘𝑢) = 𝑦) |
56 | 55 | oveq1d 7228 |
. . . . . . 7
⊢ (𝑢 = 〈𝑥, 𝑦〉 → ((2nd ‘𝑢)𝐻𝑧) = (𝑦𝐻𝑧)) |
57 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝐻‘𝑢) = (𝐻‘〈𝑥, 𝑦〉)) |
58 | | df-ov 7216 |
. . . . . . . . 9
⊢ (𝑥𝐻𝑦) = (𝐻‘〈𝑥, 𝑦〉) |
59 | 57, 58 | eqtr4di 2796 |
. . . . . . . 8
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝐻‘𝑢) = (𝑥𝐻𝑦)) |
60 | | oveq1 7220 |
. . . . . . . . . 10
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝑢 · 𝑧) = (〈𝑥, 𝑦〉 · 𝑧)) |
61 | 60 | oveqd 7230 |
. . . . . . . . 9
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝑔(𝑢 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) |
62 | | oveq1 7220 |
. . . . . . . . . 10
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝑢 ∙ 𝑧) = (〈𝑥, 𝑦〉 ∙ 𝑧)) |
63 | 62 | oveqd 7230 |
. . . . . . . . 9
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝑔(𝑢 ∙ 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓)) |
64 | 61, 63 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑢 = 〈𝑥, 𝑦〉 → ((𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓) ↔ (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |
65 | 59, 64 | raleqbidv 3313 |
. . . . . . 7
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓) ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |
66 | 56, 65 | raleqbidv 3313 |
. . . . . 6
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (∀𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)∀𝑓 ∈ (𝑥𝐻𝑦)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |
67 | | ovex 7246 |
. . . . . . . 8
⊢ (𝑔(𝑢 · 𝑧)𝑓) ∈ V |
68 | 67 | rgen2w 3074 |
. . . . . . 7
⊢
∀𝑔 ∈
((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) ∈ V |
69 | | mpo2eqb 7342 |
. . . . . . 7
⊢
(∀𝑔 ∈
((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) ∈ V → ((𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓))) |
70 | 68, 69 | ax-mp 5 |
. . . . . 6
⊢ ((𝑔 ∈ ((2nd
‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓)) |
71 | | ralcom 3267 |
. . . . . 6
⊢
(∀𝑓 ∈
(𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)∀𝑓 ∈ (𝑥𝐻𝑦)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓)) |
72 | 66, 70, 71 | 3bitr4g 317 |
. . . . 5
⊢ (𝑢 = 〈𝑥, 𝑦〉 → ((𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |
73 | 72 | ralbidv 3118 |
. . . 4
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |
74 | 73 | ralxp 5710 |
. . 3
⊢
(∀𝑢 ∈
(𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓)) |
75 | 52, 74 | bitri 278 |
. 2
⊢ ((𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓)) |
76 | 46, 75 | bitr3di 289 |
1
⊢ (𝜑 →
((compf‘𝐶) = (compf‘𝐷) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |