# 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)

Ref Expression
Hypotheses psrbag.d ${⊢}{D}=\left\{{f}\in \left({{ℕ}_{0}}^{{I}}\right)|{{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
psrbagconf1o.1 ${⊢}{S}=\left\{{y}\in {D}|{y}{\le }_{f}{F}\right\}$
gsumbagdiag.i ${⊢}{\phi }\to {I}\in {V}$
gsumbagdiag.f ${⊢}{\phi }\to {F}\in {D}$
gsumbagdiag.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
gsumbagdiag.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
gsumbagdiag.x ${⊢}\left({\phi }\wedge \left({j}\in {S}\wedge {k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\right)\to {X}\in {B}$
Assertion gsumbagdiag ${⊢}{\phi }\to {\sum }_{{G}}\left({j}\in {S},{k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)={\sum }_{{G}}\left({k}\in {S},{j}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{k}\right)\right\}⟼{X}\right)$

### Proof

Step Hyp Ref Expression
1 psrbag.d ${⊢}{D}=\left\{{f}\in \left({{ℕ}_{0}}^{{I}}\right)|{{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
2 psrbagconf1o.1 ${⊢}{S}=\left\{{y}\in {D}|{y}{\le }_{f}{F}\right\}$
3 gsumbagdiag.i ${⊢}{\phi }\to {I}\in {V}$
4 gsumbagdiag.f ${⊢}{\phi }\to {F}\in {D}$
5 gsumbagdiag.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
6 gsumbagdiag.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
7 gsumbagdiag.x ${⊢}\left({\phi }\wedge \left({j}\in {S}\wedge {k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\right)\to {X}\in {B}$
8 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
9 1 psrbaglefi ${⊢}\left({I}\in {V}\wedge {F}\in {D}\right)\to \left\{{y}\in {D}|{y}{\le }_{f}{F}\right\}\in \mathrm{Fin}$
10 3 4 9 syl2anc ${⊢}{\phi }\to \left\{{y}\in {D}|{y}{\le }_{f}{F}\right\}\in \mathrm{Fin}$
11 2 10 eqeltrid ${⊢}{\phi }\to {S}\in \mathrm{Fin}$
12 ovex ${⊢}{{ℕ}_{0}}^{{I}}\in \mathrm{V}$
13 1 12 rab2ex ${⊢}\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\in \mathrm{V}$
14 13 a1i ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\in \mathrm{V}$
15 xpfi ${⊢}\left({S}\in \mathrm{Fin}\wedge {S}\in \mathrm{Fin}\right)\to {S}×{S}\in \mathrm{Fin}$
16 11 11 15 syl2anc ${⊢}{\phi }\to {S}×{S}\in \mathrm{Fin}$
17 simprl ${⊢}\left({\phi }\wedge \left({j}\in {S}\wedge {k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\right)\to {j}\in {S}$
18 1 2 3 4 gsumbagdiaglem ${⊢}\left({\phi }\wedge \left({j}\in {S}\wedge {k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\right)\to \left({k}\in {S}\wedge {j}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{k}\right)\right\}\right)$
19 18 simpld ${⊢}\left({\phi }\wedge \left({j}\in {S}\wedge {k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\right)\to {k}\in {S}$
20 brxp ${⊢}{j}\left({S}×{S}\right){k}↔\left({j}\in {S}\wedge {k}\in {S}\right)$
21 17 19 20 sylanbrc ${⊢}\left({\phi }\wedge \left({j}\in {S}\wedge {k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\right)\to {j}\left({S}×{S}\right){k}$
22 21 pm2.24d ${⊢}\left({\phi }\wedge \left({j}\in {S}\wedge {k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\right)\to \left(¬{j}\left({S}×{S}\right){k}\to {X}={0}_{{G}}\right)$
23 22 impr ${⊢}\left({\phi }\wedge \left(\left({j}\in {S}\wedge {k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\wedge ¬{j}\left({S}×{S}\right){k}\right)\right)\to {X}={0}_{{G}}$
24 1 2 3 4 gsumbagdiaglem ${⊢}\left({\phi }\wedge \left({k}\in {S}\wedge {j}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{k}\right)\right\}\right)\right)\to \left({j}\in {S}\wedge {k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)$
25 18 24 impbida ${⊢}{\phi }\to \left(\left({j}\in {S}\wedge {k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)↔\left({k}\in {S}\wedge {j}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{k}\right)\right\}\right)\right)$
26 5 8 6 11 14 7 16 23 11 25 gsumcom2 ${⊢}{\phi }\to {\sum }_{{G}}\left({j}\in {S},{k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)={\sum }_{{G}}\left({k}\in {S},{j}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{k}\right)\right\}⟼{X}\right)$