Metamath Proof Explorer

Theorem gsumcom2

Description: Two-dimensional commutation of a group sum. Note that while A and D are constants w.r.t. j , k , C ( j ) and E ( k ) are not. (Contributed by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses gsum2d2.b 
|- B = ( Base ` G )
gsum2d2.z 
|- .0. = ( 0g ` G )
gsum2d2.g 
|- ( ph -> G e. CMnd )
gsum2d2.a 
|- ( ph -> A e. V )
gsum2d2.r 
|- ( ( ph /\ j e. A ) -> C e. W )
gsum2d2.f 
|- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )
gsum2d2.u 
|- ( ph -> U e. Fin )
gsum2d2.n 
|- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) -> X = .0. )
gsumcom2.d 
|- ( ph -> D e. Y )
gsumcom2.c 
|- ( ph -> ( ( j e. A /\ k e. C ) <-> ( k e. D /\ j e. E ) ) )
Assertion gsumcom2 
|- ( ph -> ( G gsum ( j e. A , k e. C |-> X ) ) = ( G gsum ( k e. D , j e. E |-> X ) ) )

Proof

Step Hyp Ref Expression
1 gsum2d2.b 
 |-  B = ( Base ` G )
2 gsum2d2.z 
 |-  .0. = ( 0g ` G )
3 gsum2d2.g 
 |-  ( ph -> G e. CMnd )
4 gsum2d2.a 
 |-  ( ph -> A e. V )
5 gsum2d2.r 
 |-  ( ( ph /\ j e. A ) -> C e. W )
6 gsum2d2.f 
 |-  ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )
7 gsum2d2.u 
 |-  ( ph -> U e. Fin )
8 gsum2d2.n 
 |-  ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) -> X = .0. )
9 gsumcom2.d 
 |-  ( ph -> D e. Y )
10 gsumcom2.c 
 |-  ( ph -> ( ( j e. A /\ k e. C ) <-> ( k e. D /\ j e. E ) ) )
11 snex 
 |-  { j } e. _V
12 xpexg 
 |-  ( ( { j } e. _V /\ C e. W ) -> ( { j } X. C ) e. _V )
13 11 5 12 sylancr 
 |-  ( ( ph /\ j e. A ) -> ( { j } X. C ) e. _V )
14 13 ralrimiva 
 |-  ( ph -> A. j e. A ( { j } X. C ) e. _V )
15 iunexg 
 |-  ( ( A e. V /\ A. j e. A ( { j } X. C ) e. _V ) -> U_ j e. A ( { j } X. C ) e. _V )
16 4 14 15 syl2anc 
 |-  ( ph -> U_ j e. A ( { j } X. C ) e. _V )
17 6 ralrimivva 
 |-  ( ph -> A. j e. A A. k e. C X e. B )
18 eqid 
 |-  ( j e. A , k e. C |-> X ) = ( j e. A , k e. C |-> X )
19 18 fmpox 
 |-  ( A. j e. A A. k e. C X e. B <-> ( j e. A , k e. C |-> X ) : U_ j e. A ( { j } X. C ) --> B )
20 17 19 sylib 
 |-  ( ph -> ( j e. A , k e. C |-> X ) : U_ j e. A ( { j } X. C ) --> B )
21 1 2 3 4 5 6 7 8 gsum2d2lem 
 |-  ( ph -> ( j e. A , k e. C |-> X ) finSupp .0. )
22 relxp 
 |-  Rel ( { k } X. E )
23 22 rgenw 
 |-  A. k e. D Rel ( { k } X. E )
24 reliun 
 |-  ( Rel U_ k e. D ( { k } X. E ) <-> A. k e. D Rel ( { k } X. E ) )
25 23 24 mpbir 
 |-  Rel U_ k e. D ( { k } X. E )
