Metamath Proof Explorer


Theorem curry1

Description: Composition with ` ``' ( 2nd |`( { C } X. _V ) ) turns any binary operation F with a constant first operand into a function G of the second operand only. This transformation is called "currying". (Contributed by NM, 28-Mar-2008) (Revised by Mario Carneiro, 26-Dec-2014)

Ref Expression
Hypothesis curry1.1
|- G = ( F o. `' ( 2nd |` ( { C } X. _V ) ) )
Assertion curry1
|- ( ( F Fn ( A X. B ) /\ C e. A ) -> G = ( x e. B |-> ( C F x ) ) )

Proof

Step Hyp Ref Expression
1 curry1.1
 |-  G = ( F o. `' ( 2nd |` ( { C } X. _V ) ) )
2 fnfun
 |-  ( F Fn ( A X. B ) -> Fun F )
3 2ndconst
 |-  ( C e. A -> ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V )
4 dff1o3
 |-  ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V <-> ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -onto-> _V /\ Fun `' ( 2nd |` ( { C } X. _V ) ) ) )
5 4 simprbi
 |-  ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V -> Fun `' ( 2nd |` ( { C } X. _V ) ) )
6 3 5 syl
 |-  ( C e. A -> Fun `' ( 2nd |` ( { C } X. _V ) ) )
7 funco
 |-  ( ( Fun F /\ Fun `' ( 2nd |` ( { C } X. _V ) ) ) -> Fun ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) )
8 2 6 7 syl2an
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> Fun ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) )
9 dmco
 |-  dom ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) = ( `' `' ( 2nd |` ( { C } X. _V ) ) " dom F )
10 fndm
 |-  ( F Fn ( A X. B ) -> dom F = ( A X. B ) )
11 10 adantr
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> dom F = ( A X. B ) )
12 11 imaeq2d
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> ( `' `' ( 2nd |` ( { C } X. _V ) ) " dom F ) = ( `' `' ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) )
13 imacnvcnv
 |-  ( `' `' ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) = ( ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) )
14 df-ima
 |-  ( ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) = ran ( ( 2nd |` ( { C } X. _V ) ) |` ( A X. B ) )
15 resres
 |-  ( ( 2nd |` ( { C } X. _V ) ) |` ( A X. B ) ) = ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) )
16 15 rneqi
 |-  ran ( ( 2nd |` ( { C } X. _V ) ) |` ( A X. B ) ) = ran ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) )
17 13 14 16 3eqtri
 |-  ( `' `' ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) = ran ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) )
18 inxp
 |-  ( ( { C } X. _V ) i^i ( A X. B ) ) = ( ( { C } i^i A ) X. ( _V i^i B ) )
19 incom
 |-  ( _V i^i B ) = ( B i^i _V )
20 inv1
 |-  ( B i^i _V ) = B
21 19 20 eqtri
 |-  ( _V i^i B ) = B
22 21 xpeq2i
 |-  ( ( { C } i^i A ) X. ( _V i^i B ) ) = ( ( { C } i^i A ) X. B )
23 18 22 eqtri
 |-  ( ( { C } X. _V ) i^i ( A X. B ) ) = ( ( { C } i^i A ) X. B )
24 snssi
 |-  ( C e. A -> { C } C_ A )
25 df-ss
 |-  ( { C } C_ A <-> ( { C } i^i A ) = { C } )
26 24 25 sylib
 |-  ( C e. A -> ( { C } i^i A ) = { C } )
27 26 xpeq1d
 |-  ( C e. A -> ( ( { C } i^i A ) X. B ) = ( { C } X. B ) )
28 23 27 eqtrid
 |-  ( C e. A -> ( ( { C } X. _V ) i^i ( A X. B ) ) = ( { C } X. B ) )
29 28 reseq2d
 |-  ( C e. A -> ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) ) = ( 2nd |` ( { C } X. B ) ) )
30 29 rneqd
 |-  ( C e. A -> ran ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) ) = ran ( 2nd |` ( { C } X. B ) ) )
31 2ndconst
 |-  ( C e. A -> ( 2nd |` ( { C } X. B ) ) : ( { C } X. B ) -1-1-onto-> B )
32 f1ofo
 |-  ( ( 2nd |` ( { C } X. B ) ) : ( { C } X. B ) -1-1-onto-> B -> ( 2nd |` ( { C } X. B ) ) : ( { C } X. B ) -onto-> B )
33 forn
 |-  ( ( 2nd |` ( { C } X. B ) ) : ( { C } X. B ) -onto-> B -> ran ( 2nd |` ( { C } X. B ) ) = B )
34 31 32 33 3syl
 |-  ( C e. A -> ran ( 2nd |` ( { C } X. B ) ) = B )
35 30 34 eqtrd
 |-  ( C e. A -> ran ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) ) = B )
