Metamath Proof Explorer

Theorem fvmpocurryd

Description: The value of the value of a curried operation given in maps-to notation is the operation value of the original operation. (Contributed by AV, 27-Oct-2019)

Ref Expression
Hypotheses fvmpocurryd.f 
|- F = ( x e. X , y e. Y |-> C )
fvmpocurryd.c 
|- ( ph -> A. x e. X A. y e. Y C e. V )
fvmpocurryd.y 
|- ( ph -> Y e. W )
fvmpocurryd.a 
|- ( ph -> A e. X )
fvmpocurryd.b 
|- ( ph -> B e. Y )
Assertion fvmpocurryd 
|- ( ph -> ( ( curry F ` A ) ` B ) = ( A F B ) )

Proof

Step Hyp Ref Expression
1 fvmpocurryd.f 
 |-  F = ( x e. X , y e. Y |-> C )
2 fvmpocurryd.c 
 |-  ( ph -> A. x e. X A. y e. Y C e. V )
3 fvmpocurryd.y 
 |-  ( ph -> Y e. W )
4 fvmpocurryd.a 
 |-  ( ph -> A e. X )
5 fvmpocurryd.b 
 |-  ( ph -> B e. Y )
6 csbcom 
 |-  [_ B / b ]_ [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C = [_ A / a ]_ [_ B / b ]_ [_ b / y ]_ [_ a / x ]_ C
7 csbcow 
 |-  [_ B / b ]_ [_ b / y ]_ [_ a / x ]_ C = [_ B / y ]_ [_ a / x ]_ C
8 7 csbeq2i 
 |-  [_ A / a ]_ [_ B / b ]_ [_ b / y ]_ [_ a / x ]_ C = [_ A / a ]_ [_ B / y ]_ [_ a / x ]_ C
9 csbcom 
 |-  [_ A / a ]_ [_ B / y ]_ [_ a / x ]_ C = [_ B / y ]_ [_ A / a ]_ [_ a / x ]_ C
10 csbcow 
 |-  [_ A / a ]_ [_ a / x ]_ C = [_ A / x ]_ C
11 10 csbeq2i 
 |-  [_ B / y ]_ [_ A / a ]_ [_ a / x ]_ C = [_ B / y ]_ [_ A / x ]_ C
12 9 11 eqtri 
 |-  [_ A / a ]_ [_ B / y ]_ [_ a / x ]_ C = [_ B / y ]_ [_ A / x ]_ C
13 6 8 12 3eqtri 
 |-  [_ B / b ]_ [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C = [_ B / y ]_ [_ A / x ]_ C
14 nfcsb1v 
 |-  F/_ x [_ A / x ]_ C
15 14 nfel1 
 |-  F/ x [_ A / x ]_ C e. V
16 nfcsb1v 
 |-  F/_ y [_ B / y ]_ [_ A / x ]_ C
17 16 nfel1 
 |-  F/ y [_ B / y ]_ [_ A / x ]_ C e. V
18 csbeq1a 
 |-  ( x = A -> C = [_ A / x ]_ C )
19 18 eleq1d 
 |-  ( x = A -> ( C e. V <-> [_ A / x ]_ C e. V ) )
20 csbeq1a 
 |-  ( y = B -> [_ A / x ]_ C = [_ B / y ]_ [_ A / x ]_ C )
21 20 eleq1d 
 |-  ( y = B -> ( [_ A / x ]_ C e. V <-> [_ B / y ]_ [_ A / x ]_ C e. V ) )
22 15 17 19 21 rspc2 
 |-  ( ( A e. X /\ B e. Y ) -> ( A. x e. X A. y e. Y C e. V -> [_ B / y ]_ [_ A / x ]_ C e. V ) )
23 22 imp 
 |-  ( ( ( A e. X /\ B e. Y ) /\ A. x e. X A. y e. Y C e. V ) -> [_ B / y ]_ [_ A / x ]_ C e. V )
24 4 5 2 23 syl21anc 
 |-  ( ph -> [_ B / y ]_ [_ A / x ]_ C e. V )
25 13 24 eqeltrid 
 |-  ( ph -> [_ B / b ]_ [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C e. V )
26 eqid 
 |-  ( b e. Y |-> [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C ) = ( b e. Y |-> [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C )
27 26 fvmpts 
 |-  ( ( B e. Y /\ [_ B / b ]_ [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C e. V ) -> ( ( b e. Y |-> [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C ) ` B ) = [_ B / b ]_ [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C )
28 5 25 27 syl2anc 
 |-  ( ph -> ( ( b e. Y |-> [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C ) ` B ) = [_ B / b ]_ [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C )
29 nfcv 
 |-  F/_ a C
30 nfcv 
 |-  F/_ b C
31 nfcv 
 |-  F/_ x b
32 nfcsb1v 
 |-  F/_ x [_ a / x ]_ C
33 31 32 nfcsbw 
 |-  F/_ x [_ b / y ]_ [_ a / x ]_ C
34 nfcsb1v 
 |-  F/_ y [_ b / y ]_ [_ a / x ]_ C
35 csbeq1a 
 |-  ( x = a -> C = [_ a / x ]_ C )
36 csbeq1a 
 |-  ( y = b -> [_ a / x ]_ C = [_ b / y ]_ [_ a / x ]_ C )
37 35 36 sylan9eq 
 |-  ( ( x = a /\ y = b ) -> C = [_ b / y ]_ [_ a / x ]_ C )
38 29 30 33 34 37 cbvmpo 
 |-  ( x e. X , y e. Y |-> C ) = ( a e. X , b e. Y |-> [_ b / y ]_ [_ a / x ]_ C )
39 1 38 eqtri 
 |-  F = ( a e. X , b e. Y |-> [_ b / y ]_ [_ a / x ]_ C )
40 32 nfel1 
 |-  F/ x [_ a / x ]_ C e. V
41 34 nfel1 
 |-  F/ y [_ b / y ]_ [_ a / x ]_ C e. V
42 35 eleq1d 
 |-  ( x = a -> ( C e. V <-> [_ a / x ]_ C e. V ) )
43 36 eleq1d 
 |-  ( y = b -> ( [_ a / x ]_ C e. V <-> [_ b / y ]_ [_ a / x ]_ C e. V ) )
44 40 41 42 43 rspc2 
 |-  ( ( a e. X /\ b e. Y ) -> ( A. x e. X A. y e. Y C e. V -> [_ b / y ]_ [_ a / x ]_ C e. V ) )
45 2 44 mpan9 
 |-  ( ( ph /\ ( a e. X /\ b e. Y ) ) -> [_ b / y ]_ [_ a / x ]_ C e. V )
46 45 ralrimivva 
 |-  ( ph -> A. a e. X A. b e. Y [_ b / y ]_ [_ a / x ]_ C e. V )
47 5 ne0d 
 |-  ( ph -> Y =/= (/) )
48 39 46 47 3 4 mpocurryvald 
 |-  ( ph -> ( curry F ` A ) = ( b e. Y |-> [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C ) )
49 48 fveq1d 
 |-  ( ph -> ( ( curry F ` A ) ` B ) = ( ( b e. Y |-> [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C ) ` B ) )
50 1 a1i 
 |-  ( ph -> F = ( x e. X , y e. Y |-> C ) )
51 csbcow 
 |-  [_ y / b ]_ [_ b / y ]_ [_ a / x ]_ C = [_ y / y ]_ [_ a / x ]_ C
52 csbid 
 |-  [_ y / y ]_ [_ a / x ]_ C = [_ a / x ]_ C
53 51 52 eqtr2i 
 |-  [_ a / x ]_ C = [_ y / b ]_ [_ b / y ]_ [_ a / x ]_ C
54 53 a1i 
 |-  ( ph -> [_ a / x ]_ C = [_ y / b ]_ [_ b / y ]_ [_ a / x ]_ C )
55 54 csbeq2dv 
 |-  ( ph -> [_ x / a ]_ [_ a / x ]_ C = [_ x / a ]_ [_ y / b ]_ [_ b / y ]_ [_ a / x ]_ C )
56 csbcow 
 |-  [_ x / a ]_ [_ a / x ]_ C = [_ x / x ]_ C
57 csbid 
 |-  [_ x / x ]_ C = C
58 56 57 eqtri 
 |-  [_ x / a ]_ [_ a / x ]_ C = C
59 csbcom 
 |-  [_ x / a ]_ [_ y / b ]_ [_ b / y ]_ [_ a / x ]_ C = [_ y / b ]_ [_ x / a ]_ [_ b / y ]_ [_ a / x ]_ C
60 55 58 59 3eqtr3g 
 |-  ( ph -> C = [_ y / b ]_ [_ x / a ]_ [_ b / y ]_ [_ a / x ]_ C )
61 csbeq1 
 |-  ( x = A -> [_ x / a ]_ [_ b / y ]_ [_ a / x ]_ C = [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C )
62 61 adantr 
 |-  ( ( x = A /\ y = B ) -> [_ x / a ]_ [_ b / y ]_ [_ a / x ]_ C = [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C )
63 62 csbeq2dv 
 |-  ( ( x = A /\ y = B ) -> [_ y / b ]_ [_ x / a ]_ [_ b / y ]_ [_ a / x ]_ C = [_ y / b ]_ [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C )
64 csbeq1 
 |-  ( y = B -> [_ y / b ]_ [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C = [_ B / b ]_ [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C )
65 64 adantl 
 |-  ( ( x = A /\ y = B ) -> [_ y / b ]_ [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C = [_ B / b ]_ [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C )
66 63 65 eqtrd 
 |-  ( ( x = A /\ y = B ) -> [_ y / b ]_ [_ x / a ]_ [_ b / y ]_ [_ a / x ]_ C = [_ B / b ]_ [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C )
67 60 66 sylan9eq 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> C = [_ B / b ]_ [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C )
68 eqidd 
 |-  ( ( ph /\ x = A ) -> Y = Y )
69 nfv 
 |-  F/ x ph
70 nfv 
 |-  F/ y ph
71 nfcv 
 |-  F/_ y A
72 nfcv 
 |-  F/_ x B
73 nfcv 
 |-  F/_ x A
74 73 33 nfcsbw 
 |-  F/_ x [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C
75 72 74 nfcsbw 
 |-  F/_ x [_ B / b ]_ [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C
76 13 16 nfcxfr 
 |-  F/_ y [_ B / b ]_ [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C
77 50 67 68 4 5 25 69 70 71 72 75 76 ovmpodxf 
 |-  ( ph -> ( A F B ) = [_ B / b ]_ [_ A / a ]_ [_ b / y ]_ [_ a / x ]_ C )
78 28 49 77 3eqtr4d 
 |-  ( ph -> ( ( curry F ` A ) ` B ) = ( A F B ) )