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 "> uncurryF G )
	uncfval.c	\|- ( ph -> D e. Cat )
	uncfval.d	\|- ( ph -> E e. Cat )
	uncfval.f	\|- ( ph -> G e. ( C Func ( D FuncCat E ) ) )
Assertion	uncfval	\|- ( ph -> F = ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		uncfval.g	\|- F = ( <" C D E "> uncurryF G )
2		uncfval.c	\|- ( ph -> D e. Cat )
3		uncfval.d	\|- ( ph -> E e. Cat )
4		uncfval.f	\|- ( ph -> G e. ( C Func ( D FuncCat E ) ) )
5		df-uncf	\|- uncurryF = ( c e. _V , f e. _V \|-> ( ( ( c ` 1 ) evalF ( c ` 2 ) ) o.func ( ( f o.func ( ( c ` 0 ) 1stF ( c ` 1 ) ) ) pairF ( ( c ` 0 ) 2ndF ( c ` 1 ) ) ) ) )
6	5	a1i	\|- ( ph -> uncurryF = ( c e. _V , f e. _V \|-> ( ( ( c ` 1 ) evalF ( c ` 2 ) ) o.func ( ( f o.func ( ( c ` 0 ) 1stF ( c ` 1 ) ) ) pairF ( ( c ` 0 ) 2ndF ( c ` 1 ) ) ) ) ) )
7		simprl	\|- ( ( ph /\ ( c = <" C D E "> /\ f = G ) ) -> c = <" C D E "> )
8	7	fveq1d	\|- ( ( ph /\ ( c = <" C D E "> /\ f = G ) ) -> ( c ` 1 ) = ( <" C D E "> ` 1 ) )
9		s3fv1	\|- ( D e. Cat -> ( <" C D E "> ` 1 ) = D )
10	2 9	syl	\|- ( ph -> ( <" C D E "> ` 1 ) = D )
11	10	adantr	\|- ( ( ph /\ ( c = <" C D E "> /\ f = G ) ) -> ( <" C D E "> ` 1 ) = D )
12	8 11	eqtrd	\|- ( ( ph /\ ( c = <" C D E "> /\ f = G ) ) -> ( c ` 1 ) = D )
13	7	fveq1d	\|- ( ( ph /\ ( c = <" C D E "> /\ f = G ) ) -> ( c ` 2 ) = ( <" C D E "> ` 2 ) )
14		s3fv2	\|- ( E e. Cat -> ( <" C D E "> ` 2 ) = E )
15	3 14	syl	\|- ( ph -> ( <" C D E "> ` 2 ) = E )
16	15	adantr	\|- ( ( ph /\ ( c = <" C D E "> /\ f = G ) ) -> ( <" C D E "> ` 2 ) = E )
17	13 16	eqtrd	\|- ( ( ph /\ ( c = <" C D E "> /\ f = G ) ) -> ( c ` 2 ) = E )
18	12 17	oveq12d	\|- ( ( ph /\ ( c = <" C D E "> /\ f = G ) ) -> ( ( c ` 1 ) evalF ( c ` 2 ) ) = ( D evalF E ) )
19		simprr	\|- ( ( ph /\ ( c = <" C D E "> /\ f = G ) ) -> f = G )
20	7	fveq1d	\|- ( ( ph /\ ( c = <" C D E "> /\ f = G ) ) -> ( c ` 0 ) = ( <" C D E "> ` 0 ) )
21		funcrcl	\|- ( G e. ( C Func ( D FuncCat E ) ) -> ( C e. Cat /\ ( D FuncCat E ) e. Cat ) )
22	4 21	syl	\|- ( ph -> ( C e. Cat /\ ( D FuncCat E ) e. Cat ) )
23	22	simpld	\|- ( ph -> C e. Cat )
24		s3fv0	\|- ( C e. Cat -> ( <" C D E "> ` 0 ) = C )
25	23 24	syl	\|- ( ph -> ( <" C D E "> ` 0 ) = C )
26	25	adantr	\|- ( ( ph /\ ( c = <" C D E "> /\ f = G ) ) -> ( <" C D E "> ` 0 ) = C )
27	20 26	eqtrd	\|- ( ( ph /\ ( c = <" C D E "> /\ f = G ) ) -> ( c ` 0 ) = C )
28	27 12	oveq12d	\|- ( ( ph /\ ( c = <" C D E "> /\ f = G ) ) -> ( ( c ` 0 ) 1stF ( c ` 1 ) ) = ( C 1stF D ) )
29	19 28	oveq12d	\|- ( ( ph /\ ( c = <" C D E "> /\ f = G ) ) -> ( f o.func ( ( c ` 0 ) 1stF ( c ` 1 ) ) ) = ( G o.func ( C 1stF D ) ) )
30	27 12	oveq12d	\|- ( ( ph /\ ( c = <" C D E "> /\ f = G ) ) -> ( ( c ` 0 ) 2ndF ( c ` 1 ) ) = ( C 2ndF D ) )
31	29 30	oveq12d	\|- ( ( ph /\ ( c = <" C D E "> /\ f = G ) ) -> ( ( f o.func ( ( c ` 0 ) 1stF ( c ` 1 ) ) ) pairF ( ( c ` 0 ) 2ndF ( c ` 1 ) ) ) = ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) )
32	18 31	oveq12d	\|- ( ( ph /\ ( c = <" C D E "> /\ f = G ) ) -> ( ( ( c ` 1 ) evalF ( c ` 2 ) ) o.func ( ( f o.func ( ( c ` 0 ) 1stF ( c ` 1 ) ) ) pairF ( ( c ` 0 ) 2ndF ( c ` 1 ) ) ) ) = ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) )
33		s3cli	\|- <" C D E "> e. Word _V
34		elex	\|- ( <" C D E "> e. Word _V -> <" C D E "> e. _V )
35	33 34	mp1i	\|- ( ph -> <" C D E "> e. _V )
36	4	elexd	\|- ( ph -> G e. _V )
37		ovexd	\|- ( ph -> ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) e. _V )
38	6 32 35 36 37	ovmpod	\|- ( ph -> ( <" C D E "> uncurryF G ) = ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) )
39	1 38	eqtrid	\|- ( ph -> F = ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) pairF ( C 2ndF D ) ) ) )

Metamath Proof Explorer

Theorem uncfval

Proof