36 17 35 eqtrid
 |-  ( C e. A -> ( `' `' ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) = B )
37 36 adantl
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> ( `' `' ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) = B )
38 12 37 eqtrd
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> ( `' `' ( 2nd |` ( { C } X. _V ) ) " dom F ) = B )
39 9 38 eqtrid
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> dom ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) = B )
40 1 fneq1i
 |-  ( G Fn B <-> ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) Fn B )
41 df-fn
 |-  ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) Fn B <-> ( Fun ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) /\ dom ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) = B ) )
42 40 41 bitri
 |-  ( G Fn B <-> ( Fun ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) /\ dom ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) = B ) )
43 8 39 42 sylanbrc
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> G Fn B )
44 dffn5
 |-  ( G Fn B <-> G = ( x e. B |-> ( G ` x ) ) )
45 43 44 sylib
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> G = ( x e. B |-> ( G ` x ) ) )
46 1 fveq1i
 |-  ( G ` x ) = ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) ` x )
47 dff1o4
 |-  ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V <-> ( ( 2nd |` ( { C } X. _V ) ) Fn ( { C } X. _V ) /\ `' ( 2nd |` ( { C } X. _V ) ) Fn _V ) )
48 3 47 sylib
 |-  ( C e. A -> ( ( 2nd |` ( { C } X. _V ) ) Fn ( { C } X. _V ) /\ `' ( 2nd |` ( { C } X. _V ) ) Fn _V ) )
49 fvco2
 |-  ( ( `' ( 2nd |` ( { C } X. _V ) ) Fn _V /\ x e. _V ) -> ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) ` x ) = ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) )
50 49 elvd
 |-  ( `' ( 2nd |` ( { C } X. _V ) ) Fn _V -> ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) ` x ) = ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) )
51 48 50 simpl2im
 |-  ( C e. A -> ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) ` x ) = ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) )
52 51 ad2antlr
 |-  ( ( ( F Fn ( A X. B ) /\ C e. A ) /\ x e. B ) -> ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) ` x ) = ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) )
53 46 52 eqtrid
 |-  ( ( ( F Fn ( A X. B ) /\ C e. A ) /\ x e. B ) -> ( G ` x ) = ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) )
54 3 adantr
 |-  ( ( C e. A /\ x e. B ) -> ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V )
55 snidg
 |-  ( C e. A -> C e. { C } )
56 vex
 |-  x e. _V
57 opelxp
 |-  ( <. C , x >. e. ( { C } X. _V ) <-> ( C e. { C } /\ x e. _V ) )
58 55 56 57 sylanblrc
 |-  ( C e. A -> <. C , x >. e. ( { C } X. _V ) )
59 58 adantr
 |-  ( ( C e. A /\ x e. B ) -> <. C , x >. e. ( { C } X. _V ) )
60 54 59 jca
 |-  ( ( C e. A /\ x e. B ) -> ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V /\ <. C , x >. e. ( { C } X. _V ) ) )
61 58 fvresd
 |-  ( C e. A -> ( ( 2nd |` ( { C } X. _V ) ) ` <. C , x >. ) = ( 2nd ` <. C , x >. ) )
62 op2ndg
 |-  ( ( C e. A /\ x e. _V ) -> ( 2nd ` <. C , x >. ) = x )
63 62 elvd
 |-  ( C e. A -> ( 2nd ` <. C , x >. ) = x )
64 61 63 eqtrd
 |-  ( C e. A -> ( ( 2nd |` ( { C } X. _V ) ) ` <. C , x >. ) = x )
65 64 adantr
 |-  ( ( C e. A /\ x e. B ) -> ( ( 2nd |` ( { C } X. _V ) ) ` <. C , x >. ) = x )
66 f1ocnvfv
 |-  ( ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V /\ <. C , x >. e. ( { C } X. _V ) ) -> ( ( ( 2nd |` ( { C } X. _V ) ) ` <. C , x >. ) = x -> ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) = <. C , x >. ) )
67 60 65 66 sylc
 |-  ( ( C e. A /\ x e. B ) -> ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) = <. C , x >. )
68 67 fveq2d
 |-  ( ( C e. A /\ x e. B ) -> ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) = ( F ` <. C , x >. ) )
69 68 adantll
 |-  ( ( ( F Fn ( A X. B ) /\ C e. A ) /\ x e. B ) -> ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) = ( F ` <. C , x >. ) )
70 df-ov
 |-  ( C F x ) = ( F ` <. C , x >. )
71 69 70 eqtr4di
 |-  ( ( ( F Fn ( A X. B ) /\ C e. A ) /\ x e. B ) -> ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) = ( C F x ) )
72 53 71 eqtrd
 |-  ( ( ( F Fn ( A X. B ) /\ C e. A ) /\ x e. B ) -> ( G ` x ) = ( C F x ) )
73 72 mpteq2dva
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> ( x e. B |-> ( G ` x ) ) = ( x e. B |-> ( C F x ) ) )
74 45 73 eqtrd
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> G = ( x e. B |-> ( C F x ) ) )