comfeq

Description: Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	comfeq.1	$⊢ \underset{˙}{\cdot} = comp (C)$
	comfeq.2	$⊢ \underset{˙}{∙} = comp (D)$
	comfeq.h	$⊢ H = Hom (C)$
	comfeq.3	$⊢ φ \to B = {Base}_{C}$
	comfeq.4	$⊢ φ \to B = {Base}_{D}$
	comfeq.5	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
Assertion	comfeq	$⊢ φ \to ({comp}_{𝑓} (C) = {comp}_{𝑓} (D) \leftrightarrow \forall x \in B \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f = g (⟨x, y⟩ \underset{˙}{∙} z) f)$

Proof

Step	Hyp	Ref	Expression
1		comfeq.1	$⊢ \underset{˙}{\cdot} = comp (C)$
2		comfeq.2	$⊢ \underset{˙}{∙} = comp (D)$
3		comfeq.h	$⊢ H = Hom (C)$
4		comfeq.3	$⊢ φ \to B = {Base}_{C}$
5		comfeq.4	$⊢ φ \to B = {Base}_{D}$
6		comfeq.5	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
7	4	sqxpeqd	$⊢ φ \to B \times B = {Base}_{C} \times {Base}_{C}$
8		eqidd	$⊢ φ \to (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f) = (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f)$
9	7 4 8	mpoeq123dv	$⊢ φ \to (u \in (B \times B), z \in B ⟼ (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f)) = (u \in ({Base}_{C} \times {Base}_{C}), z \in {Base}_{C} ⟼ (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f))$
10		eqid	$⊢ {comp}_{𝑓} (C) = {comp}_{𝑓} (C)$
11		eqid	$⊢ {Base}_{C} = {Base}_{C}$
12	10 11 3 1	comfffval	$⊢ {comp}_{𝑓} (C) = (u \in ({Base}_{C} \times {Base}_{C}), z \in {Base}_{C} ⟼ (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f))$
13	9 12	eqtr4di	$⊢ φ \to (u \in (B \times B), z \in B ⟼ (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f)) = {comp}_{𝑓} (C)$
14		eqid	$⊢ Hom (D) = Hom (D)$
15	6	3ad2ant1	$⊢ (φ \land u \in (B \times B) \land z \in B) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
16		xp2nd	$⊢ u \in (B \times B) \to 2^{nd} (u) \in B$
17	16	3ad2ant2	$⊢ (φ \land u \in (B \times B) \land z \in B) \to 2^{nd} (u) \in B$
18	4	3ad2ant1	$⊢ (φ \land u \in (B \times B) \land z \in B) \to B = {Base}_{C}$
19	17 18	eleqtrd	$⊢ (φ \land u \in (B \times B) \land z \in B) \to 2^{nd} (u) \in {Base}_{C}$
20		simp3	$⊢ (φ \land u \in (B \times B) \land z \in B) \to z \in B$
21	20 18	eleqtrd	$⊢ (φ \land u \in (B \times B) \land z \in B) \to z \in {Base}_{C}$
22	11 3 14 15 19 21	homfeqval	$⊢ (φ \land u \in (B \times B) \land z \in B) \to 2^{nd} (u) H z = 2^{nd} (u) Hom (D) z$
23		xp1st	$⊢ u \in (B \times B) \to 1^{st} (u) \in B$
24	23	3ad2ant2	$⊢ (φ \land u \in (B \times B) \land z \in B) \to 1^{st} (u) \in B$
25	24 18	eleqtrd	$⊢ (φ \land u \in (B \times B) \land z \in B) \to 1^{st} (u) \in {Base}_{C}$
26	11 3 14 15 25 19	homfeqval	$⊢ (φ \land u \in (B \times B) \land z \in B) \to 1^{st} (u) H 2^{nd} (u) = 1^{st} (u) Hom (D) 2^{nd} (u)$
27		df-ov	$⊢ 1^{st} (u) H 2^{nd} (u) = H (⟨1^{st} (u), 2^{nd} (u)⟩)$
28		df-ov	$⊢ 1^{st} (u) Hom (D) 2^{nd} (u) = Hom (D) (⟨1^{st} (u), 2^{nd} (u)⟩)$
29	26 27 28	3eqtr3g	$⊢ (φ \land u \in (B \times B) \land z \in B) \to H (⟨1^{st} (u), 2^{nd} (u)⟩) = Hom (D) (⟨1^{st} (u), 2^{nd} (u)⟩)$
30		1st2nd2	$⊢ u \in (B \times B) \to u = ⟨1^{st} (u), 2^{nd} (u)⟩$
31	30	3ad2ant2	$⊢ (φ \land u \in (B \times B) \land z \in B) \to u = ⟨1^{st} (u), 2^{nd} (u)⟩$
32	31	fveq2d	$⊢ (φ \land u \in (B \times B) \land z \in B) \to H (u) = H (⟨1^{st} (u), 2^{nd} (u)⟩)$
33	31	fveq2d	$⊢ (φ \land u \in (B \times B) \land z \in B) \to Hom (D) (u) = Hom (D) (⟨1^{st} (u), 2^{nd} (u)⟩)$
34	29 32 33	3eqtr4d	$⊢ (φ \land u \in (B \times B) \land z \in B) \to H (u) = Hom (D) (u)$
35		eqidd	$⊢ (φ \land u \in (B \times B) \land z \in B) \to g (u \underset{˙}{∙} z) f = g (u \underset{˙}{∙} z) f$
36	22 34 35	mpoeq123dv	$⊢ (φ \land u \in (B \times B) \land z \in B) \to (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{∙} z) f) = (g \in (2^{nd} (u) Hom (D) z), f \in Hom (D) (u) ⟼ g (u \underset{˙}{∙} z) f)$
37	36	mpoeq3dva	$⊢ φ \to (u \in (B \times B), z \in B ⟼ (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{∙} z) f)) = (u \in (B \times B), z \in B ⟼ (g \in (2^{nd} (u) Hom (D) z), f \in Hom (D) (u) ⟼ g (u \underset{˙}{∙} z) f))$
38	5	sqxpeqd	$⊢ φ \to B \times B = {Base}_{D} \times {Base}_{D}$
39		eqidd	$⊢ φ \to (g \in (2^{nd} (u) Hom (D) z), f \in Hom (D) (u) ⟼ g (u \underset{˙}{∙} z) f) = (g \in (2^{nd} (u) Hom (D) z), f \in Hom (D) (u) ⟼ g (u \underset{˙}{∙} z) f)$
40	38 5 39	mpoeq123dv	$⊢ φ \to (u \in (B \times B), z \in B ⟼ (g \in (2^{nd} (u) Hom (D) z), f \in Hom (D) (u) ⟼ g (u \underset{˙}{∙} z) f)) = (u \in ({Base}_{D} \times {Base}_{D}), z \in {Base}_{D} ⟼ (g \in (2^{nd} (u) Hom (D) z), f \in Hom (D) (u) ⟼ g (u \underset{˙}{∙} z) f))$
41	37 40	eqtrd	$⊢ φ \to (u \in (B \times B), z \in B ⟼ (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{∙} z) f)) = (u \in ({Base}_{D} \times {Base}_{D}), z \in {Base}_{D} ⟼ (g \in (2^{nd} (u) Hom (D) z), f \in Hom (D) (u) ⟼ g (u \underset{˙}{∙} z) f))$
42		eqid	$⊢ {comp}_{𝑓} (D) = {comp}_{𝑓} (D)$
43		eqid	$⊢ {Base}_{D} = {Base}_{D}$
44	42 43 14 2	comfffval	$⊢ {comp}_{𝑓} (D) = (u \in ({Base}_{D} \times {Base}_{D}), z \in {Base}_{D} ⟼ (g \in (2^{nd} (u) Hom (D) z), f \in Hom (D) (u) ⟼ g (u \underset{˙}{∙} z) f))$
45	41 44	eqtr4di	$⊢ φ \to (u \in (B \times B), z \in B ⟼ (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{∙} z) f)) = {comp}_{𝑓} (D)$
46	13 45	eqeq12d	$⊢ φ \to ((u \in (B \times B), z \in B ⟼ (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f)) = (u \in (B \times B), z \in B ⟼ (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{∙} z) f)) \leftrightarrow {comp}_{𝑓} (C) = {comp}_{𝑓} (D))$
47		ovex	$⊢ 2^{nd} (u) H z \in V$
48		fvex	$⊢ H (u) \in V$
49	47 48	mpoex	$⊢ (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f) \in V$
50	49	rgen2w	$⊢ \forall u \in (B \times B) \forall z \in B (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f) \in V$
51		mpo2eqb	$⊢ \forall u \in (B \times B) \forall z \in B (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f) \in V \to ((u \in (B \times B), z \in B ⟼ (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f)) = (u \in (B \times B), z \in B ⟼ (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{∙} z) f)) \leftrightarrow \forall u \in (B \times B) \forall z \in B (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f) = (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{∙} z) f))$
52	50 51	ax-mp	$⊢ (u \in (B \times B), z \in B ⟼ (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f)) = (u \in (B \times B), z \in B ⟼ (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{∙} z) f)) \leftrightarrow \forall u \in (B \times B) \forall z \in B (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f) = (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{∙} z) f)$
53		vex	$⊢ x \in V$
54		vex	$⊢ y \in V$
55	53 54	op2ndd	$⊢ u = ⟨x, y⟩ \to 2^{nd} (u) = y$
56	55	oveq1d	$⊢ u = ⟨x, y⟩ \to 2^{nd} (u) H z = y H z$
57		fveq2	$⊢ u = ⟨x, y⟩ \to H (u) = H (⟨x, y⟩)$
58		df-ov	$⊢ x H y = H (⟨x, y⟩)$
59	57 58	eqtr4di	$⊢ u = ⟨x, y⟩ \to H (u) = x H y$
60		oveq1	$⊢ u = ⟨x, y⟩ \to u \underset{˙}{\cdot} z = ⟨x, y⟩ \underset{˙}{\cdot} z$
61	60	oveqd	$⊢ u = ⟨x, y⟩ \to g (u \underset{˙}{\cdot} z) f = g (⟨x, y⟩ \underset{˙}{\cdot} z) f$
62		oveq1	$⊢ u = ⟨x, y⟩ \to u \underset{˙}{∙} z = ⟨x, y⟩ \underset{˙}{∙} z$
63	62	oveqd	$⊢ u = ⟨x, y⟩ \to g (u \underset{˙}{∙} z) f = g (⟨x, y⟩ \underset{˙}{∙} z) f$
64	61 63	eqeq12d	$⊢ u = ⟨x, y⟩ \to (g (u \underset{˙}{\cdot} z) f = g (u \underset{˙}{∙} z) f \leftrightarrow g (⟨x, y⟩ \underset{˙}{\cdot} z) f = g (⟨x, y⟩ \underset{˙}{∙} z) f)$
65	59 64	raleqbidv	$⊢ u = ⟨x, y⟩ \to (\forall f \in H (u) g (u \underset{˙}{\cdot} z) f = g (u \underset{˙}{∙} z) f \leftrightarrow \forall f \in (x H y) g (⟨x, y⟩ \underset{˙}{\cdot} z) f = g (⟨x, y⟩ \underset{˙}{∙} z) f)$
66	56 65	raleqbidv	$⊢ u = ⟨x, y⟩ \to (\forall g \in (2^{nd} (u) H z) \forall f \in H (u) g (u \underset{˙}{\cdot} z) f = g (u \underset{˙}{∙} z) f \leftrightarrow \forall g \in (y H z) \forall f \in (x H y) g (⟨x, y⟩ \underset{˙}{\cdot} z) f = g (⟨x, y⟩ \underset{˙}{∙} z) f)$
67		ovex	$⊢ g (u \underset{˙}{\cdot} z) f \in V$
68	67	rgen2w	$⊢ \forall g \in (2^{nd} (u) H z) \forall f \in H (u) g (u \underset{˙}{\cdot} z) f \in V$
69		mpo2eqb	$⊢ \forall g \in (2^{nd} (u) H z) \forall f \in H (u) g (u \underset{˙}{\cdot} z) f \in V \to ((g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f) = (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{∙} z) f) \leftrightarrow \forall g \in (2^{nd} (u) H z) \forall f \in H (u) g (u \underset{˙}{\cdot} z) f = g (u \underset{˙}{∙} z) f)$
70	68 69	ax-mp	$⊢ (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f) = (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{∙} z) f) \leftrightarrow \forall g \in (2^{nd} (u) H z) \forall f \in H (u) g (u \underset{˙}{\cdot} z) f = g (u \underset{˙}{∙} z) f$
71		ralcom	$⊢ \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f = g (⟨x, y⟩ \underset{˙}{∙} z) f \leftrightarrow \forall g \in (y H z) \forall f \in (x H y) g (⟨x, y⟩ \underset{˙}{\cdot} z) f = g (⟨x, y⟩ \underset{˙}{∙} z) f$
72	66 70 71	3bitr4g	$⊢ u = ⟨x, y⟩ \to ((g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f) = (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{∙} z) f) \leftrightarrow \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f = g (⟨x, y⟩ \underset{˙}{∙} z) f)$
73	72	ralbidv	$⊢ u = ⟨x, y⟩ \to (\forall z \in B (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f) = (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{∙} z) f) \leftrightarrow \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f = g (⟨x, y⟩ \underset{˙}{∙} z) f)$
74	73	ralxp	$⊢ \forall u \in (B \times B) \forall z \in B (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f) = (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{∙} z) f) \leftrightarrow \forall x \in B \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f = g (⟨x, y⟩ \underset{˙}{∙} z) f$
75	52 74	bitri	$⊢ (u \in (B \times B), z \in B ⟼ (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{\cdot} z) f)) = (u \in (B \times B), z \in B ⟼ (g \in (2^{nd} (u) H z), f \in H (u) ⟼ g (u \underset{˙}{∙} z) f)) \leftrightarrow \forall x \in B \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f = g (⟨x, y⟩ \underset{˙}{∙} z) f$
76	46 75	bitr3di	$⊢ φ \to ({comp}_{𝑓} (C) = {comp}_{𝑓} (D) \leftrightarrow \forall x \in B \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f = g (⟨x, y⟩ \underset{˙}{∙} z) f)$

Metamath Proof Explorer

Theorem comfeq

Proof