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 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ 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 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ 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 ( ℕ0m 𝐼 ) ∈ 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𝑘 ) } ↦ 𝑋 ) ) )