Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  comfeq Structured version   Visualization version   GIF version

Theorem comfeq 16988
 Description: Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypotheses
Ref Expression
comfeq.1 · = (comp‘𝐶)
comfeq.2 = (comp‘𝐷)
comfeq.h 𝐻 = (Hom ‘𝐶)
comfeq.3 (𝜑𝐵 = (Base‘𝐶))
comfeq.4 (𝜑𝐵 = (Base‘𝐷))
comfeq.5 (𝜑 → (Homf𝐶) = (Homf𝐷))
Assertion
Ref Expression
comfeq (𝜑 → ((compf𝐶) = (compf𝐷) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦 𝑧)𝑓)))
Distinct variable groups:   𝑓,𝑔,𝑥,𝑦,𝑧,𝐵   𝐶,𝑓,𝑔,𝑧   𝜑,𝑓,𝑔,𝑧   · ,𝑓,𝑔,𝑥,𝑦   𝐷,𝑓,𝑔,𝑧   𝑓,𝐻,𝑔,𝑥,𝑦   ,𝑓,𝑔,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)   (𝑧)   · (𝑧)   𝐻(𝑧)

Proof of Theorem comfeq
Dummy variable 𝑢 is distinct from all other variables.
StepHypRef Expression
1 comfeq.3 . . . . . 6 (𝜑𝐵 = (Base‘𝐶))
21sqxpeqd 5555 . . . . 5 (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐶) × (Base‘𝐶)))
3 eqidd 2799 . . . . 5 (𝜑 → (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)))
42, 1, 3mpoeq123dv 7218 . . . 4 (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))))
5 eqid 2798 . . . . 5 (compf𝐶) = (compf𝐶)
6 eqid 2798 . . . . 5 (Base‘𝐶) = (Base‘𝐶)
7 comfeq.h . . . . 5 𝐻 = (Hom ‘𝐶)
8 comfeq.1 . . . . 5 · = (comp‘𝐶)
95, 6, 7, 8comfffval 16980 . . . 4 (compf𝐶) = (𝑢 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)))
104, 9eqtr4di 2851 . . 3 (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (compf𝐶))
11 eqid 2798 . . . . . . . 8 (Hom ‘𝐷) = (Hom ‘𝐷)
12 comfeq.5 . . . . . . . . 9 (𝜑 → (Homf𝐶) = (Homf𝐷))
13123ad2ant1 1130 . . . . . . . 8 ((𝜑𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧𝐵) → (Homf𝐶) = (Homf𝐷))
14 xp2nd 7717 . . . . . . . . . 10 (𝑢 ∈ (𝐵 × 𝐵) → (2nd𝑢) ∈ 𝐵)
15143ad2ant2 1131 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧𝐵) → (2nd𝑢) ∈ 𝐵)
1613ad2ant1 1130 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧𝐵) → 𝐵 = (Base‘𝐶))
1715, 16eleqtrd 2892 . . . . . . . 8 ((𝜑𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧𝐵) → (2nd𝑢) ∈ (Base‘𝐶))
18 simp3 1135 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧𝐵) → 𝑧𝐵)
1918, 16eleqtrd 2892 . . . . . . . 8 ((𝜑𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧𝐵) → 𝑧 ∈ (Base‘𝐶))
206, 7, 11, 13, 17, 19homfeqval 16979 . . . . . . 7 ((𝜑𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧𝐵) → ((2nd𝑢)𝐻𝑧) = ((2nd𝑢)(Hom ‘𝐷)𝑧))
21 xp1st 7716 . . . . . . . . . . . 12 (𝑢 ∈ (𝐵 × 𝐵) → (1st𝑢) ∈ 𝐵)
22213ad2ant2 1131 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧𝐵) → (1st𝑢) ∈ 𝐵)
2322, 16eleqtrd 2892 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧𝐵) → (1st𝑢) ∈ (Base‘𝐶))
246, 7, 11, 13, 23, 17homfeqval 16979 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧𝐵) → ((1st𝑢)𝐻(2nd𝑢)) = ((1st𝑢)(Hom ‘𝐷)(2nd𝑢)))
25 df-ov 7148 . . . . . . . . 9 ((1st𝑢)𝐻(2nd𝑢)) = (𝐻‘⟨(1st𝑢), (2nd𝑢)⟩)
26 df-ov 7148 . . . . . . . . 9 ((1st𝑢)(Hom ‘𝐷)(2nd𝑢)) = ((Hom ‘𝐷)‘⟨(1st𝑢), (2nd𝑢)⟩)
2724, 25, 263eqtr3g 2856 . . . . . . . 8 ((𝜑𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧𝐵) → (𝐻‘⟨(1st𝑢), (2nd𝑢)⟩) = ((Hom ‘𝐷)‘⟨(1st𝑢), (2nd𝑢)⟩))
28 1st2nd2 7723 . . . . . . . . . 10 (𝑢 ∈ (𝐵 × 𝐵) → 𝑢 = ⟨(1st𝑢), (2nd𝑢)⟩)
29283ad2ant2 1131 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧𝐵) → 𝑢 = ⟨(1st𝑢), (2nd𝑢)⟩)
3029fveq2d 6659 . . . . . . . 8 ((𝜑𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧𝐵) → (𝐻𝑢) = (𝐻‘⟨(1st𝑢), (2nd𝑢)⟩))
3129fveq2d 6659 . . . . . . . 8 ((𝜑𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧𝐵) → ((Hom ‘𝐷)‘𝑢) = ((Hom ‘𝐷)‘⟨(1st𝑢), (2nd𝑢)⟩))
3227, 30, 313eqtr4d 2843 . . . . . . 7 ((𝜑𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧𝐵) → (𝐻𝑢) = ((Hom ‘𝐷)‘𝑢))
33 eqidd 2799 . . . . . . 7 ((𝜑𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧𝐵) → (𝑔(𝑢 𝑧)𝑓) = (𝑔(𝑢 𝑧)𝑓))
3420, 32, 33mpoeq123dv 7218 . . . . . 6 ((𝜑𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧𝐵) → (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 𝑧)𝑓)) = (𝑔 ∈ ((2nd𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 𝑧)𝑓)))
3534mpoeq3dva 7220 . . . . 5 (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 𝑧)𝑓))))
36 comfeq.4 . . . . . . 7 (𝜑𝐵 = (Base‘𝐷))
3736sqxpeqd 5555 . . . . . 6 (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐷) × (Base‘𝐷)))
38 eqidd 2799 . . . . . 6 (𝜑 → (𝑔 ∈ ((2nd𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 𝑧)𝑓)) = (𝑔 ∈ ((2nd𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 𝑧)𝑓)))
3937, 36, 38mpoeq123dv 7218 . . . . 5 (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 𝑧)𝑓))) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ ((2nd𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 𝑧)𝑓))))
4035, 39eqtrd 2833 . . . 4 (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 𝑧)𝑓))) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ ((2nd𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 𝑧)𝑓))))
41 eqid 2798 . . . . 5 (compf𝐷) = (compf𝐷)
42 eqid 2798 . . . . 5 (Base‘𝐷) = (Base‘𝐷)
43 comfeq.2 . . . . 5 = (comp‘𝐷)
4441, 42, 11, 43comfffval 16980 . . . 4 (compf𝐷) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ ((2nd𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 𝑧)𝑓)))
4540, 44eqtr4di 2851 . . 3 (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 𝑧)𝑓))) = (compf𝐷))
4610, 45eqeq12d 2814 . 2 (𝜑 → ((𝑢 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 𝑧)𝑓))) ↔ (compf𝐶) = (compf𝐷)))
47 ovex 7178 . . . . . 6 ((2nd𝑢)𝐻𝑧) ∈ V
48 fvex 6668 . . . . . 6 (𝐻𝑢) ∈ V
4947, 48mpoex 7773 . . . . 5 (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) ∈ V
5049rgen2w 3119 . . . 4 𝑢 ∈ (𝐵 × 𝐵)∀𝑧𝐵 (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) ∈ V
51 mpo2eqb 7273 . . . 4 (∀𝑢 ∈ (𝐵 × 𝐵)∀𝑧𝐵 (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) ∈ V → ((𝑢 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 𝑧)𝑓))) ↔ ∀𝑢 ∈ (𝐵 × 𝐵)∀𝑧𝐵 (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 𝑧)𝑓))))
5250, 51ax-mp 5 . . 3 ((𝑢 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 𝑧)𝑓))) ↔ ∀𝑢 ∈ (𝐵 × 𝐵)∀𝑧𝐵 (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 𝑧)𝑓)))
53 vex 3445 . . . . . . . . 9 𝑥 ∈ V
54 vex 3445 . . . . . . . . 9 𝑦 ∈ V
5553, 54op2ndd 7695 . . . . . . . 8 (𝑢 = ⟨𝑥, 𝑦⟩ → (2nd𝑢) = 𝑦)
5655oveq1d 7160 . . . . . . 7 (𝑢 = ⟨𝑥, 𝑦⟩ → ((2nd𝑢)𝐻𝑧) = (𝑦𝐻𝑧))
57 fveq2 6655 . . . . . . . . 9 (𝑢 = ⟨𝑥, 𝑦⟩ → (𝐻𝑢) = (𝐻‘⟨𝑥, 𝑦⟩))
58 df-ov 7148 . . . . . . . . 9 (𝑥𝐻𝑦) = (𝐻‘⟨𝑥, 𝑦⟩)
5957, 58eqtr4di 2851 . . . . . . . 8 (𝑢 = ⟨𝑥, 𝑦⟩ → (𝐻𝑢) = (𝑥𝐻𝑦))
60 oveq1 7152 . . . . . . . . . 10 (𝑢 = ⟨𝑥, 𝑦⟩ → (𝑢 · 𝑧) = (⟨𝑥, 𝑦· 𝑧))
6160oveqd 7162 . . . . . . . . 9 (𝑢 = ⟨𝑥, 𝑦⟩ → (𝑔(𝑢 · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))
62 oveq1 7152 . . . . . . . . . 10 (𝑢 = ⟨𝑥, 𝑦⟩ → (𝑢 𝑧) = (⟨𝑥, 𝑦 𝑧))
6362oveqd 7162 . . . . . . . . 9 (𝑢 = ⟨𝑥, 𝑦⟩ → (𝑔(𝑢 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦 𝑧)𝑓))
6461, 63eqeq12d 2814 . . . . . . . 8 (𝑢 = ⟨𝑥, 𝑦⟩ → ((𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 𝑧)𝑓) ↔ (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦 𝑧)𝑓)))
6559, 64raleqbidv 3355 . . . . . . 7 (𝑢 = ⟨𝑥, 𝑦⟩ → (∀𝑓 ∈ (𝐻𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 𝑧)𝑓) ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦 𝑧)𝑓)))
6656, 65raleqbidv 3355 . . . . . 6 (𝑢 = ⟨𝑥, 𝑦⟩ → (∀𝑔 ∈ ((2nd𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 𝑧)𝑓) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)∀𝑓 ∈ (𝑥𝐻𝑦)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦 𝑧)𝑓)))
67 ovex 7178 . . . . . . . 8 (𝑔(𝑢 · 𝑧)𝑓) ∈ V
6867rgen2w 3119 . . . . . . 7 𝑔 ∈ ((2nd𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻𝑢)(𝑔(𝑢 · 𝑧)𝑓) ∈ V
69 mpo2eqb 7273 . . . . . . 7 (∀𝑔 ∈ ((2nd𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻𝑢)(𝑔(𝑢 · 𝑧)𝑓) ∈ V → ((𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 𝑧)𝑓)) ↔ ∀𝑔 ∈ ((2nd𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 𝑧)𝑓)))
7068, 69ax-mp 5 . . . . . 6 ((𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 𝑧)𝑓)) ↔ ∀𝑔 ∈ ((2nd𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 𝑧)𝑓))
71 ralcom 3308 . . . . . 6 (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦 𝑧)𝑓) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)∀𝑓 ∈ (𝑥𝐻𝑦)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦 𝑧)𝑓))
7266, 70, 713bitr4g 317 . . . . 5 (𝑢 = ⟨𝑥, 𝑦⟩ → ((𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 𝑧)𝑓)) ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦 𝑧)𝑓)))
7372ralbidv 3162 . . . 4 (𝑢 = ⟨𝑥, 𝑦⟩ → (∀𝑧𝐵 (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 𝑧)𝑓)) ↔ ∀𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦 𝑧)𝑓)))
7473ralxp 5680 . . 3 (∀𝑢 ∈ (𝐵 × 𝐵)∀𝑧𝐵 (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 𝑧)𝑓)) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦 𝑧)𝑓))
7552, 74bitri 278 . 2 ((𝑢 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑢)𝐻𝑧), 𝑓 ∈ (𝐻𝑢) ↦ (𝑔(𝑢 𝑧)𝑓))) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦 𝑧)𝑓))
7646, 75bitr3di 289 1 (𝜑 → ((compf𝐶) = (compf𝐷) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦 𝑧)𝑓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∀wral 3106  Vcvv 3442  ⟨cop 4534   × cxp 5521  ‘cfv 6332  (class class class)co 7145   ∈ cmpo 7147  1st c1st 7682  2nd c2nd 7683  Basecbs 16495  Hom chom 16588  compcco 16589  Homf chomf 16949  compfccomf 16950 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4805  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-id 5429  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-ov 7148  df-oprab 7149  df-mpo 7150  df-1st 7684  df-2nd 7685  df-homf 16953  df-comf 16954 This theorem is referenced by:  comfeqd  16989  2oppccomf  17007  oppccomfpropd  17009  resssetc  17364  resscatc  17377
 Copyright terms: Public domain W3C validator