uncfval

Description: Value of the uncurry functor, which is the reverse of the curry functor, taking G : C --> ( D --> E ) to uncurryF ( G ) : C X. D --> E . (Contributed by Mario Carneiro, 13-Jan-2017)

	Ref	Expression
Hypotheses	uncfval.g	$⊢ F = ⟨“ C D E ”⟩ {uncurry}_{F} G$
	uncfval.c	$⊢ φ \to D \in Cat$
	uncfval.d	$⊢ φ \to E \in Cat$
	uncfval.f	$⊢ φ \to G \in (C Func (D FuncCat E))$
Assertion	uncfval	$⊢ φ \to F = (D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D))$

Proof

Step	Hyp	Ref	Expression
1		uncfval.g	$⊢ F = ⟨“ C D E ”⟩ {uncurry}_{F} G$
2		uncfval.c	$⊢ φ \to D \in Cat$
3		uncfval.d	$⊢ φ \to E \in Cat$
4		uncfval.f	$⊢ φ \to G \in (C Func (D FuncCat E))$
5		df-uncf	$⊢ {uncurry}_{F} = (c \in V, f \in V ⟼ (c (1) {eval}_{F} c (2)) \circ_{func} ((f \circ_{func} (c (0) {1^{st}}_{F} c (1))) {⟨,⟩}_{F} (c (0) {2^{nd}}_{F} c (1))))$
6	5	a1i	$⊢ φ \to {uncurry}_{F} = (c \in V, f \in V ⟼ (c (1) {eval}_{F} c (2)) \circ_{func} ((f \circ_{func} (c (0) {1^{st}}_{F} c (1))) {⟨,⟩}_{F} (c (0) {2^{nd}}_{F} c (1))))$
7		simprl	$⊢ (φ \land (c = ⟨“ C D E ”⟩ \land f = G)) \to c = ⟨“ C D E ”⟩$
8	7	fveq1d	$⊢ (φ \land (c = ⟨“ C D E ”⟩ \land f = G)) \to c (1) = ⟨“ C D E ”⟩ (1)$
9		s3fv1	$⊢ D \in Cat \to ⟨“ C D E ”⟩ (1) = D$
10	2 9	syl	$⊢ φ \to ⟨“ C D E ”⟩ (1) = D$
11	10	adantr	$⊢ (φ \land (c = ⟨“ C D E ”⟩ \land f = G)) \to ⟨“ C D E ”⟩ (1) = D$
12	8 11	eqtrd	$⊢ (φ \land (c = ⟨“ C D E ”⟩ \land f = G)) \to c (1) = D$
13	7	fveq1d	$⊢ (φ \land (c = ⟨“ C D E ”⟩ \land f = G)) \to c (2) = ⟨“ C D E ”⟩ (2)$
14		s3fv2	$⊢ E \in Cat \to ⟨“ C D E ”⟩ (2) = E$
15	3 14	syl	$⊢ φ \to ⟨“ C D E ”⟩ (2) = E$
16	15	adantr	$⊢ (φ \land (c = ⟨“ C D E ”⟩ \land f = G)) \to ⟨“ C D E ”⟩ (2) = E$
17	13 16	eqtrd	$⊢ (φ \land (c = ⟨“ C D E ”⟩ \land f = G)) \to c (2) = E$
18	12 17	oveq12d	$⊢ (φ \land (c = ⟨“ C D E ”⟩ \land f = G)) \to c (1) {eval}_{F} c (2) = D {eval}_{F} E$
19		simprr	$⊢ (φ \land (c = ⟨“ C D E ”⟩ \land f = G)) \to f = G$
20	7	fveq1d	$⊢ (φ \land (c = ⟨“ C D E ”⟩ \land f = G)) \to c (0) = ⟨“ C D E ”⟩ (0)$
21		funcrcl	$⊢ G \in (C Func (D FuncCat E)) \to (C \in Cat \land D FuncCat E \in Cat)$
22	4 21	syl	$⊢ φ \to (C \in Cat \land D FuncCat E \in Cat)$
23	22	simpld	$⊢ φ \to C \in Cat$
24		s3fv0	$⊢ C \in Cat \to ⟨“ C D E ”⟩ (0) = C$
25	23 24	syl	$⊢ φ \to ⟨“ C D E ”⟩ (0) = C$
26	25	adantr	$⊢ (φ \land (c = ⟨“ C D E ”⟩ \land f = G)) \to ⟨“ C D E ”⟩ (0) = C$
27	20 26	eqtrd	$⊢ (φ \land (c = ⟨“ C D E ”⟩ \land f = G)) \to c (0) = C$
28	27 12	oveq12d	$⊢ (φ \land (c = ⟨“ C D E ”⟩ \land f = G)) \to c (0) {1^{st}}_{F} c (1) = C {1^{st}}_{F} D$
29	19 28	oveq12d	$⊢ (φ \land (c = ⟨“ C D E ”⟩ \land f = G)) \to f \circ_{func} (c (0) {1^{st}}_{F} c (1)) = G \circ_{func} (C {1^{st}}_{F} D)$
30	27 12	oveq12d	$⊢ (φ \land (c = ⟨“ C D E ”⟩ \land f = G)) \to c (0) {2^{nd}}_{F} c (1) = C {2^{nd}}_{F} D$
31	29 30	oveq12d	$⊢ (φ \land (c = ⟨“ C D E ”⟩ \land f = G)) \to (f \circ_{func} (c (0) {1^{st}}_{F} c (1))) {⟨,⟩}_{F} (c (0) {2^{nd}}_{F} c (1)) = (G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)$
32	18 31	oveq12d	$⊢ (φ \land (c = ⟨“ C D E ”⟩ \land f = G)) \to (c (1) {eval}_{F} c (2)) \circ_{func} ((f \circ_{func} (c (0) {1^{st}}_{F} c (1))) {⟨,⟩}_{F} (c (0) {2^{nd}}_{F} c (1))) = (D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D))$
33		s3cli	$⊢ ⟨“ C D E ”⟩ \in Word V$
34		elex	$⊢ ⟨“ C D E ”⟩ \in Word V \to ⟨“ C D E ”⟩ \in V$
35	33 34	mp1i	$⊢ φ \to ⟨“ C D E ”⟩ \in V$
36	4	elexd	$⊢ φ \to G \in V$
37		ovexd	$⊢ φ \to (D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) \in V$
38	6 32 35 36 37	ovmpod	$⊢ φ \to ⟨“ C D E ”⟩ {uncurry}_{F} G = (D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D))$
39	1 38	syl5eq	$⊢ φ \to F = (D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D))$

Metamath Proof Explorer

Theorem uncfval

Proof