| Step | Hyp | Ref
| Expression |
| 1 | | comfeq.3 |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) |
| 2 | 1 | sqxpeqd 5717 |
. . . . 5
⊢ (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐶) × (Base‘𝐶))) |
| 3 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) |
| 4 | 2, 1, 3 | mpoeq123dv 7508 |
. . . 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 17741 |
. . . 4
⊢
(compf‘𝐶) = (𝑢 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) |
| 10 | 4, 9 | eqtr4di 2795 |
. . 3
⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (compf‘𝐶)) |
| 11 | | eqid 2737 |
. . . . . . . 8
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
| 12 | | comfeq.5 |
. . . . . . . . 9
⊢ (𝜑 → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
| 13 | 12 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
| 14 | | xp2nd 8047 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (𝐵 × 𝐵) → (2nd ‘𝑢) ∈ 𝐵) |
| 15 | 14 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (2nd ‘𝑢) ∈ 𝐵) |
| 16 | 1 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝐵 = (Base‘𝐶)) |
| 17 | 15, 16 | eleqtrd 2843 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (2nd ‘𝑢) ∈ (Base‘𝐶)) |
| 18 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵) |
| 19 | 18, 16 | eleqtrd 2843 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ (Base‘𝐶)) |
| 20 | 6, 7, 11, 13, 17, 19 | homfeqval 17740 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → ((2nd ‘𝑢)𝐻𝑧) = ((2nd ‘𝑢)(Hom ‘𝐷)𝑧)) |
| 21 | | xp1st 8046 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (𝐵 × 𝐵) → (1st ‘𝑢) ∈ 𝐵) |
| 22 | 21 | 3ad2ant2 1135 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (1st ‘𝑢) ∈ 𝐵) |
| 23 | 22, 16 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (1st ‘𝑢) ∈ (Base‘𝐶)) |
| 24 | 6, 7, 11, 13, 23, 17 | homfeqval 17740 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → ((1st ‘𝑢)𝐻(2nd ‘𝑢)) = ((1st ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑢))) |
| 25 | | df-ov 7434 |
. . . . . . . . 9
⊢
((1st ‘𝑢)𝐻(2nd ‘𝑢)) = (𝐻‘〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
| 26 | | df-ov 7434 |
. . . . . . . . 9
⊢
((1st ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑢)) = ((Hom ‘𝐷)‘〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
| 27 | 24, 25, 26 | 3eqtr3g 2800 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝐻‘〈(1st ‘𝑢), (2nd ‘𝑢)〉) = ((Hom ‘𝐷)‘〈(1st
‘𝑢), (2nd
‘𝑢)〉)) |
| 28 | | 1st2nd2 8053 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (𝐵 × 𝐵) → 𝑢 = 〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
| 29 | 28 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑢 = 〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
| 30 | 29 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝐻‘𝑢) = (𝐻‘〈(1st ‘𝑢), (2nd ‘𝑢)〉)) |
| 31 | 29 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → ((Hom ‘𝐷)‘𝑢) = ((Hom ‘𝐷)‘〈(1st ‘𝑢), (2nd ‘𝑢)〉)) |
| 32 | 27, 30, 31 | 3eqtr4d 2787 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝐻‘𝑢) = ((Hom ‘𝐷)‘𝑢)) |
| 33 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝑔(𝑢 ∙ 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓)) |
| 34 | 20, 32, 33 | mpoeq123dv 7508 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) |
| 35 | 34 | mpoeq3dva 7510 |
. . . . 5
⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)))) |
| 36 | | comfeq.4 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (Base‘𝐷)) |
| 37 | 36 | sqxpeqd 5717 |
. . . . . 6
⊢ (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐷) × (Base‘𝐷))) |
| 38 | | eqidd 2738 |
. . . . . 6
⊢ (𝜑 → (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) |
| 39 | 37, 36, 38 | mpoeq123dv 7508 |
. . . . 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 17741 |
. . . 4
⊢
(compf‘𝐷) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) |
| 45 | 40, 44 | eqtr4di 2795 |
. . 3
⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) = (compf‘𝐷)) |
| 46 | 10, 45 | eqeq12d 2753 |
. 2
⊢ (𝜑 → ((𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) ↔
(compf‘𝐶) = (compf‘𝐷))) |
| 47 | | ovex 7464 |
. . . . . 6
⊢
((2nd ‘𝑢)𝐻𝑧) ∈ V |
| 48 | | fvex 6919 |
. . . . . 6
⊢ (𝐻‘𝑢) ∈ V |
| 49 | 47, 48 | mpoex 8104 |
. . . . 5
⊢ (𝑔 ∈ ((2nd
‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) ∈ V |
| 50 | 49 | rgen2w 3066 |
. . . 4
⊢
∀𝑢 ∈
(𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) ∈ V |
| 51 | | mpo2eqb 7565 |
. . . 4
⊢
(∀𝑢 ∈
(𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) ∈ V → ((𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) ↔ ∀𝑢 ∈ (𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)))) |
| 52 | 50, 51 | ax-mp 5 |
. . 3
⊢ ((𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) ↔ ∀𝑢 ∈ (𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) |
| 53 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
| 54 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
| 55 | 53, 54 | op2ndd 8025 |
. . . . . . . 8
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (2nd ‘𝑢) = 𝑦) |
| 56 | 55 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑢 = 〈𝑥, 𝑦〉 → ((2nd ‘𝑢)𝐻𝑧) = (𝑦𝐻𝑧)) |
| 57 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝐻‘𝑢) = (𝐻‘〈𝑥, 𝑦〉)) |
| 58 | | df-ov 7434 |
. . . . . . . . 9
⊢ (𝑥𝐻𝑦) = (𝐻‘〈𝑥, 𝑦〉) |
| 59 | 57, 58 | eqtr4di 2795 |
. . . . . . . 8
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝐻‘𝑢) = (𝑥𝐻𝑦)) |
| 60 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝑢 · 𝑧) = (〈𝑥, 𝑦〉 · 𝑧)) |
| 61 | 60 | oveqd 7448 |
. . . . . . . . 9
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝑔(𝑢 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) |
| 62 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝑢 ∙ 𝑧) = (〈𝑥, 𝑦〉 ∙ 𝑧)) |
| 63 | 62 | oveqd 7448 |
. . . . . . . . 9
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝑔(𝑢 ∙ 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓)) |
| 64 | 61, 63 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑢 = 〈𝑥, 𝑦〉 → ((𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓) ↔ (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |
| 65 | 59, 64 | raleqbidv 3346 |
. . . . . . 7
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓) ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |
| 66 | 56, 65 | raleqbidv 3346 |
. . . . . 6
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (∀𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)∀𝑓 ∈ (𝑥𝐻𝑦)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |
| 67 | | ovex 7464 |
. . . . . . . 8
⊢ (𝑔(𝑢 · 𝑧)𝑓) ∈ V |
| 68 | 67 | rgen2w 3066 |
. . . . . . 7
⊢
∀𝑔 ∈
((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) ∈ V |
| 69 | | mpo2eqb 7565 |
. . . . . . 7
⊢
(∀𝑔 ∈
((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) ∈ V → ((𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓))) |
| 70 | 68, 69 | ax-mp 5 |
. . . . . 6
⊢ ((𝑔 ∈ ((2nd
‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓)) |
| 71 | | ralcom 3289 |
. . . . . 6
⊢
(∀𝑓 ∈
(𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)∀𝑓 ∈ (𝑥𝐻𝑦)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓)) |
| 72 | 66, 70, 71 | 3bitr4g 314 |
. . . . 5
⊢ (𝑢 = 〈𝑥, 𝑦〉 → ((𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |
| 73 | 72 | ralbidv 3178 |
. . . 4
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |
| 74 | 73 | ralxp 5852 |
. . 3
⊢
(∀𝑢 ∈
(𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓)) |
| 75 | 52, 74 | bitri 275 |
. 2
⊢ ((𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓)) |
| 76 | 46, 75 | bitr3di 286 |
1
⊢ (𝜑 →
((compf‘𝐶) = (compf‘𝐷) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) |