Metamath Proof Explorer

Theorem 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 ) ) ) )