26 cnvf1o 
 |-  ( Rel U_ k e. D ( { k } X. E ) -> ( z e. U_ k e. D ( { k } X. E ) |-> U. `' { z } ) : U_ k e. D ( { k } X. E ) -1-1-onto-> `' U_ k e. D ( { k } X. E ) )
27 25 26 ax-mp 
 |-  ( z e. U_ k e. D ( { k } X. E ) |-> U. `' { z } ) : U_ k e. D ( { k } X. E ) -1-1-onto-> `' U_ k e. D ( { k } X. E )
28 relxp 
 |-  Rel ( { j } X. C )
29 28 rgenw 
 |-  A. j e. A Rel ( { j } X. C )
30 reliun 
 |-  ( Rel U_ j e. A ( { j } X. C ) <-> A. j e. A Rel ( { j } X. C ) )
31 29 30 mpbir 
 |-  Rel U_ j e. A ( { j } X. C )
32 relcnv 
 |-  Rel `' U_ k e. D ( { k } X. E )
33 nfv 
 |-  F/ k ph
34 nfv 
 |-  F/ k <. x , y >. e. U_ j e. A ( { j } X. C )
35 nfiu1 
 |-  F/_ k U_ k e. D ( { k } X. E )
36 35 nfcnv 
 |-  F/_ k `' U_ k e. D ( { k } X. E )
37 36 nfel2 
 |-  F/ k <. x , y >. e. `' U_ k e. D ( { k } X. E )
38 34 37 nfbi 
 |-  F/ k ( <. x , y >. e. U_ j e. A ( { j } X. C ) <-> <. x , y >. e. `' U_ k e. D ( { k } X. E ) )
39 33 38 nfim 
 |-  F/ k ( ph -> ( <. x , y >. e. U_ j e. A ( { j } X. C ) <-> <. x , y >. e. `' U_ k e. D ( { k } X. E ) ) )
40 opeq2 
 |-  ( k = y -> <. x , k >. = <. x , y >. )
41 40 eleq1d 
 |-  ( k = y -> ( <. x , k >. e. U_ j e. A ( { j } X. C ) <-> <. x , y >. e. U_ j e. A ( { j } X. C ) ) )
42 40 eleq1d 
 |-  ( k = y -> ( <. x , k >. e. `' U_ k e. D ( { k } X. E ) <-> <. x , y >. e. `' U_ k e. D ( { k } X. E ) ) )
43 41 42 bibi12d 
 |-  ( k = y -> ( ( <. x , k >. e. U_ j e. A ( { j } X. C ) <-> <. x , k >. e. `' U_ k e. D ( { k } X. E ) ) <-> ( <. x , y >. e. U_ j e. A ( { j } X. C ) <-> <. x , y >. e. `' U_ k e. D ( { k } X. E ) ) ) )
44 43 imbi2d 
 |-  ( k = y -> ( ( ph -> ( <. x , k >. e. U_ j e. A ( { j } X. C ) <-> <. x , k >. e. `' U_ k e. D ( { k } X. E ) ) ) <-> ( ph -> ( <. x , y >. e. U_ j e. A ( { j } X. C ) <-> <. x , y >. e. `' U_ k e. D ( { k } X. E ) ) ) ) )
45 nfv 
 |-  F/ j ph
46 nfiu1 
 |-  F/_ j U_ j e. A ( { j } X. C )
47 46 nfel2 
 |-  F/ j <. x , k >. e. U_ j e. A ( { j } X. C )
48 nfv 
 |-  F/ j <. x , k >. e. `' U_ k e. D ( { k } X. E )
49 47 48 nfbi 
 |-  F/ j ( <. x , k >. e. U_ j e. A ( { j } X. C ) <-> <. x , k >. e. `' U_ k e. D ( { k } X. E ) )
50 45 49 nfim 
 |-  F/ j ( ph -> ( <. x , k >. e. U_ j e. A ( { j } X. C ) <-> <. x , k >. e. `' U_ k e. D ( { k } X. E ) ) )
51 opeq1 
 |-  ( j = x -> <. j , k >. = <. x , k >. )
52 51 eleq1d 
 |-  ( j = x -> ( <. j , k >. e. U_ j e. A ( { j } X. C ) <-> <. x , k >. e. U_ j e. A ( { j } X. C ) ) )
53 51 eleq1d 
 |-  ( j = x -> ( <. j , k >. e. `' U_ k e. D ( { k } X. E ) <-> <. x , k >. e. `' U_ k e. D ( { k } X. E ) ) )
54 52 53 bibi12d 
 |-  ( j = x -> ( ( <. j , k >. e. U_ j e. A ( { j } X. C ) <-> <. j , k >. e. `' U_ k e. D ( { k } X. E ) ) <-> ( <. x , k >. e. U_ j e. A ( { j } X. C ) <-> <. x , k >. e. `' U_ k e. D ( { k } X. E ) ) ) )
55 54 imbi2d 
 |-  ( j = x -> ( ( ph -> ( <. j , k >. e. U_ j e. A ( { j } X. C ) <-> <. j , k >. e. `' U_ k e. D ( { k } X. E ) ) ) <-> ( ph -> ( <. x , k >. e. U_ j e. A ( { j } X. C ) <-> <. x , k >. e. `' U_ k e. D ( { k } X. E ) ) ) ) )
56 opeliunxp 
 |-  ( <. j , k >. e. U_ j e. A ( { j } X. C ) <-> ( j e. A /\ k e. C ) )
57 opeliunxp 
 |-  ( <. k , j >. e. U_ k e. D ( { k } X. E ) <-> ( k e. D /\ j e. E ) )
58 10 56 57 3bitr4g 
 |-  ( ph -> ( <. j , k >. e. U_ j e. A ( { j } X. C ) <-> <. k , j >. e. U_ k e. D ( { k } X. E ) ) )
59 vex 
 |-  j e. _V
60 vex 
 |-  k e. _V
61 59 60 opelcnv 
 |-  ( <. j , k >. e. `' U_ k e. D ( { k } X. E ) <-> <. k , j >. e. U_ k e. D ( { k } X. E ) )
62 58 61 bitr4di 
 |-  ( ph -> ( <. j , k >. e. U_ j e. A ( { j } X. C ) <-> <. j , k >. e. `' U_ k e. D ( { k } X. E ) ) )
63 50 55 62 chvarfv 
 |-  ( ph -> ( <. x , k >. e. U_ j e. A ( { j } X. C ) <-> <. x , k >. e. `' U_ k e. D ( { k } X. E ) ) )
64 39 44 63 chvarfv 
 |-  ( ph -> ( <. x , y >. e. U_ j e. A ( { j } X. C ) <-> <. x , y >. e. `' U_ k e. D ( { k } X. E ) ) )
65 31 32 64 eqrelrdv 
 |-  ( ph -> U_ j e. A ( { j } X. C ) = `' U_ k e. D ( { k } X. E ) )
66 65 f1oeq3d 
 |-  ( ph -> ( ( z e. U_ k e. D ( { k } X. E ) |-> U. `' { z } ) : U_ k e. D ( { k } X. E ) -1-1-onto-> U_ j e. A ( { j } X. C ) <-> ( z e. U_ k e. D ( { k } X. E ) |-> U. `' { z } ) : U_ k e. D ( { k } X. E ) -1-1-onto-> `' U_ k e. D ( { k } X. E ) ) )
67 27 66 mpbiri 
 |-  ( ph -> ( z e. U_ k e. D ( { k } X. E ) |-> U. `' { z } ) : U_ k e. D ( { k } X. E ) -1-1-onto-> U_ j e. A ( { j } X. C ) )
68 1 2 3 16 20 21 67 gsumf1o 
 |-  ( ph -> ( G gsum ( j e. A , k e. C |-> X ) ) = ( G gsum ( ( j e. A , k e. C |-> X ) o. ( z e. U_ k e. D ( { k } X. E ) |-> U. `' { z } ) ) ) )
69 sneq 
 |-  ( z = <. x , y >. -> { z } = { <. x , y >. } )
70 69 cnveqd 
 |-  ( z = <. x , y >. -> `' { z } = `' { <. x , y >. } )
71 70 unieqd 
 |-  ( z = <. x , y >. -> U. `' { z } = U. `' { <. x , y >. } )
72 opswap 
 |-  U. `' { <. x , y >. } = <. y , x >.
73 71 72 eqtrdi 
 |-  ( z = <. x , y >. -> U. `' { z } = <. y , x >. )
74 73 fveq2d 
 |-  ( z = <. x , y >. -> ( ( j e. A , k e. C |-> X ) ` U. `' { z } ) = ( ( j e. A , k e. C |-> X ) ` <. y , x >. ) )
75 df-ov 
 |-  ( y ( j e. A , k e. C |-> X ) x ) = ( ( j e. A , k e. C |-> X ) ` <. y , x >. )
76 74 75 eqtr4di 
 |-  ( z = <. x , y >. -> ( ( j e. A , k e. C |-> X ) ` U. `' { z } ) = ( y ( j e. A , k e. C |-> X ) x ) )
77 76 mpomptx 
 |-  ( z e. U_ x e. D ( { x } X. [_ x / k ]_ E ) |-> ( ( j e. A , k e. C |-> X ) ` U. `' { z } ) ) = ( x e. D , y e. [_ x / k ]_ E |-> ( y ( j e. A , k e. C |-> X ) x ) )
78 nfcv 
 |-  F/_ x ( { k } X. E )
79 nfcv 
 |-  F/_ k { x }
80 nfcsb1v 
 |-  F/_ k [_ x / k ]_ E
81 79 80 nfxp 
 |-  F/_ k ( { x } X. [_ x / k ]_ E )
82 sneq 
 |-  ( k = x -> { k } = { x } )
83 csbeq1a 
 |-  ( k = x -> E = [_ x / k ]_ E )
84 82 83 xpeq12d 
 |-  ( k = x -> ( { k } X. E ) = ( { x } X. [_ x / k ]_ E ) )
85 78 81 84 cbviun 
 |-  U_ k e. D ( { k } X. E ) = U_ x e. D ( { x } X. [_ x / k ]_ E )
86 85 mpteq1i 
 |-  ( z e. U_ k e. D ( { k } X. E ) |-> ( ( j e. A , k e. C |-> X ) ` U. `' { z } ) ) = ( z e. U_ x e. D ( { x } X. [_ x / k ]_ E ) |-> ( ( j e. A , k e. C |-> X ) ` U. `' { z } ) )
87 nfcv 
 |-  F/_ x E
88 nfcv 
 |-  F/_ x ( j ( j e. A , k e. C |-> X ) k )
89 nfcv 
 |-  F/_ y ( j ( j e. A , k e. C |-> X ) k )
90 nfcv 
 |-  F/_ k y
91 nfmpo2 
 |-  F/_ k ( j e. A , k e. C |-> X )
92 nfcv 
 |-  F/_ k x
93 90 91 92 nfov 
 |-  F/_ k ( y ( j e. A , k e. C |-> X ) x )
94 nfcv 
 |-  F/_ j y
95 nfmpo1 
 |-  F/_ j ( j e. A , k e. C |-> X )
96 nfcv 
 |-  F/_ j x
97 94 95 96 nfov 
 |-  F/_ j ( y ( j e. A , k e. C |-> X ) x )
98 oveq2 
 |-  ( k = x -> ( j ( j e. A , k e. C |-> X ) k ) = ( j ( j e. A , k e. C |-> X ) x ) )
99 oveq1 
 |-  ( j = y -> ( j ( j e. A , k e. C |-> X ) x ) = ( y ( j e. A , k e. C |-> X ) x ) )
100 98 99 sylan9eq 
 |-  ( ( k = x /\ j = y ) -> ( j ( j e. A , k e. C |-> X ) k ) = ( y ( j e. A , k e. C |-> X ) x ) )
101 87 80 88 89 93 97 83 100 cbvmpox 
 |-  ( k e. D , j e. E |-> ( j ( j e. A , k e. C |-> X ) k ) ) = ( x e. D , y e. [_ x / k ]_ E |-> ( y ( j e. A , k e. C |-> X ) x ) )
102 77 86 101 3eqtr4i 
 |-  ( z e. U_ k e. D ( { k } X. E ) |-> ( ( j e. A , k e. C |-> X ) ` U. `' { z } ) ) = ( k e. D , j e. E |-> ( j ( j e. A , k e. C |-> X ) k ) )
103 f1of 
 |-  ( ( z e. U_ k e. D ( { k } X. E ) |-> U. `' { z } ) : U_ k e. D ( { k } X. E ) -1-1-onto-> U_ j e. A ( { j } X. C ) -> ( z e. U_ k e. D ( { k } X. E ) |-> U. `' { z } ) : U_ k e. D ( { k } X. E ) --> U_ j e. A ( { j } X. C ) )
104 67 103 syl 
 |-  ( ph -> ( z e. U_ k e. D ( { k } X. E ) |-> U. `' { z } ) : U_ k e. D ( { k } X. E ) --> U_ j e. A ( { j } X. C ) )
105 eqid 
 |-  ( z e. U_ k e. D ( { k } X. E ) |-> U. `' { z } ) = ( z e. U_ k e. D ( { k } X. E ) |-> U. `' { z } )
106 105 fmpt 
 |-  ( A. z e. U_ k e. D ( { k } X. E ) U. `' { z } e. U_ j e. A ( { j } X. C ) <-> ( z e. U_ k e. D ( { k } X. E ) |-> U. `' { z } ) : U_ k e. D ( { k } X. E ) --> U_ j e. A ( { j } X. C ) )
107 104 106 sylibr 
 |-  ( ph -> A. z e. U_ k e. D ( { k } X. E ) U. `' { z } e. U_ j e. A ( { j } X. C ) )
108 eqidd 
 |-  ( ph -> ( z e. U_ k e. D ( { k } X. E ) |-> U. `' { z } ) = ( z e. U_ k e. D ( { k } X. E ) |-> U. `' { z } ) )
109 20 feqmptd 
 |-  ( ph -> ( j e. A , k e. C |-> X ) = ( x e. U_ j e. A ( { j } X. C ) |-> ( ( j e. A , k e. C |-> X ) ` x ) ) )
110 fveq2 
 |-  ( x = U. `' { z } -> ( ( j e. A , k e. C |-> X ) ` x ) = ( ( j e. A , k e. C |-> X ) ` U. `' { z } ) )
111 107 108 109 110 fmptcof 
 |-  ( ph -> ( ( j e. A , k e. C |-> X ) o. ( z e. U_ k e. D ( { k } X. E ) |-> U. `' { z } ) ) = ( z e. U_ k e. D ( { k } X. E ) |-> ( ( j e. A , k e. C |-> X ) ` U. `' { z } ) ) )
112 6 ex 
 |-  ( ph -> ( ( j e. A /\ k e. C ) -> X e. B ) )
113 18 ovmpt4g 
 |-  ( ( j e. A /\ k e. C /\ X e. B ) -> ( j ( j e. A , k e. C |-> X ) k ) = X )
114 113 3expia 
 |-  ( ( j e. A /\ k e. C ) -> ( X e. B -> ( j ( j e. A , k e. C |-> X ) k ) = X ) )
115 112 114 sylcom 
 |-  ( ph -> ( ( j e. A /\ k e. C ) -> ( j ( j e. A , k e. C |-> X ) k ) = X ) )
116 10 115 sylbird 
 |-  ( ph -> ( ( k e. D /\ j e. E ) -> ( j ( j e. A , k e. C |-> X ) k ) = X ) )
117 116 3impib 
 |-  ( ( ph /\ k e. D /\ j e. E ) -> ( j ( j e. A , k e. C |-> X ) k ) = X )
118 117 eqcomd 
 |-  ( ( ph /\ k e. D /\ j e. E ) -> X = ( j ( j e. A , k e. C |-> X ) k ) )
119 118 mpoeq3dva 
 |-  ( ph -> ( k e. D , j e. E |-> X ) = ( k e. D , j e. E |-> ( j ( j e. A , k e. C |-> X ) k ) ) )
120 102 111 119 3eqtr4a 
 |-  ( ph -> ( ( j e. A , k e. C |-> X ) o. ( z e. U_ k e. D ( { k } X. E ) |-> U. `' { z } ) ) = ( k e. D , j e. E |-> X ) )
121 120 oveq2d 
 |-  ( ph -> ( G gsum ( ( j e. A , k e. C |-> X ) o. ( z e. U_ k e. D ( { k } X. E ) |-> U. `' { z } ) ) ) = ( G gsum ( k e. D , j e. E |-> X ) ) )
122 68 121 eqtrd 
 |-  ( ph -> ( G gsum ( j e. A , k e. C |-> X ) ) = ( G gsum ( k e. D , j e. E |-> X ) ) )