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 ˙ = 0 G
gsum2d2.g φ G CMnd
gsum2d2.a φ A V
gsum2d2.r φ j A C W
gsum2d2.f φ j A k C X B
gsum2d2.u φ U Fin
gsum2d2.n φ j A k C ¬ j U k X = 0 ˙
gsumcom2.d φ D Y
gsumcom2.c φ j A k C k D j E
Assertion gsumcom2 φ G j A , k C X = G k D , j E X

Proof

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