fucco

Description: Value of the composition of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	fucco.q	$⊢ Q = C FuncCat D$
	fucco.n	$⊢ N = C Nat D$
	fucco.a	$⊢ A = {Base}_{C}$
	fucco.o	$⊢ \underset{˙}{\cdot} = comp (D)$
	fucco.x	$⊢ \underset{˙}{∙} = comp (Q)$
	fucco.f	$⊢ φ \to R \in (F N G)$
	fucco.g	$⊢ φ \to S \in (G N H)$
Assertion	fucco	$⊢ φ \to S (⟨F, G⟩ \underset{˙}{∙} H) R = (x \in A ⟼ S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) R (x))$

Proof

Step	Hyp	Ref	Expression
1		fucco.q	$⊢ Q = C FuncCat D$
2		fucco.n	$⊢ N = C Nat D$
3		fucco.a	$⊢ A = {Base}_{C}$
4		fucco.o	$⊢ \underset{˙}{\cdot} = comp (D)$
5		fucco.x	$⊢ \underset{˙}{∙} = comp (Q)$
6		fucco.f	$⊢ φ \to R \in (F N G)$
7		fucco.g	$⊢ φ \to S \in (G N H)$
8		eqid	$⊢ C Func D = C Func D$
9	2	natrcl	$⊢ R \in (F N G) \to (F \in (C Func D) \land G \in (C Func D))$
10	6 9	syl	$⊢ φ \to (F \in (C Func D) \land G \in (C Func D))$
11	10	simpld	$⊢ φ \to F \in (C Func D)$
12		funcrcl	$⊢ F \in (C Func D) \to (C \in Cat \land D \in Cat)$
13	11 12	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
14	13	simpld	$⊢ φ \to C \in Cat$
15	13	simprd	$⊢ φ \to D \in Cat$
16	1 8 2 3 4 14 15 5	fuccofval	$⊢ φ \to \underset{˙}{∙} = (v \in ((C Func D) \times (C Func D)), h \in (C Func D) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))))$
17		fvexd	$⊢ (φ \land (v = ⟨F, G⟩ \land h = H)) \to 1^{st} (v) \in V$
18		simprl	$⊢ (φ \land (v = ⟨F, G⟩ \land h = H)) \to v = ⟨F, G⟩$
19	18	fveq2d	$⊢ (φ \land (v = ⟨F, G⟩ \land h = H)) \to 1^{st} (v) = 1^{st} (⟨F, G⟩)$
20		op1stg	$⊢ (F \in (C Func D) \land G \in (C Func D)) \to 1^{st} (⟨F, G⟩) = F$
21	10 20	syl	$⊢ φ \to 1^{st} (⟨F, G⟩) = F$
22	21	adantr	$⊢ (φ \land (v = ⟨F, G⟩ \land h = H)) \to 1^{st} (⟨F, G⟩) = F$
23	19 22	eqtrd	$⊢ (φ \land (v = ⟨F, G⟩ \land h = H)) \to 1^{st} (v) = F$
24		fvexd	$⊢ ((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \to 2^{nd} (v) \in V$
25	18	adantr	$⊢ ((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \to v = ⟨F, G⟩$
26	25	fveq2d	$⊢ ((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \to 2^{nd} (v) = 2^{nd} (⟨F, G⟩)$
27		op2ndg	$⊢ (F \in (C Func D) \land G \in (C Func D)) \to 2^{nd} (⟨F, G⟩) = G$
28	10 27	syl	$⊢ φ \to 2^{nd} (⟨F, G⟩) = G$
29	28	ad2antrr	$⊢ ((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \to 2^{nd} (⟨F, G⟩) = G$
30	26 29	eqtrd	$⊢ ((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \to 2^{nd} (v) = G$
31		simpr	$⊢ (((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \land g = G) \to g = G$
32		simprr	$⊢ (φ \land (v = ⟨F, G⟩ \land h = H)) \to h = H$
33	32	ad2antrr	$⊢ (((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \land g = G) \to h = H$
34	31 33	oveq12d	$⊢ (((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \land g = G) \to g N h = G N H$
35		simplr	$⊢ (((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \land g = G) \to f = F$
36	35 31	oveq12d	$⊢ (((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \land g = G) \to f N g = F N G$
37	35	fveq2d	$⊢ (((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \land g = G) \to 1^{st} (f) = 1^{st} (F)$
38	37	fveq1d	$⊢ (((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \land g = G) \to 1^{st} (f) (x) = 1^{st} (F) (x)$
39	31	fveq2d	$⊢ (((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \land g = G) \to 1^{st} (g) = 1^{st} (G)$
40	39	fveq1d	$⊢ (((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \land g = G) \to 1^{st} (g) (x) = 1^{st} (G) (x)$
41	38 40	opeq12d	$⊢ (((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \land g = G) \to ⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ = ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩$
42	33	fveq2d	$⊢ (((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \land g = G) \to 1^{st} (h) = 1^{st} (H)$
43	42	fveq1d	$⊢ (((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \land g = G) \to 1^{st} (h) (x) = 1^{st} (H) (x)$
44	41 43	oveq12d	$⊢ (((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \land g = G) \to ⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x) = ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)$
45	44	oveqd	$⊢ (((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \land g = G) \to b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x) = b (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) a (x)$
46	45	mpteq2dv	$⊢ (((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \land g = G) \to (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x)) = (x \in A ⟼ b (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) a (x))$
47	34 36 46	mpoeq123dv	$⊢ (((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \land g = G) \to (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))) = (b \in (G N H), a \in (F N G) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) a (x)))$
48	24 30 47	csbied2	$⊢ ((φ \land (v = ⟨F, G⟩ \land h = H)) \land f = F) \to ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))) = (b \in (G N H), a \in (F N G) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) a (x)))$
49	17 23 48	csbied2	$⊢ (φ \land (v = ⟨F, G⟩ \land h = H)) \to ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))) = (b \in (G N H), a \in (F N G) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) a (x)))$
50		opelxpi	$⊢ (F \in (C Func D) \land G \in (C Func D)) \to ⟨F, G⟩ \in ((C Func D) \times (C Func D))$
51	10 50	syl	$⊢ φ \to ⟨F, G⟩ \in ((C Func D) \times (C Func D))$
52	2	natrcl	$⊢ S \in (G N H) \to (G \in (C Func D) \land H \in (C Func D))$
53	7 52	syl	$⊢ φ \to (G \in (C Func D) \land H \in (C Func D))$
54	53	simprd	$⊢ φ \to H \in (C Func D)$
55		ovex	$⊢ G N H \in V$
56		ovex	$⊢ F N G \in V$
57	55 56	mpoex	$⊢ (b \in (G N H), a \in (F N G) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) a (x))) \in V$
58	57	a1i	$⊢ φ \to (b \in (G N H), a \in (F N G) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) a (x))) \in V$
59	16 49 51 54 58	ovmpod	$⊢ φ \to ⟨F, G⟩ \underset{˙}{∙} H = (b \in (G N H), a \in (F N G) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) a (x)))$
60		simprl	$⊢ (φ \land (b = S \land a = R)) \to b = S$
61	60	fveq1d	$⊢ (φ \land (b = S \land a = R)) \to b (x) = S (x)$
62		simprr	$⊢ (φ \land (b = S \land a = R)) \to a = R$
63	62	fveq1d	$⊢ (φ \land (b = S \land a = R)) \to a (x) = R (x)$
64	61 63	oveq12d	$⊢ (φ \land (b = S \land a = R)) \to b (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) a (x) = S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) R (x)$
65	64	mpteq2dv	$⊢ (φ \land (b = S \land a = R)) \to (x \in A ⟼ b (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) a (x)) = (x \in A ⟼ S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) R (x))$
66	3	fvexi	$⊢ A \in V$
67	66	mptex	$⊢ (x \in A ⟼ S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) R (x)) \in V$
68	67	a1i	$⊢ φ \to (x \in A ⟼ S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) R (x)) \in V$
69	59 65 7 6 68	ovmpod	$⊢ φ \to S (⟨F, G⟩ \underset{˙}{∙} H) R = (x \in A ⟼ S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (H) (x)) R (x))$

Metamath Proof Explorer

Theorem fucco

Proof