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