Metamath Proof Explorer

Theorem gsumcom3

Description: A commutative law for finitely supported iterated sums. (Contributed by Stefan O'Rear, 2-Nov-2015)

Ref Expression
Hypotheses gsumcom3.b 
|- B = ( Base ` G )
gsumcom3.z 
|- .0. = ( 0g ` G )
gsumcom3.g 
|- ( ph -> G e. CMnd )
gsumcom3.a 
|- ( ph -> A e. V )
gsumcom3.r 
|- ( ph -> C e. W )
gsumcom3.f 
|- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )
gsumcom3.u 
|- ( ph -> U e. Fin )
gsumcom3.n 
|- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) -> X = .0. )
Assertion gsumcom3 
|- ( ph -> ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> X ) ) ) ) = ( G gsum ( k e. C |-> ( G gsum ( j e. A |-> X ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumcom3.b 
 |-  B = ( Base ` G )
2 gsumcom3.z 
 |-  .0. = ( 0g ` G )
3 gsumcom3.g 
 |-  ( ph -> G e. CMnd )
4 gsumcom3.a 
 |-  ( ph -> A e. V )
5 gsumcom3.r 
 |-  ( ph -> C e. W )
6 gsumcom3.f 
 |-  ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )
7 gsumcom3.u 
 |-  ( ph -> U e. Fin )
8 gsumcom3.n 
 |-  ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) -> X = .0. )
9 1 2 3 4 5 6 7 8 gsumcom 
 |-  ( ph -> ( G gsum ( j e. A , k e. C |-> X ) ) = ( G gsum ( k e. C , j e. A |-> X ) ) )
10 5 adantr 
 |-  ( ( ph /\ j e. A ) -> C e. W )
11 1 2 3 4 10 6 7 8 gsum2d2 
 |-  ( ph -> ( G gsum ( j e. A , k e. C |-> X ) ) = ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> X ) ) ) ) )
12 4 adantr 
 |-  ( ( ph /\ k e. C ) -> A e. V )
13 6 ancom2s 
 |-  ( ( ph /\ ( k e. C /\ j e. A ) ) -> X e. B )
14 cnvfi 
 |-  ( U e. Fin -> `' U e. Fin )
15 7 14 syl 
 |-  ( ph -> `' U e. Fin )
16 ancom 
 |-  ( ( k e. C /\ j e. A ) <-> ( j e. A /\ k e. C ) )
17 vex 
 |-  k e. _V
18 vex 
 |-  j e. _V
19 17 18 brcnv 
 |-  ( k `' U j <-> j U k )
20 19 notbii 
 |-  ( -. k `' U j <-> -. j U k )
21 16 20 anbi12i 
 |-  ( ( ( k e. C /\ j e. A ) /\ -. k `' U j ) <-> ( ( j e. A /\ k e. C ) /\ -. j U k ) )
22 21 8 sylan2b 
 |-  ( ( ph /\ ( ( k e. C /\ j e. A ) /\ -. k `' U j ) ) -> X = .0. )
23 1 2 3 5 12 13 15 22 gsum2d2 
 |-  ( ph -> ( G gsum ( k e. C , j e. A |-> X ) ) = ( G gsum ( k e. C |-> ( G gsum ( j e. A |-> X ) ) ) ) )
24 9 11 23 3eqtr3d 
 |-  ( ph -> ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> X ) ) ) ) = ( G gsum ( k e. C |-> ( G gsum ( j e. A |-> X ) ) ) ) )