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 ⊢ 𝐵 = ( 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 ( 𝑗 ∈ 𝐴 ↦ 𝑋 ) ) ) ) )