This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gsumcom3fi

Description: A commutative law for finite iterated sums. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses gsumcom3fi.b 
|- B = ( Base ` G )
gsumcom3fi.g 
|- ( ph -> G e. CMnd )
gsumcom3fi.a 
|- ( ph -> A e. Fin )
gsumcom3fi.r 
|- ( ph -> C e. Fin )
gsumcom3fi.f 
|- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )
Assertion gsumcom3fi 
|- ( 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 gsumcom3fi.b 
 |-  B = ( Base ` G )
2 gsumcom3fi.g 
 |-  ( ph -> G e. CMnd )
3 gsumcom3fi.a 
 |-  ( ph -> A e. Fin )
4 gsumcom3fi.r 
 |-  ( ph -> C e. Fin )
5 gsumcom3fi.f 
 |-  ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )
6 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
7 xpfi 
 |-  ( ( A e. Fin /\ C e. Fin ) -> ( A X. C ) e. Fin )
8 3 4 7 syl2anc 
 |-  ( ph -> ( A X. C ) e. Fin )
9 brxp 
 |-  ( j ( A X. C ) k <-> ( j e. A /\ k e. C ) )
10 9 biimpri 
 |-  ( ( j e. A /\ k e. C ) -> j ( A X. C ) k )
11 10 adantl 
 |-  ( ( ph /\ ( j e. A /\ k e. C ) ) -> j ( A X. C ) k )
12 11 pm2.24d 
 |-  ( ( ph /\ ( j e. A /\ k e. C ) ) -> ( -. j ( A X. C ) k -> X = ( 0g ` G ) ) )
13 12 impr 
 |-  ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j ( A X. C ) k ) ) -> X = ( 0g ` G ) )
14 1 6 2 3 4 5 8 13 gsumcom3 
 |-  ( ph -> ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> X ) ) ) ) = ( G gsum ( k e. C |-> ( G gsum ( j e. A |-> X ) ) ) ) )