Metamath Proof Explorer

Theorem gsum2d2

Description: Write a group sum over a two-dimensional region as a double sum. Note that C ( j ) is a function of j . (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. )
Assertion gsum2d2 
|- ( ph -> ( G gsum ( j e. A , k e. C |-> X ) ) = ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> 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 snex 
 |-  { j } e. _V
10 xpexg 
 |-  ( ( { j } e. _V /\ C e. W ) -> ( { j } X. C ) e. _V )
11 9 5 10 sylancr 
 |-  ( ( ph /\ j e. A ) -> ( { j } X. C ) e. _V )
12 11 ralrimiva 
 |-  ( ph -> A. j e. A ( { j } X. C ) e. _V )
13 iunexg 
 |-  ( ( A e. V /\ A. j e. A ( { j } X. C ) e. _V ) -> U_ j e. A ( { j } X. C ) e. _V )
14 4 12 13 syl2anc 
 |-  ( ph -> U_ j e. A ( { j } X. C ) e. _V )
15 relxp 
 |-  Rel ( { j } X. C )
16 15 rgenw 
 |-  A. j e. A Rel ( { j } X. C )
17 reliun 
 |-  ( Rel U_ j e. A ( { j } X. C ) <-> A. j e. A Rel ( { j } X. C ) )
18 16 17 mpbir 
 |-  Rel U_ j e. A ( { j } X. C )
19 18 a1i 
 |-  ( ph -> Rel U_ j e. A ( { j } X. C ) )
20 vex 
 |-  x e. _V
21 20 eldm2 
 |-  ( x e. dom U_ j e. A ( { j } X. C ) <-> E. y <. x , y >. e. U_ j e. A ( { j } X. C ) )
22 eliunxp 
 |-  ( <. x , y >. e. U_ j e. A ( { j } X. C ) <-> E. j E. k ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) )
23 vex 
 |-  y e. _V
24 20 23 opth1 
 |-  ( <. x , y >. = <. j , k >. -> x = j )
25 24 ad2antrl 
 |-  ( ( ph /\ ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) ) -> x = j )
26 simprrl 
 |-  ( ( ph /\ ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) ) -> j e. A )
27 25 26 eqeltrd 
 |-  ( ( ph /\ ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) ) -> x e. A )
28 27 ex 
 |-  ( ph -> ( ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) -> x e. A ) )
29 28 exlimdvv 
 |-  ( ph -> ( E. j E. k ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) -> x e. A ) )
30 22 29 syl5bi 
 |-  ( ph -> ( <. x , y >. e. U_ j e. A ( { j } X. C ) -> x e. A ) )
31 30 exlimdv 
 |-  ( ph -> ( E. y <. x , y >. e. U_ j e. A ( { j } X. C ) -> x e. A ) )
32 21 31 syl5bi 
 |-  ( ph -> ( x e. dom U_ j e. A ( { j } X. C ) -> x e. A ) )
33 32 ssrdv 
 |-  ( ph -> dom U_ j e. A ( { j } X. C ) C_ A )
34 6 ralrimivva 
 |-  ( ph -> A. j e. A A. k e. C X e. B )
35 eqid 
 |-  ( j e. A , k e. C |-> X ) = ( j e. A , k e. C |-> X )
36 35 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 )
37 34 36 sylib 
 |-  ( ph -> ( j e. A , k e. C |-> X ) : U_ j e. A ( { j } X. C ) --> B )
38 1 2 3 4 5 6 7 8 gsum2d2lem 
 |-  ( ph -> ( j e. A , k e. C |-> X ) finSupp .0. )
39 1 2 3 14 19 4 33 37 38 gsum2d 
 |-  ( ph -> ( G gsum ( j e. A , k e. C |-> X ) ) = ( G gsum ( m e. A |-> ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) ) ) ) )
40 nfcv 
 |-  F/_ j G
41 nfcv 
 |-  F/_ j gsum
42 nfiu1 
 |-  F/_ j U_ j e. A ( { j } X. C )
43 nfcv 
 |-  F/_ j { m }
44 42 43 nfima 
 |-  F/_ j ( U_ j e. A ( { j } X. C ) " { m } )
45 nfcv 
 |-  F/_ j m
46 nfmpo1 
 |-  F/_ j ( j e. A , k e. C |-> X )
47 nfcv 
 |-  F/_ j n
48 45 46 47 nfov 
 |-  F/_ j ( m ( j e. A , k e. C |-> X ) n )
49 44 48 nfmpt 
 |-  F/_ j ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) )
50 40 41 49 nfov 
 |-  F/_ j ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) )
51 nfcv 
 |-  F/_ m ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) )
52 sneq 
 |-  ( m = j -> { m } = { j } )
