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

Metamath Proof Explorer

Theorem gsumcom

Description: Commute the arguments of a double sum. (Contributed by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses gsumxp.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumxp.z ⊢ 0 = ( 0g ‘ 𝐺 )
gsumxp.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsumxp.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsumxp.r ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
gsumcom.f ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) → 𝑋 ∈ 𝐵 )
gsumcom.u ⊢ ( 𝜑 → 𝑈 ∈ Fin )
gsumcom.n ⊢ ( ( 𝜑 ∧ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ∧ ¬ 𝑗 𝑈 𝑘 ) ) → 𝑋 = 0 )
Assertion gsumcom ( 𝜑 → ( 𝐺 Σg ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐶 , 𝑗 ∈ 𝐴 ↦ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 gsumxp.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumxp.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsumxp.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 gsumxp.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5 gsumxp.r ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
6 gsumcom.f ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) → 𝑋 ∈ 𝐵 )
7 gsumcom.u ⊢ ( 𝜑 → 𝑈 ∈ Fin )
8 gsumcom.n ⊢ ( ( 𝜑 ∧ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ∧ ¬ 𝑗 𝑈 𝑘 ) ) → 𝑋 = 0 )
9 5 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐶 ∈ 𝑊 )
10 ancom ⊢ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ↔ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐴 ) )
11 10 a1i ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ↔ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐴 ) ) )
12 1 2 3 4 9 6 7 8 5 11 gsumcom2 ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐶 , 𝑗 ∈ 𝐴 ↦ 𝑋 ) ) )