Metamath Proof Explorer

Theorem fsumcnv

Description: Transform a region of summation by using the converse operation. (Contributed by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypotheses fsumcnv.1 
|- ( x = <. j , k >. -> B = D )
fsumcnv.2 
|- ( y = <. k , j >. -> C = D )
fsumcnv.3 
|- ( ph -> A e. Fin )
fsumcnv.4 
|- ( ph -> Rel A )
fsumcnv.5 
|- ( ( ph /\ x e. A ) -> B e. CC )
Assertion fsumcnv 
|- ( ph -> sum_ x e. A B = sum_ y e. `' A C )

Proof

Step Hyp Ref Expression
1 fsumcnv.1 
 |-  ( x = <. j , k >. -> B = D )
2 fsumcnv.2 
 |-  ( y = <. k , j >. -> C = D )
3 fsumcnv.3 
 |-  ( ph -> A e. Fin )
4 fsumcnv.4 
 |-  ( ph -> Rel A )
5 fsumcnv.5 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
6 csbeq1a 
 |-  ( x = <. ( 2nd ` y ) , ( 1st ` y ) >. -> B = [_ <. ( 2nd ` y ) , ( 1st ` y ) >. / x ]_ B )
7 fvex 
 |-  ( 2nd ` y ) e. _V
8 fvex 
 |-  ( 1st ` y ) e. _V
9 opex 
 |-  <. j , k >. e. _V
10 9 1 csbie 
 |-  [_ <. j , k >. / x ]_ B = D
11 opeq12 
 |-  ( ( j = ( 2nd ` y ) /\ k = ( 1st ` y ) ) -> <. j , k >. = <. ( 2nd ` y ) , ( 1st ` y ) >. )
12 11 csbeq1d 
 |-  ( ( j = ( 2nd ` y ) /\ k = ( 1st ` y ) ) -> [_ <. j , k >. / x ]_ B = [_ <. ( 2nd ` y ) , ( 1st ` y ) >. / x ]_ B )
13 10 12 eqtr3id 
 |-  ( ( j = ( 2nd ` y ) /\ k = ( 1st ` y ) ) -> D = [_ <. ( 2nd ` y ) , ( 1st ` y ) >. / x ]_ B )
14 7 8 13 csbie2 
 |-  [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / k ]_ D = [_ <. ( 2nd ` y ) , ( 1st ` y ) >. / x ]_ B
15 6 14 eqtr4di 
 |-  ( x = <. ( 2nd ` y ) , ( 1st ` y ) >. -> B = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / k ]_ D )
16 cnvfi 
 |-  ( A e. Fin -> `' A e. Fin )
17 3 16 syl 
 |-  ( ph -> `' A e. Fin )
18 relcnv 
 |-  Rel `' A
19 cnvf1o 
 |-  ( Rel `' A -> ( z e. `' A |-> U. `' { z } ) : `' A -1-1-onto-> `' `' A )
20 18 19 ax-mp 
 |-  ( z e. `' A |-> U. `' { z } ) : `' A -1-1-onto-> `' `' A
21 dfrel2 
 |-  ( Rel A <-> `' `' A = A )
22 4 21 sylib 
 |-  ( ph -> `' `' A = A )
23 22 f1oeq3d 
 |-  ( ph -> ( ( z e. `' A |-> U. `' { z } ) : `' A -1-1-onto-> `' `' A <-> ( z e. `' A |-> U. `' { z } ) : `' A -1-1-onto-> A ) )
24 20 23 mpbii 
 |-  ( ph -> ( z e. `' A |-> U. `' { z } ) : `' A -1-1-onto-> A )
25 1st2nd 
 |-  ( ( Rel `' A /\ y e. `' A ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
26 18 25 mpan 
 |-  ( y e. `' A -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
27 26 fveq2d 
 |-  ( y e. `' A -> ( ( z e. `' A |-> U. `' { z } ) ` y ) = ( ( z e. `' A |-> U. `' { z } ) ` <. ( 1st ` y ) , ( 2nd ` y ) >. ) )
28 id 
 |-  ( y e. `' A -> y e. `' A )
29 26 28 eqeltrrd 
 |-  ( y e. `' A -> <. ( 1st ` y ) , ( 2nd ` y ) >. e. `' A )
30 sneq 
 |-  ( z = <. ( 1st ` y ) , ( 2nd ` y ) >. -> { z } = { <. ( 1st ` y ) , ( 2nd ` y ) >. } )
31 30 cnveqd 
 |-  ( z = <. ( 1st ` y ) , ( 2nd ` y ) >. -> `' { z } = `' { <. ( 1st ` y ) , ( 2nd ` y ) >. } )
32 31 unieqd 
 |-  ( z = <. ( 1st ` y ) , ( 2nd ` y ) >. -> U. `' { z } = U. `' { <. ( 1st ` y ) , ( 2nd ` y ) >. } )
33 opswap 
 |-  U. `' { <. ( 1st ` y ) , ( 2nd ` y ) >. } = <. ( 2nd ` y ) , ( 1st ` y ) >.
34 32 33 eqtrdi 
 |-  ( z = <. ( 1st ` y ) , ( 2nd ` y ) >. -> U. `' { z } = <. ( 2nd ` y ) , ( 1st ` y ) >. )
35 eqid 
 |-  ( z e. `' A |-> U. `' { z } ) = ( z e. `' A |-> U. `' { z } )
36 opex 
 |-  <. ( 2nd ` y ) , ( 1st ` y ) >. e. _V
37 34 35 36 fvmpt 
 |-  ( <. ( 1st ` y ) , ( 2nd ` y ) >. e. `' A -> ( ( z e. `' A |-> U. `' { z } ) ` <. ( 1st ` y ) , ( 2nd ` y ) >. ) = <. ( 2nd ` y ) , ( 1st ` y ) >. )
38 29 37 syl 
 |-  ( y e. `' A -> ( ( z e. `' A |-> U. `' { z } ) ` <. ( 1st ` y ) , ( 2nd ` y ) >. ) = <. ( 2nd ` y ) , ( 1st ` y ) >. )
39 27 38 eqtrd 
 |-  ( y e. `' A -> ( ( z e. `' A |-> U. `' { z } ) ` y ) = <. ( 2nd ` y ) , ( 1st ` y ) >. )
40 39 adantl 
 |-  ( ( ph /\ y e. `' A ) -> ( ( z e. `' A |-> U. `' { z } ) ` y ) = <. ( 2nd ` y ) , ( 1st ` y ) >. )
41 15 17 24 40 5 fsumf1o 
 |-  ( ph -> sum_ x e. A B = sum_ y e. `' A [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / k ]_ D )
42 csbeq1a 
 |-  ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. -> C = [_ <. ( 1st ` y ) , ( 2nd ` y ) >. / y ]_ C )
43 26 42 syl 
 |-  ( y e. `' A -> C = [_ <. ( 1st ` y ) , ( 2nd ` y ) >. / y ]_ C )
44 opex 
 |-  <. k , j >. e. _V
45 44 2 csbie 
 |-  [_ <. k , j >. / y ]_ C = D
46 opeq12 
 |-  ( ( k = ( 1st ` y ) /\ j = ( 2nd ` y ) ) -> <. k , j >. = <. ( 1st ` y ) , ( 2nd ` y ) >. )
47 46 ancoms 
 |-  ( ( j = ( 2nd ` y ) /\ k = ( 1st ` y ) ) -> <. k , j >. = <. ( 1st ` y ) , ( 2nd ` y ) >. )
48 47 csbeq1d 
 |-  ( ( j = ( 2nd ` y ) /\ k = ( 1st ` y ) ) -> [_ <. k , j >. / y ]_ C = [_ <. ( 1st ` y ) , ( 2nd ` y ) >. / y ]_ C )
49 45 48 eqtr3id 
 |-  ( ( j = ( 2nd ` y ) /\ k = ( 1st ` y ) ) -> D = [_ <. ( 1st ` y ) , ( 2nd ` y ) >. / y ]_ C )
50 7 8 49 csbie2 
 |-  [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / k ]_ D = [_ <. ( 1st ` y ) , ( 2nd ` y ) >. / y ]_ C
51 43 50 eqtr4di 
 |-  ( y e. `' A -> C = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / k ]_ D )
52 51 sumeq2i 
 |-  sum_ y e. `' A C = sum_ y e. `' A [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / k ]_ D
53 41 52 eqtr4di 
 |-  ( ph -> sum_ x e. A B = sum_ y e. `' A C )