53 52 imaeq2d 
 |-  ( m = j -> ( U_ j e. A ( { j } X. C ) " { m } ) = ( U_ j e. A ( { j } X. C ) " { j } ) )
54 oveq1 
 |-  ( m = j -> ( m ( j e. A , k e. C |-> X ) n ) = ( j ( j e. A , k e. C |-> X ) n ) )
55 53 54 mpteq12dv 
 |-  ( m = j -> ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) = ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) )
56 55 oveq2d 
 |-  ( m = j -> ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) ) = ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) ) )
57 50 51 56 cbvmpt 
 |-  ( m e. A |-> ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) ) ) = ( j e. A |-> ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) ) )
58 vex 
 |-  j e. _V
59 vex 
 |-  k e. _V
60 58 59 elimasn 
 |-  ( k e. ( U_ j e. A ( { j } X. C ) " { j } ) <-> <. j , k >. e. U_ j e. A ( { j } X. C ) )
61 opeliunxp 
 |-  ( <. j , k >. e. U_ j e. A ( { j } X. C ) <-> ( j e. A /\ k e. C ) )
62 60 61 bitri 
 |-  ( k e. ( U_ j e. A ( { j } X. C ) " { j } ) <-> ( j e. A /\ k e. C ) )
63 62 baib 
 |-  ( j e. A -> ( k e. ( U_ j e. A ( { j } X. C ) " { j } ) <-> k e. C ) )
64 63 eqrdv 
 |-  ( j e. A -> ( U_ j e. A ( { j } X. C ) " { j } ) = C )
65 64 mpteq1d 
 |-  ( j e. A -> ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) = ( n e. C |-> ( j ( j e. A , k e. C |-> X ) n ) ) )
66 nfcv 
 |-  F/_ k j
67 nfmpo2 
 |-  F/_ k ( j e. A , k e. C |-> X )
68 nfcv 
 |-  F/_ k n
69 66 67 68 nfov 
 |-  F/_ k ( j ( j e. A , k e. C |-> X ) n )
70 nfcv 
 |-  F/_ n ( j ( j e. A , k e. C |-> X ) k )
71 oveq2 
 |-  ( n = k -> ( j ( j e. A , k e. C |-> X ) n ) = ( j ( j e. A , k e. C |-> X ) k ) )
72 69 70 71 cbvmpt 
 |-  ( n e. C |-> ( j ( j e. A , k e. C |-> X ) n ) ) = ( k e. C |-> ( j ( j e. A , k e. C |-> X ) k ) )
73 65 72 eqtrdi 
 |-  ( j e. A -> ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) = ( k e. C |-> ( j ( j e. A , k e. C |-> X ) k ) ) )
74 73 adantl 
 |-  ( ( ph /\ j e. A ) -> ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) = ( k e. C |-> ( j ( j e. A , k e. C |-> X ) k ) ) )
75 simprl 
 |-  ( ( ph /\ ( j e. A /\ k e. C ) ) -> j e. A )
76 simprr 
 |-  ( ( ph /\ ( j e. A /\ k e. C ) ) -> k e. C )
77 35 ovmpt4g 
 |-  ( ( j e. A /\ k e. C /\ X e. B ) -> ( j ( j e. A , k e. C |-> X ) k ) = X )
78 75 76 6 77 syl3anc 
 |-  ( ( ph /\ ( j e. A /\ k e. C ) ) -> ( j ( j e. A , k e. C |-> X ) k ) = X )
79 78 anassrs 
 |-  ( ( ( ph /\ j e. A ) /\ k e. C ) -> ( j ( j e. A , k e. C |-> X ) k ) = X )
80 79 mpteq2dva 
 |-  ( ( ph /\ j e. A ) -> ( k e. C |-> ( j ( j e. A , k e. C |-> X ) k ) ) = ( k e. C |-> X ) )
81 74 80 eqtrd 
 |-  ( ( ph /\ j e. A ) -> ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) = ( k e. C |-> X ) )
82 81 oveq2d 
 |-  ( ( ph /\ j e. A ) -> ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) ) = ( G gsum ( k e. C |-> X ) ) )
83 82 mpteq2dva 
 |-  ( ph -> ( j e. A |-> ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) ) ) = ( j e. A |-> ( G gsum ( k e. C |-> X ) ) ) )
84 57 83 syl5eq 
 |-  ( ph -> ( m e. A |-> ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) ) ) = ( j e. A |-> ( G gsum ( k e. C |-> X ) ) ) )
85 84 oveq2d 
 |-  ( ph -> ( G gsum ( m e. A |-> ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) ) ) ) = ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> X ) ) ) ) )
86 39 85 eqtrd 
 |-  ( ph -> ( G gsum ( j e. A , k e. C |-> X ) ) = ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> X ) ) ) ) )