Theorem comfeq 16189

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.

Step	Hyp	Ref	Expression
1		ovex 6577	. . . . . 6 ⊢ ((2nd ‘𝑢)𝐻𝑧) ∈ V
2		fvex 6113	. . . . . 6 ⊢ (𝐻‘𝑢) ∈ V
3	1, 2	mpt2ex 7136	. . . . 5 ⊢ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) ∈ V
4	3	rgen2w 2909	. . . 4 ⊢ ∀𝑢 ∈ (𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) ∈ V
5		mpt22eqb 6667	. . . 4 ⊢ (∀𝑢 ∈ (𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) ∈ V → ((𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) ↔ ∀𝑢 ∈ (𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))))
6	4, 5	ax-mp 5	. . 3 ⊢ ((𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) ↔ ∀𝑢 ∈ (𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)))
7		vex 3176	. . . . . . . . 9 ⊢ 𝑥 ∈ V
8		vex 3176	. . . . . . . . 9 ⊢ 𝑦 ∈ V
9	7, 8	op2ndd 7070	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (2nd ‘𝑢) = 𝑦)
10	9	oveq1d 6564	. . . . . . 7 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → ((2nd ‘𝑢)𝐻𝑧) = (𝑦𝐻𝑧))
11		fveq2 6103	. . . . . . . . 9 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (𝐻‘𝑢) = (𝐻‘⟨𝑥, 𝑦⟩))
12		df-ov 6552	. . . . . . . . 9 ⊢ (𝑥𝐻𝑦) = (𝐻‘⟨𝑥, 𝑦⟩)
13	11, 12	syl6eqr 2662	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (𝐻‘𝑢) = (𝑥𝐻𝑦))
14		oveq1 6556	. . . . . . . . . 10 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (𝑢 · 𝑧) = (⟨𝑥, 𝑦⟩ · 𝑧))
15	14	oveqd 6566	. . . . . . . . 9 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (𝑔(𝑢 · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓))
16		oveq1 6556	. . . . . . . . . 10 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (𝑢 ∙ 𝑧) = (⟨𝑥, 𝑦⟩ ∙ 𝑧))
17	16	oveqd 6566	. . . . . . . . 9 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (𝑔(𝑢 ∙ 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ ∙ 𝑧)𝑓))
18	15, 17	eqeq12d 2625	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → ((𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓) ↔ (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ ∙ 𝑧)𝑓)))
19	13, 18	raleqbidv 3129	. . . . . . 7 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓) ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ ∙ 𝑧)𝑓)))
20	10, 19	raleqbidv 3129	. . . . . 6 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (∀𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)∀𝑓 ∈ (𝑥𝐻𝑦)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ ∙ 𝑧)𝑓)))
21		ovex 6577	. . . . . . . 8 ⊢ (𝑔(𝑢 · 𝑧)𝑓) ∈ V
22	21	rgen2w 2909	. . . . . . 7 ⊢ ∀𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) ∈ V
23		mpt22eqb 6667	. . . . . . 7 ⊢ (∀𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) ∈ V → ((𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓)))
24	22, 23	ax-mp 5	. . . . . 6 ⊢ ((𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧)∀𝑓 ∈ (𝐻‘𝑢)(𝑔(𝑢 · 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓))
25		ralcom 3079	. . . . . 6 ⊢ (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ ∙ 𝑧)𝑓) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)∀𝑓 ∈ (𝑥𝐻𝑦)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ ∙ 𝑧)𝑓))
26	20, 24, 25	3bitr4g 302	. . . . 5 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → ((𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ ∙ 𝑧)𝑓)))
27	26	ralbidv 2969	. . . 4 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ ∙ 𝑧)𝑓)))
28	27	ralxp 5185	. . 3 ⊢ (∀𝑢 ∈ (𝐵 × 𝐵)∀𝑧 ∈ 𝐵 (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ ∙ 𝑧)𝑓))
29	6, 28	bitri 263	. 2 ⊢ ((𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ ∙ 𝑧)𝑓))
30		comfeq.3	. . . . . 6 ⊢ (𝜑 → 𝐵 = (Base‘𝐶))
31	30	sqxpeqd 5065	. . . . 5 ⊢ (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐶) × (Base‘𝐶)))
32		eqidd 2611	. . . . 5 ⊢ (𝜑 → (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)))
33	31, 30, 32	mpt2eq123dv 6615	. . . 4 ⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))))
34		eqid 2610	. . . . 5 ⊢ (compf‘𝐶) = (compf‘𝐶)
35		eqid 2610	. . . . 5 ⊢ (Base‘𝐶) = (Base‘𝐶)
36		comfeq.h	. . . . 5 ⊢ 𝐻 = (Hom ‘𝐶)
37		comfeq.1	. . . . 5 ⊢ · = (comp‘𝐶)
38	34, 35, 36, 37	comfffval 16181	. . . 4 ⊢ (compf‘𝐶) = (𝑢 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑧 ∈ (Base‘𝐶) ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓)))
39	33, 38	syl6eqr 2662	. . 3 ⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (compf‘𝐶))
40		eqid 2610	. . . . . . . 8 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
41		comfeq.5	. . . . . . . . 9 ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))
42	41	3ad2ant1 1075	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (Homf ‘𝐶) = (Homf ‘𝐷))
43		xp2nd 7090	. . . . . . . . . 10 ⊢ (𝑢 ∈ (𝐵 × 𝐵) → (2nd ‘𝑢) ∈ 𝐵)
44	43	3ad2ant2 1076	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (2nd ‘𝑢) ∈ 𝐵)
45	30	3ad2ant1 1075	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝐵 = (Base‘𝐶))
46	44, 45	eleqtrd 2690	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (2nd ‘𝑢) ∈ (Base‘𝐶))
47		simp3 1056	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵)
48	47, 45	eleqtrd 2690	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ (Base‘𝐶))
49	35, 36, 40, 42, 46, 48	homfeqval 16180	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → ((2nd ‘𝑢)𝐻𝑧) = ((2nd ‘𝑢)(Hom ‘𝐷)𝑧))
50		xp1st 7089	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (𝐵 × 𝐵) → (1st ‘𝑢) ∈ 𝐵)
51	50	3ad2ant2 1076	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (1st ‘𝑢) ∈ 𝐵)
52	51, 45	eleqtrd 2690	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (1st ‘𝑢) ∈ (Base‘𝐶))
53	35, 36, 40, 42, 52, 46	homfeqval 16180	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → ((1st ‘𝑢)𝐻(2nd ‘𝑢)) = ((1st ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑢)))
54		df-ov 6552	. . . . . . . . 9 ⊢ ((1st ‘𝑢)𝐻(2nd ‘𝑢)) = (𝐻‘⟨(1st ‘𝑢), (2nd ‘𝑢)⟩)
55		df-ov 6552	. . . . . . . . 9 ⊢ ((1st ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑢)) = ((Hom ‘𝐷)‘⟨(1st ‘𝑢), (2nd ‘𝑢)⟩)
56	53, 54, 55	3eqtr3g 2667	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝐻‘⟨(1st ‘𝑢), (2nd ‘𝑢)⟩) = ((Hom ‘𝐷)‘⟨(1st ‘𝑢), (2nd ‘𝑢)⟩))
57		1st2nd2 7096	. . . . . . . . . 10 ⊢ (𝑢 ∈ (𝐵 × 𝐵) → 𝑢 = ⟨(1st ‘𝑢), (2nd ‘𝑢)⟩)
58	57	3ad2ant2 1076	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑢 = ⟨(1st ‘𝑢), (2nd ‘𝑢)⟩)
59	58	fveq2d 6107	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝐻‘𝑢) = (𝐻‘⟨(1st ‘𝑢), (2nd ‘𝑢)⟩))
60	58	fveq2d 6107	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → ((Hom ‘𝐷)‘𝑢) = ((Hom ‘𝐷)‘⟨(1st ‘𝑢), (2nd ‘𝑢)⟩))
61	56, 59, 60	3eqtr4d 2654	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝐻‘𝑢) = ((Hom ‘𝐷)‘𝑢))
62		eqidd 2611	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝑔(𝑢 ∙ 𝑧)𝑓) = (𝑔(𝑢 ∙ 𝑧)𝑓))
63	49, 61, 62	mpt2eq123dv 6615	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐵 × 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)))
64	63	mpt2eq3dva 6617	. . . . 5 ⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))))
65		comfeq.4	. . . . . . 7 ⊢ (𝜑 → 𝐵 = (Base‘𝐷))
66	65	sqxpeqd 5065	. . . . . 6 ⊢ (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐷) × (Base‘𝐷)))
67		eqidd 2611	. . . . . 6 ⊢ (𝜑 → (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)) = (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)))
68	66, 65, 67	mpt2eq123dv 6615	. . . . 5 ⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))))
69	64, 68	eqtrd 2644	. . . 4 ⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))))
70		eqid 2610	. . . . 5 ⊢ (compf‘𝐷) = (compf‘𝐷)
71		eqid 2610	. . . . 5 ⊢ (Base‘𝐷) = (Base‘𝐷)
72		comfeq.2	. . . . 5 ⊢ ∙ = (comp‘𝐷)
73	70, 71, 40, 72	comfffval 16181	. . . 4 ⊢ (compf‘𝐷) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ ((2nd ‘𝑢)(Hom ‘𝐷)𝑧), 𝑓 ∈ ((Hom ‘𝐷)‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓)))
74	69, 73	syl6eqr 2662	. . 3 ⊢ (𝜑 → (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) = (compf‘𝐷))
75	39, 74	eqeq12d 2625	. 2 ⊢ (𝜑 → ((𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 · 𝑧)𝑓))) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑢)𝐻𝑧), 𝑓 ∈ (𝐻‘𝑢) ↦ (𝑔(𝑢 ∙ 𝑧)𝑓))) ↔ (compf‘𝐶) = (compf‘𝐷)))
76	29, 75	syl5rbbr 274	1 ⊢ (𝜑 → ((compf‘𝐶) = (compf‘𝐷) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩ ∙ 𝑧)𝑓)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  Vcvv 3173  ⟨cop 4131   × cxp 5036  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  1^st c1st 7057  2^nd c2nd 7058  Basecbs 15695  Hom chom 15779  compcco 15780  Hom_f chomf 16150  comp_fccomf 16151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-homf 16154  df-comf 16155

This theorem is referenced by:  comfeqd  16190  2oppccomf  16208  oppccomfpropd  16210  resssetc  16565  resscatc  16578