1st2ndprf

Description: Break a functor into a product category into first and second projections. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	1st2ndprf.t	$⊢ T = D \times_{c} E$
	1st2ndprf.f	$⊢ φ \to F \in (C Func T)$
	1st2ndprf.d	$⊢ φ \to D \in Cat$
	1st2ndprf.e	$⊢ φ \to E \in Cat$
Assertion	1st2ndprf	$⊢ φ \to F = ((D {1^{st}}_{F} E) \circ_{func} F) {⟨,⟩}_{F} ((D {2^{nd}}_{F} E) \circ_{func} F)$

Proof

Step	Hyp	Ref	Expression
1		1st2ndprf.t	$⊢ T = D \times_{c} E$
2		1st2ndprf.f	$⊢ φ \to F \in (C Func T)$
3		1st2ndprf.d	$⊢ φ \to D \in Cat$
4		1st2ndprf.e	$⊢ φ \to E \in Cat$
5		eqid	$⊢ {Base}_{C} = {Base}_{C}$
6		eqid	$⊢ {Base}_{D} = {Base}_{D}$
7		eqid	$⊢ {Base}_{E} = {Base}_{E}$
8	1 6 7	xpcbas	$⊢ {Base}_{D} \times {Base}_{E} = {Base}_{T}$
9		relfunc	$⊢ Rel (C Func T)$
10		1st2ndbr	$⊢ (Rel (C Func T) \land F \in (C Func T)) \to 1^{st} (F) (C Func T) 2^{nd} (F)$
11	9 2 10	sylancr	$⊢ φ \to 1^{st} (F) (C Func T) 2^{nd} (F)$
12	5 8 11	funcf1	$⊢ φ \to 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D} \times {Base}_{E}$
13	12	feqmptd	$⊢ φ \to 1^{st} (F) = (x \in {Base}_{C} ⟼ 1^{st} (F) (x))$
14	12	ffvelrnda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (F) (x) \in ({Base}_{D} \times {Base}_{E})$
15		1st2nd2	$⊢ 1^{st} (F) (x) \in ({Base}_{D} \times {Base}_{E}) \to 1^{st} (F) (x) = ⟨1^{st} (1^{st} (F) (x)), 2^{nd} (1^{st} (F) (x))⟩$
16	14 15	syl	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (F) (x) = ⟨1^{st} (1^{st} (F) (x)), 2^{nd} (1^{st} (F) (x))⟩$
17	2	adantr	$⊢ (φ \land x \in {Base}_{C}) \to F \in (C Func T)$
18		eqid	$⊢ D {1^{st}}_{F} E = D {1^{st}}_{F} E$
19	1 3 4 18	1stfcl	$⊢ φ \to D {1^{st}}_{F} E \in (T Func D)$
20	19	adantr	$⊢ (φ \land x \in {Base}_{C}) \to D {1^{st}}_{F} E \in (T Func D)$
21		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
22	5 17 20 21	cofu1	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} ((D {1^{st}}_{F} E) \circ_{func} F) (x) = 1^{st} (D {1^{st}}_{F} E) (1^{st} (F) (x))$
23		eqid	$⊢ Hom (T) = Hom (T)$
24	3	adantr	$⊢ (φ \land x \in {Base}_{C}) \to D \in Cat$
25	4	adantr	$⊢ (φ \land x \in {Base}_{C}) \to E \in Cat$
26	1 8 23 24 25 18 14	1stf1	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (D {1^{st}}_{F} E) (1^{st} (F) (x)) = 1^{st} (1^{st} (F) (x))$
27	22 26	eqtrd	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} ((D {1^{st}}_{F} E) \circ_{func} F) (x) = 1^{st} (1^{st} (F) (x))$
28		eqid	$⊢ D {2^{nd}}_{F} E = D {2^{nd}}_{F} E$
29	1 3 4 28	2ndfcl	$⊢ φ \to D {2^{nd}}_{F} E \in (T Func E)$
30	29	adantr	$⊢ (φ \land x \in {Base}_{C}) \to D {2^{nd}}_{F} E \in (T Func E)$
31	5 17 30 21	cofu1	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} ((D {2^{nd}}_{F} E) \circ_{func} F) (x) = 1^{st} (D {2^{nd}}_{F} E) (1^{st} (F) (x))$
32	1 8 23 24 25 28 14	2ndf1	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (D {2^{nd}}_{F} E) (1^{st} (F) (x)) = 2^{nd} (1^{st} (F) (x))$
33	31 32	eqtrd	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} ((D {2^{nd}}_{F} E) \circ_{func} F) (x) = 2^{nd} (1^{st} (F) (x))$
34	27 33	opeq12d	$⊢ (φ \land x \in {Base}_{C}) \to ⟨1^{st} ((D {1^{st}}_{F} E) \circ_{func} F) (x), 1^{st} ((D {2^{nd}}_{F} E) \circ_{func} F) (x)⟩ = ⟨1^{st} (1^{st} (F) (x)), 2^{nd} (1^{st} (F) (x))⟩$
35	16 34	eqtr4d	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (F) (x) = ⟨1^{st} ((D {1^{st}}_{F} E) \circ_{func} F) (x), 1^{st} ((D {2^{nd}}_{F} E) \circ_{func} F) (x)⟩$
36	35	mpteq2dva	$⊢ φ \to (x \in {Base}_{C} ⟼ 1^{st} (F) (x)) = (x \in {Base}_{C} ⟼ ⟨1^{st} ((D {1^{st}}_{F} E) \circ_{func} F) (x), 1^{st} ((D {2^{nd}}_{F} E) \circ_{func} F) (x)⟩)$
37	13 36	eqtrd	$⊢ φ \to 1^{st} (F) = (x \in {Base}_{C} ⟼ ⟨1^{st} ((D {1^{st}}_{F} E) \circ_{func} F) (x), 1^{st} ((D {2^{nd}}_{F} E) \circ_{func} F) (x)⟩)$
38	5 11	funcfn2	$⊢ φ \to 2^{nd} (F) Fn ({Base}_{C} \times {Base}_{C})$
39		fnov	$⊢ 2^{nd} (F) Fn ({Base}_{C} \times {Base}_{C}) \leftrightarrow 2^{nd} (F) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (F) y)$
40	38 39	sylib	$⊢ φ \to 2^{nd} (F) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (F) y)$
41		eqid	$⊢ Hom (C) = Hom (C)$
42	11	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (F) (C Func T) 2^{nd} (F)$
43		simprl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x \in {Base}_{C}$
44		simprr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to y \in {Base}_{C}$
45	5 41 23 42 43 44	funcf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (F) y) : x Hom (C) y ⟶ 1^{st} (F) (x) Hom (T) 1^{st} (F) (y)$
46	45	feqmptd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x 2^{nd} (F) y = (f \in (x Hom (C) y) ⟼ (x 2^{nd} (F) y) (f))$
47	1 23	relxpchom	$⊢ Rel (1^{st} (F) (x) Hom (T) 1^{st} (F) (y))$
48	45	ffvelrnda	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (x 2^{nd} (F) y) (f) \in (1^{st} (F) (x) Hom (T) 1^{st} (F) (y))$
49		1st2nd	$⊢ (Rel (1^{st} (F) (x) Hom (T) 1^{st} (F) (y)) \land (x 2^{nd} (F) y) (f) \in (1^{st} (F) (x) Hom (T) 1^{st} (F) (y))) \to (x 2^{nd} (F) y) (f) = ⟨1^{st} ((x 2^{nd} (F) y) (f)), 2^{nd} ((x 2^{nd} (F) y) (f))⟩$
50	47 48 49	sylancr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (x 2^{nd} (F) y) (f) = ⟨1^{st} ((x 2^{nd} (F) y) (f)), 2^{nd} ((x 2^{nd} (F) y) (f))⟩$
51	2	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to F \in (C Func T)$
52	19	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to D {1^{st}}_{F} E \in (T Func D)$
53	43	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to x \in {Base}_{C}$
54	44	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to y \in {Base}_{C}$
55		simpr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to f \in (x Hom (C) y)$
56	5 51 52 53 54 41 55	cofu2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (x 2^{nd} ((D {1^{st}}_{F} E) \circ_{func} F) y) (f) = (1^{st} (F) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (F) (y)) ((x 2^{nd} (F) y) (f))$
57	3	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to D \in Cat$
58	4	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to E \in Cat$
59	14	adantrr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (F) (x) \in ({Base}_{D} \times {Base}_{E})$
60	12	ffvelrnda	$⊢ (φ \land y \in {Base}_{C}) \to 1^{st} (F) (y) \in ({Base}_{D} \times {Base}_{E})$
61	60	adantrl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (F) (y) \in ({Base}_{D} \times {Base}_{E})$
62	1 8 23 57 58 18 59 61	1stf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (F) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (F) (y) = {1^{st} ↾}_{(1^{st} (F) (x) Hom (T) 1^{st} (F) (y))}$
63	62	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to 1^{st} (F) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (F) (y) = {1^{st} ↾}_{(1^{st} (F) (x) Hom (T) 1^{st} (F) (y))}$
64	63	fveq1d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (1^{st} (F) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (F) (y)) ((x 2^{nd} (F) y) (f)) = ({1^{st} ↾}_{(1^{st} (F) (x) Hom (T) 1^{st} (F) (y))}) ((x 2^{nd} (F) y) (f))$
65	48	fvresd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to ({1^{st} ↾}_{(1^{st} (F) (x) Hom (T) 1^{st} (F) (y))}) ((x 2^{nd} (F) y) (f)) = 1^{st} ((x 2^{nd} (F) y) (f))$
66	56 64 65	3eqtrd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (x 2^{nd} ((D {1^{st}}_{F} E) \circ_{func} F) y) (f) = 1^{st} ((x 2^{nd} (F) y) (f))$
67	29	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to D {2^{nd}}_{F} E \in (T Func E)$
68	5 51 67 53 54 41 55	cofu2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (x 2^{nd} ((D {2^{nd}}_{F} E) \circ_{func} F) y) (f) = (1^{st} (F) (x) 2^{nd} (D {2^{nd}}_{F} E) 1^{st} (F) (y)) ((x 2^{nd} (F) y) (f))$
69	1 8 23 57 58 28 59 61	2ndf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (F) (x) 2^{nd} (D {2^{nd}}_{F} E) 1^{st} (F) (y) = {2^{nd} ↾}_{(1^{st} (F) (x) Hom (T) 1^{st} (F) (y))}$
70	69	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to 1^{st} (F) (x) 2^{nd} (D {2^{nd}}_{F} E) 1^{st} (F) (y) = {2^{nd} ↾}_{(1^{st} (F) (x) Hom (T) 1^{st} (F) (y))}$
71	70	fveq1d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (1^{st} (F) (x) 2^{nd} (D {2^{nd}}_{F} E) 1^{st} (F) (y)) ((x 2^{nd} (F) y) (f)) = ({2^{nd} ↾}_{(1^{st} (F) (x) Hom (T) 1^{st} (F) (y))}) ((x 2^{nd} (F) y) (f))$
72	48	fvresd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to ({2^{nd} ↾}_{(1^{st} (F) (x) Hom (T) 1^{st} (F) (y))}) ((x 2^{nd} (F) y) (f)) = 2^{nd} ((x 2^{nd} (F) y) (f))$
73	68 71 72	3eqtrd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (x 2^{nd} ((D {2^{nd}}_{F} E) \circ_{func} F) y) (f) = 2^{nd} ((x 2^{nd} (F) y) (f))$
74	66 73	opeq12d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to ⟨(x 2^{nd} ((D {1^{st}}_{F} E) \circ_{func} F) y) (f), (x 2^{nd} ((D {2^{nd}}_{F} E) \circ_{func} F) y) (f)⟩ = ⟨1^{st} ((x 2^{nd} (F) y) (f)), 2^{nd} ((x 2^{nd} (F) y) (f))⟩$
75	50 74	eqtr4d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (x 2^{nd} (F) y) (f) = ⟨(x 2^{nd} ((D {1^{st}}_{F} E) \circ_{func} F) y) (f), (x 2^{nd} ((D {2^{nd}}_{F} E) \circ_{func} F) y) (f)⟩$
76	75	mpteq2dva	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (f \in (x Hom (C) y) ⟼ (x 2^{nd} (F) y) (f)) = (f \in (x Hom (C) y) ⟼ ⟨(x 2^{nd} ((D {1^{st}}_{F} E) \circ_{func} F) y) (f), (x 2^{nd} ((D {2^{nd}}_{F} E) \circ_{func} F) y) (f)⟩)$
77	46 76	eqtrd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x 2^{nd} (F) y = (f \in (x Hom (C) y) ⟼ ⟨(x 2^{nd} ((D {1^{st}}_{F} E) \circ_{func} F) y) (f), (x 2^{nd} ((D {2^{nd}}_{F} E) \circ_{func} F) y) (f)⟩)$
78	77	3impb	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to x 2^{nd} (F) y = (f \in (x Hom (C) y) ⟼ ⟨(x 2^{nd} ((D {1^{st}}_{F} E) \circ_{func} F) y) (f), (x 2^{nd} ((D {2^{nd}}_{F} E) \circ_{func} F) y) (f)⟩)$
79	78	mpoeq3dva	$⊢ φ \to (x \in {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (F) y) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (f \in (x Hom (C) y) ⟼ ⟨(x 2^{nd} ((D {1^{st}}_{F} E) \circ_{func} F) y) (f), (x 2^{nd} ((D {2^{nd}}_{F} E) \circ_{func} F) y) (f)⟩))$
80	40 79	eqtrd	$⊢ φ \to 2^{nd} (F) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (f \in (x Hom (C) y) ⟼ ⟨(x 2^{nd} ((D {1^{st}}_{F} E) \circ_{func} F) y) (f), (x 2^{nd} ((D {2^{nd}}_{F} E) \circ_{func} F) y) (f)⟩))$
81	37 80	opeq12d	$⊢ φ \to ⟨1^{st} (F), 2^{nd} (F)⟩ = ⟨(x \in {Base}_{C} ⟼ ⟨1^{st} ((D {1^{st}}_{F} E) \circ_{func} F) (x), 1^{st} ((D {2^{nd}}_{F} E) \circ_{func} F) (x)⟩), (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (f \in (x Hom (C) y) ⟼ ⟨(x 2^{nd} ((D {1^{st}}_{F} E) \circ_{func} F) y) (f), (x 2^{nd} ((D {2^{nd}}_{F} E) \circ_{func} F) y) (f)⟩))⟩$
82		1st2nd	$⊢ (Rel (C Func T) \land F \in (C Func T)) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
83	9 2 82	sylancr	$⊢ φ \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
84		eqid	$⊢ ((D {1^{st}}_{F} E) \circ_{func} F) {⟨,⟩}_{F} ((D {2^{nd}}_{F} E) \circ_{func} F) = ((D {1^{st}}_{F} E) \circ_{func} F) {⟨,⟩}_{F} ((D {2^{nd}}_{F} E) \circ_{func} F)$
85	2 19	cofucl	$⊢ φ \to (D {1^{st}}_{F} E) \circ_{func} F \in (C Func D)$
86	2 29	cofucl	$⊢ φ \to (D {2^{nd}}_{F} E) \circ_{func} F \in (C Func E)$
87	84 5 41 85 86	prfval	$⊢ φ \to ((D {1^{st}}_{F} E) \circ_{func} F) {⟨,⟩}_{F} ((D {2^{nd}}_{F} E) \circ_{func} F) = ⟨(x \in {Base}_{C} ⟼ ⟨1^{st} ((D {1^{st}}_{F} E) \circ_{func} F) (x), 1^{st} ((D {2^{nd}}_{F} E) \circ_{func} F) (x)⟩), (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (f \in (x Hom (C) y) ⟼ ⟨(x 2^{nd} ((D {1^{st}}_{F} E) \circ_{func} F) y) (f), (x 2^{nd} ((D {2^{nd}}_{F} E) \circ_{func} F) y) (f)⟩))⟩$
88	81 83 87	3eqtr4d	$⊢ φ \to F = ((D {1^{st}}_{F} E) \circ_{func} F) {⟨,⟩}_{F} ((D {2^{nd}}_{F} E) \circ_{func} F)$

Metamath Proof Explorer

Theorem 1st2ndprf

Proof