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 𝐵 = ( Base ‘ 𝐺 )
gsumcom3fi.g ( 𝜑𝐺 ∈ CMnd )
gsumcom3fi.a ( 𝜑𝐴 ∈ Fin )
gsumcom3fi.r ( 𝜑𝐶 ∈ Fin )
gsumcom3fi.f ( ( 𝜑 ∧ ( 𝑗𝐴𝑘𝐶 ) ) → 𝑋𝐵 )
Assertion gsumcom3fi ( 𝜑 → ( 𝐺 Σg ( 𝑗𝐴 ↦ ( 𝐺 Σg ( 𝑘𝐶𝑋 ) ) ) ) = ( 𝐺 Σg ( 𝑘𝐶 ↦ ( 𝐺 Σg ( 𝑗𝐴𝑋 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumcom3fi.b 𝐵 = ( Base ‘ 𝐺 )
2 gsumcom3fi.g ( 𝜑𝐺 ∈ CMnd )
3 gsumcom3fi.a ( 𝜑𝐴 ∈ Fin )
4 gsumcom3fi.r ( 𝜑𝐶 ∈ Fin )
5 gsumcom3fi.f ( ( 𝜑 ∧ ( 𝑗𝐴𝑘𝐶 ) ) → 𝑋𝐵 )
6 eqid ( 0g𝐺 ) = ( 0g𝐺 )
7 xpfi ( ( 𝐴 ∈ Fin ∧ 𝐶 ∈ Fin ) → ( 𝐴 × 𝐶 ) ∈ Fin )
8 3 4 7 syl2anc ( 𝜑 → ( 𝐴 × 𝐶 ) ∈ Fin )
9 brxp ( 𝑗 ( 𝐴 × 𝐶 ) 𝑘 ↔ ( 𝑗𝐴𝑘𝐶 ) )
10 9 biimpri ( ( 𝑗𝐴𝑘𝐶 ) → 𝑗 ( 𝐴 × 𝐶 ) 𝑘 )
11 10 adantl ( ( 𝜑 ∧ ( 𝑗𝐴𝑘𝐶 ) ) → 𝑗 ( 𝐴 × 𝐶 ) 𝑘 )
12 11 pm2.24d ( ( 𝜑 ∧ ( 𝑗𝐴𝑘𝐶 ) ) → ( ¬ 𝑗 ( 𝐴 × 𝐶 ) 𝑘𝑋 = ( 0g𝐺 ) ) )
13 12 impr ( ( 𝜑 ∧ ( ( 𝑗𝐴𝑘𝐶 ) ∧ ¬ 𝑗 ( 𝐴 × 𝐶 ) 𝑘 ) ) → 𝑋 = ( 0g𝐺 ) )
14 1 6 2 3 4 5 8 13 gsumcom3 ( 𝜑 → ( 𝐺 Σg ( 𝑗𝐴 ↦ ( 𝐺 Σg ( 𝑘𝐶𝑋 ) ) ) ) = ( 𝐺 Σg ( 𝑘𝐶 ↦ ( 𝐺 Σg ( 𝑗𝐴𝑋 ) ) ) ) )