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

Metamath Proof Explorer

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 − 𝑘 ) } ↦ 𝑋 ) ) )