nati

Description: Naturality property of a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	natrcl.1	$⊢ N = C Nat D$
	natixp.2	$⊢ φ \to A \in (⟨F, G⟩ N ⟨K, L⟩)$
	natixp.b	$⊢ B = {Base}_{C}$
	nati.h	$⊢ H = Hom (C)$
	nati.o	$⊢ \underset{˙}{\cdot} = comp (D)$
	nati.x	$⊢ φ \to X \in B$
	nati.y	$⊢ φ \to Y \in B$
	nati.r	$⊢ φ \to R \in (X H Y)$
Assertion	nati	$⊢ φ \to A (Y) (⟨F (X), F (Y)⟩ \underset{˙}{\cdot} K (Y)) (X G Y) (R) = (X L Y) (R) (⟨F (X), K (X)⟩ \underset{˙}{\cdot} K (Y)) A (X)$

Proof

Step	Hyp	Ref	Expression
1		natrcl.1	$⊢ N = C Nat D$
2		natixp.2	$⊢ φ \to A \in (⟨F, G⟩ N ⟨K, L⟩)$
3		natixp.b	$⊢ B = {Base}_{C}$
4		nati.h	$⊢ H = Hom (C)$
5		nati.o	$⊢ \underset{˙}{\cdot} = comp (D)$
6		nati.x	$⊢ φ \to X \in B$
7		nati.y	$⊢ φ \to Y \in B$
8		nati.r	$⊢ φ \to R \in (X H Y)$
9		eqid	$⊢ Hom (D) = Hom (D)$
10	1	natrcl	$⊢ A \in (⟨F, G⟩ N ⟨K, L⟩) \to (⟨F, G⟩ \in (C Func D) \land ⟨K, L⟩ \in (C Func D))$
11	2 10	syl	$⊢ φ \to (⟨F, G⟩ \in (C Func D) \land ⟨K, L⟩ \in (C Func D))$
12	11	simpld	$⊢ φ \to ⟨F, G⟩ \in (C Func D)$
13		df-br	$⊢ F (C Func D) G \leftrightarrow ⟨F, G⟩ \in (C Func D)$
14	12 13	sylibr	$⊢ φ \to F (C Func D) G$
15	11	simprd	$⊢ φ \to ⟨K, L⟩ \in (C Func D)$
16		df-br	$⊢ K (C Func D) L \leftrightarrow ⟨K, L⟩ \in (C Func D)$
17	15 16	sylibr	$⊢ φ \to K (C Func D) L$
18	1 3 4 9 5 14 17	isnat	$⊢ φ \to (A \in (⟨F, G⟩ N ⟨K, L⟩) \leftrightarrow (A \in \underset{x \in B}{⨉} (F (x) Hom (D) K (x)) \land \forall x \in B \forall y \in B \forall f \in (x H y) A (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (f) = (x L y) (f) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) A (x)))$
19	2 18	mpbid	$⊢ φ \to (A \in \underset{x \in B}{⨉} (F (x) Hom (D) K (x)) \land \forall x \in B \forall y \in B \forall f \in (x H y) A (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (f) = (x L y) (f) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) A (x))$
20	19	simprd	$⊢ φ \to \forall x \in B \forall y \in B \forall f \in (x H y) A (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (f) = (x L y) (f) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) A (x)$
21	7	adantr	$⊢ (φ \land x = X) \to Y \in B$
22	8	ad2antrr	$⊢ ((φ \land x = X) \land y = Y) \to R \in (X H Y)$
23		simplr	$⊢ ((φ \land x = X) \land y = Y) \to x = X$
24		simpr	$⊢ ((φ \land x = X) \land y = Y) \to y = Y$
25	23 24	oveq12d	$⊢ ((φ \land x = X) \land y = Y) \to x H y = X H Y$
26	22 25	eleqtrrd	$⊢ ((φ \land x = X) \land y = Y) \to R \in (x H y)$
27		simpllr	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to x = X$
28	27	fveq2d	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to F (x) = F (X)$
29		simplr	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to y = Y$
30	29	fveq2d	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to F (y) = F (Y)$
31	28 30	opeq12d	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to ⟨F (x), F (y)⟩ = ⟨F (X), F (Y)⟩$
32	29	fveq2d	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to K (y) = K (Y)$
33	31 32	oveq12d	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to ⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y) = ⟨F (X), F (Y)⟩ \underset{˙}{\cdot} K (Y)$
34	29	fveq2d	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to A (y) = A (Y)$
35	27 29	oveq12d	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to x G y = X G Y$
36		simpr	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to f = R$
37	35 36	fveq12d	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to (x G y) (f) = (X G Y) (R)$
38	33 34 37	oveq123d	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to A (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (f) = A (Y) (⟨F (X), F (Y)⟩ \underset{˙}{\cdot} K (Y)) (X G Y) (R)$
39	27	fveq2d	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to K (x) = K (X)$
40	28 39	opeq12d	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to ⟨F (x), K (x)⟩ = ⟨F (X), K (X)⟩$
41	40 32	oveq12d	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to ⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y) = ⟨F (X), K (X)⟩ \underset{˙}{\cdot} K (Y)$
42	27 29	oveq12d	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to x L y = X L Y$
43	42 36	fveq12d	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to (x L y) (f) = (X L Y) (R)$
44	27	fveq2d	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to A (x) = A (X)$
45	41 43 44	oveq123d	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to (x L y) (f) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) A (x) = (X L Y) (R) (⟨F (X), K (X)⟩ \underset{˙}{\cdot} K (Y)) A (X)$
46	38 45	eqeq12d	$⊢ (((φ \land x = X) \land y = Y) \land f = R) \to (A (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (f) = (x L y) (f) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) A (x) \leftrightarrow A (Y) (⟨F (X), F (Y)⟩ \underset{˙}{\cdot} K (Y)) (X G Y) (R) = (X L Y) (R) (⟨F (X), K (X)⟩ \underset{˙}{\cdot} K (Y)) A (X))$
47	26 46	rspcdv	$⊢ ((φ \land x = X) \land y = Y) \to (\forall f \in (x H y) A (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (f) = (x L y) (f) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) A (x) \to A (Y) (⟨F (X), F (Y)⟩ \underset{˙}{\cdot} K (Y)) (X G Y) (R) = (X L Y) (R) (⟨F (X), K (X)⟩ \underset{˙}{\cdot} K (Y)) A (X))$
48	21 47	rspcimdv	$⊢ (φ \land x = X) \to (\forall y \in B \forall f \in (x H y) A (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (f) = (x L y) (f) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) A (x) \to A (Y) (⟨F (X), F (Y)⟩ \underset{˙}{\cdot} K (Y)) (X G Y) (R) = (X L Y) (R) (⟨F (X), K (X)⟩ \underset{˙}{\cdot} K (Y)) A (X))$
49	6 48	rspcimdv	$⊢ φ \to (\forall x \in B \forall y \in B \forall f \in (x H y) A (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (f) = (x L y) (f) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) A (x) \to A (Y) (⟨F (X), F (Y)⟩ \underset{˙}{\cdot} K (Y)) (X G Y) (R) = (X L Y) (R) (⟨F (X), K (X)⟩ \underset{˙}{\cdot} K (Y)) A (X))$
50	20 49	mpd	$⊢ φ \to A (Y) (⟨F (X), F (Y)⟩ \underset{˙}{\cdot} K (Y)) (X G Y) (R) = (X L Y) (R) (⟨F (X), K (X)⟩ \underset{˙}{\cdot} K (Y)) A (X)$

Metamath Proof Explorer

Theorem nati

Proof