Theorem gsumbagdiag

Description: Two-dimensional commutation of a group sum over a "triangular" region. fsum0diag analogue for finite bags. (Contributed by Mario Carneiro, 5-Jan-2015)

	Ref	Expression
Hypotheses	psrbag.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	psrbagconf1o.1	⊢ 𝑆 = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 }
	gsumbagdiag.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	gsumbagdiag.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
	gsumbagdiag.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumbagdiag.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsumbagdiag.x	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → 𝑋 ∈ 𝐵 )
Assertion	gsumbagdiag	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑗 ∈ 𝑆 , 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑆 , 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑘 ) } ↦ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2		psrbagconf1o.1	⊢ 𝑆 = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 }
3		gsumbagdiag.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4		gsumbagdiag.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
5		gsumbagdiag.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
6		gsumbagdiag.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
7		gsumbagdiag.x	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → 𝑋 ∈ 𝐵 )
8		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
9	1	psrbaglefi	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 } ∈ Fin )
10	3 4 9	syl2anc	⊢ ( 𝜑 → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 } ∈ Fin )
11	2 10	eqeltrid	⊢ ( 𝜑 → 𝑆 ∈ Fin )
12		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
13	1 12	rab2ex	⊢ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ∈ V
14	13	a1i	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ∈ V )
15		xpfi	⊢ ( ( 𝑆 ∈ Fin ∧ 𝑆 ∈ Fin ) → ( 𝑆 × 𝑆 ) ∈ Fin )
16	11 11 15	syl2anc	⊢ ( 𝜑 → ( 𝑆 × 𝑆 ) ∈ Fin )
17		simprl	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → 𝑗 ∈ 𝑆 )
18	1 2 3 4	gsumbagdiaglem	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → ( 𝑘 ∈ 𝑆 ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑘 ) } ) )
19	18	simpld	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → 𝑘 ∈ 𝑆 )
20		brxp	⊢ ( 𝑗 ( 𝑆 × 𝑆 ) 𝑘 ↔ ( 𝑗 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) )
21	17 19 20	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → 𝑗 ( 𝑆 × 𝑆 ) 𝑘 )
22	21	pm2.24d	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → ( ¬ 𝑗 ( 𝑆 × 𝑆 ) 𝑘 → 𝑋 = ( 0g ‘ 𝐺 ) ) )
23	22	impr	⊢ ( ( 𝜑 ∧ ( ( 𝑗 ∈ 𝑆 ∧ 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ∧ ¬ 𝑗 ( 𝑆 × 𝑆 ) 𝑘 ) ) → 𝑋 = ( 0g ‘ 𝐺 ) )
24	1 2 3 4	gsumbagdiaglem	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑘 ) } ) ) → ( 𝑗 ∈ 𝑆 ∧ 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) )
25	18 24	impbida	⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝑆 ∧ 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ↔ ( 𝑘 ∈ 𝑆 ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑘 ) } ) ) )
26	5 8 6 11 14 7 16 23 11 25	gsumcom2	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑗 ∈ 𝑆 , 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑆 , 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑘 ) } ↦ 𝑋 ) ) )