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) Remove a sethood hypothesis. (Revised by SN, 6-Aug-2024)

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