funcco

Description: A functor maps composition in the source category to composition in the target. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	funcco.b	$⊢ B = {Base}_{D}$
	funcco.h	$⊢ H = Hom (D)$
	funcco.o	$⊢ \underset{˙}{\cdot} = comp (D)$
	funcco.O	$⊢ O = comp (E)$
	funcco.f	$⊢ φ \to F (D Func E) G$
	funcco.x	$⊢ φ \to X \in B$
	funcco.y	$⊢ φ \to Y \in B$
	funcco.z	$⊢ φ \to Z \in B$
	funcco.m	$⊢ φ \to M \in (X H Y)$
	funcco.n	$⊢ φ \to N \in (Y H Z)$
Assertion	funcco	$⊢ φ \to (X G Z) (N (⟨X, Y⟩ \underset{˙}{\cdot} Z) M) = (Y G Z) (N) (⟨F (X), F (Y)⟩ O F (Z)) (X G Y) (M)$

Proof

Step	Hyp	Ref	Expression
1		funcco.b	$⊢ B = {Base}_{D}$
2		funcco.h	$⊢ H = Hom (D)$
3		funcco.o	$⊢ \underset{˙}{\cdot} = comp (D)$
4		funcco.O	$⊢ O = comp (E)$
5		funcco.f	$⊢ φ \to F (D Func E) G$
6		funcco.x	$⊢ φ \to X \in B$
7		funcco.y	$⊢ φ \to Y \in B$
8		funcco.z	$⊢ φ \to Z \in B$
9		funcco.m	$⊢ φ \to M \in (X H Y)$
10		funcco.n	$⊢ φ \to N \in (Y H Z)$
11		eqid	$⊢ {Base}_{E} = {Base}_{E}$
12		eqid	$⊢ Hom (E) = Hom (E)$
13		eqid	$⊢ Id (D) = Id (D)$
14		eqid	$⊢ Id (E) = Id (E)$
15		df-br	$⊢ F (D Func E) G \leftrightarrow ⟨F, G⟩ \in (D Func E)$
16	5 15	sylib	$⊢ φ \to ⟨F, G⟩ \in (D Func E)$
17		funcrcl	$⊢ ⟨F, G⟩ \in (D Func E) \to (D \in Cat \land E \in Cat)$
18	16 17	syl	$⊢ φ \to (D \in Cat \land E \in Cat)$
19	18	simpld	$⊢ φ \to D \in Cat$
20	18	simprd	$⊢ φ \to E \in Cat$
21	1 11 2 12 13 14 3 4 19 20	isfunc	$⊢ φ \to (F (D Func E) G \leftrightarrow (F : B ⟶ {Base}_{E} \land G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) Hom (E) F (2^{nd} (z)))}^{H (z)}) \land \forall x \in B ((x G x) (Id (D) (x)) = Id (E) (F (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m))))$
22	5 21	mpbid	$⊢ φ \to (F : B ⟶ {Base}_{E} \land G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) Hom (E) F (2^{nd} (z)))}^{H (z)}) \land \forall x \in B ((x G x) (Id (D) (x)) = Id (E) (F (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m)))$
23	22	simp3d	$⊢ φ \to \forall x \in B ((x G x) (Id (D) (x)) = Id (E) (F (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m))$
24	7	adantr	$⊢ (φ \land x = X) \to Y \in B$
25	8	ad2antrr	$⊢ ((φ \land x = X) \land y = Y) \to Z \in B$
26	9	ad3antrrr	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to M \in (X H Y)$
27		simpllr	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to x = X$
28		simplr	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to y = Y$
29	27 28	oveq12d	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to x H y = X H Y$
30	26 29	eleqtrrd	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to M \in (x H y)$
31	10	ad4antr	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \to N \in (Y H Z)$
32		simpllr	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \to y = Y$
33		simplr	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \to z = Z$
34	32 33	oveq12d	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \to y H z = Y H Z$
35	31 34	eleqtrrd	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \to N \in (y H z)$
36		simp-5r	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to x = X$
37		simpllr	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to z = Z$
38	36 37	oveq12d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to x G z = X G Z$
39		simp-4r	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to y = Y$
40	36 39	opeq12d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to ⟨x, y⟩ = ⟨X, Y⟩$
41	40 37	oveq12d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to ⟨x, y⟩ \underset{˙}{\cdot} z = ⟨X, Y⟩ \underset{˙}{\cdot} Z$
42		simpr	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to n = N$
43		simplr	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to m = M$
44	41 42 43	oveq123d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to n (⟨x, y⟩ \underset{˙}{\cdot} z) m = N (⟨X, Y⟩ \underset{˙}{\cdot} Z) M$
45	38 44	fveq12d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (X G Z) (N (⟨X, Y⟩ \underset{˙}{\cdot} Z) M)$
46	36	fveq2d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to F (x) = F (X)$
47	39	fveq2d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to F (y) = F (Y)$
48	46 47	opeq12d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to ⟨F (x), F (y)⟩ = ⟨F (X), F (Y)⟩$
49	37	fveq2d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to F (z) = F (Z)$
50	48 49	oveq12d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to ⟨F (x), F (y)⟩ O F (z) = ⟨F (X), F (Y)⟩ O F (Z)$
51	39 37	oveq12d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to y G z = Y G Z$
52	51 42	fveq12d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to (y G z) (n) = (Y G Z) (N)$
53	36 39	oveq12d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to x G y = X G Y$
54	53 43	fveq12d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to (x G y) (m) = (X G Y) (M)$
55	50 52 54	oveq123d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m) = (Y G Z) (N) (⟨F (X), F (Y)⟩ O F (Z)) (X G Y) (M)$
56	45 55	eqeq12d	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \land n = N) \to ((x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m) \leftrightarrow (X G Z) (N (⟨X, Y⟩ \underset{˙}{\cdot} Z) M) = (Y G Z) (N) (⟨F (X), F (Y)⟩ O F (Z)) (X G Y) (M))$
57	35 56	rspcdv	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land m = M) \to (\forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m) \to (X G Z) (N (⟨X, Y⟩ \underset{˙}{\cdot} Z) M) = (Y G Z) (N) (⟨F (X), F (Y)⟩ O F (Z)) (X G Y) (M))$
58	30 57	rspcimdv	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to (\forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m) \to (X G Z) (N (⟨X, Y⟩ \underset{˙}{\cdot} Z) M) = (Y G Z) (N) (⟨F (X), F (Y)⟩ O F (Z)) (X G Y) (M))$
59	25 58	rspcimdv	$⊢ ((φ \land x = X) \land y = Y) \to (\forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m) \to (X G Z) (N (⟨X, Y⟩ \underset{˙}{\cdot} Z) M) = (Y G Z) (N) (⟨F (X), F (Y)⟩ O F (Z)) (X G Y) (M))$
60	24 59	rspcimdv	$⊢ (φ \land x = X) \to (\forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m) \to (X G Z) (N (⟨X, Y⟩ \underset{˙}{\cdot} Z) M) = (Y G Z) (N) (⟨F (X), F (Y)⟩ O F (Z)) (X G Y) (M))$
61	60	adantld	$⊢ (φ \land x = X) \to (((x G x) (Id (D) (x)) = Id (E) (F (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m)) \to (X G Z) (N (⟨X, Y⟩ \underset{˙}{\cdot} Z) M) = (Y G Z) (N) (⟨F (X), F (Y)⟩ O F (Z)) (X G Y) (M))$
62	6 61	rspcimdv	$⊢ φ \to (\forall x \in B ((x G x) (Id (D) (x)) = Id (E) (F (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m)) \to (X G Z) (N (⟨X, Y⟩ \underset{˙}{\cdot} Z) M) = (Y G Z) (N) (⟨F (X), F (Y)⟩ O F (Z)) (X G Y) (M))$
63	23 62	mpd	$⊢ φ \to (X G Z) (N (⟨X, Y⟩ \underset{˙}{\cdot} Z) M) = (Y G Z) (N) (⟨F (X), F (Y)⟩ O F (Z)) (X G Y) (M)$

Metamath Proof Explorer

Theorem funcco

Proof