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 eqtrid
 |-  ( 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 ) ) ) ) )