gsumcom3

Description: A commutative law for finitely supported iterated sums. (Contributed by Stefan O'Rear, 2-Nov-2015)

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

Proof

Step	Hyp	Ref	Expression
1		gsumcom3.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumcom3.z	⊢ 0 = ( 0_g ‘ 𝐺 )
3		gsumcom3.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		gsumcom3.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5		gsumcom3.r	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
6		gsumcom3.f	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) → 𝑋 ∈ 𝐵 )
7		gsumcom3.u	⊢ ( 𝜑 → 𝑈 ∈ Fin )
8		gsumcom3.n	⊢ ( ( 𝜑 ∧ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ∧ ¬ 𝑗 𝑈 𝑘 ) ) → 𝑋 = 0 )
9	1 2 3 4 5 6 7 8	gsumcom	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) = ( 𝐺 Σ_g ( 𝑘 ∈ 𝐶 , 𝑗 ∈ 𝐴 ↦ 𝑋 ) ) )
10	5	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐶 ∈ 𝑊 )
11	1 2 3 4 10 6 7 8	gsum2d2	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) = ( 𝐺 Σ_g ( 𝑗 ∈ 𝐴 ↦ ( 𝐺 Σ_g ( 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) ) ) )
12	4	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → 𝐴 ∈ 𝑉 )
13	6	ancom2s	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐴 ) ) → 𝑋 ∈ 𝐵 )
14		cnvfi	⊢ ( 𝑈 ∈ Fin → ^◡ 𝑈 ∈ Fin )
15	7 14	syl	⊢ ( 𝜑 → ^◡ 𝑈 ∈ Fin )
16		ancom	⊢ ( ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐴 ) ↔ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) )
17		vex	⊢ 𝑘 ∈ V
18		vex	⊢ 𝑗 ∈ V
19	17 18	brcnv	⊢ ( 𝑘 ^◡ 𝑈 𝑗 ↔ 𝑗 𝑈 𝑘 )
20	19	notbii	⊢ ( ¬ 𝑘 ^◡ 𝑈 𝑗 ↔ ¬ 𝑗 𝑈 𝑘 )
21	16 20	anbi12i	⊢ ( ( ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐴 ) ∧ ¬ 𝑘 ^◡ 𝑈 𝑗 ) ↔ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ∧ ¬ 𝑗 𝑈 𝑘 ) )
22	21 8	sylan2b	⊢ ( ( 𝜑 ∧ ( ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐴 ) ∧ ¬ 𝑘 ^◡ 𝑈 𝑗 ) ) → 𝑋 = 0 )
23	1 2 3 5 12 13 15 22	gsum2d2	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑘 ∈ 𝐶 , 𝑗 ∈ 𝐴 ↦ 𝑋 ) ) = ( 𝐺 Σ_g ( 𝑘 ∈ 𝐶 ↦ ( 𝐺 Σ_g ( 𝑗 ∈ 𝐴 ↦ 𝑋 ) ) ) ) )
24	9 11 23	3eqtr3d	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑗 ∈ 𝐴 ↦ ( 𝐺 Σ_g ( 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) ) ) = ( 𝐺 Σ_g ( 𝑘 ∈ 𝐶 ↦ ( 𝐺 Σ_g ( 𝑗 ∈ 𝐴 ↦ 𝑋 ) ) ) ) )

Metamath Proof Explorer

Theorem gsumcom3

Proof