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 ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
gsumbagdiag.s ⊢ S = y ∈ D | y ≤ f F
gsumbagdiag.f ⊢ φ → F ∈ D
gsumbagdiag.b ⊢ B = Base G
gsumbagdiag.g ⊢ φ → G ∈ CMnd
gsumbagdiag.x ⊢ φ ∧ j ∈ S ∧ k ∈ x ∈ D | x ≤ f F − f j → X ∈ B
Assertion gsumbagdiag ⊢ φ → ∑ G j ∈ S , k ∈ x ∈ D | x ≤ f F − f j ⟼ X = ∑ G k ∈ S , j ∈ x ∈ D | x ≤ f F − f k ⟼ X

Proof

Step Hyp Ref Expression
1 gsumbagdiag.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
2 gsumbagdiag.s ⊢ S = y ∈ D | y ≤ f F
3 gsumbagdiag.f ⊢ φ → F ∈ D
4 gsumbagdiag.b ⊢ B = Base G
5 gsumbagdiag.g ⊢ φ → G ∈ CMnd
6 gsumbagdiag.x ⊢ φ ∧ j ∈ S ∧ k ∈ x ∈ D | x ≤ f F − f j → X ∈ B
7 eqid ⊢ 0 G = 0 G
8 1 psrbaglefi ⊢ F ∈ D → y ∈ D | y ≤ f F ∈ Fin
9 3 8 syl ⊢ φ → y ∈ D | y ≤ f F ∈ Fin
10 2 9 eqeltrid ⊢ φ → S ∈ Fin
11 ovex ⊢ ℕ 0 I ∈ V
12 1 11 rab2ex ⊢ x ∈ D | x ≤ f F − f j ∈ V
13 12 a1i ⊢ φ ∧ j ∈ S → x ∈ D | x ≤ f F − f j ∈ V
14 xpfi ⊢ S ∈ Fin ∧ S ∈ Fin → S × S ∈ Fin
15 10 10 14 syl2anc ⊢ φ → S × S ∈ Fin
16 simprl ⊢ φ ∧ j ∈ S ∧ k ∈ x ∈ D | x ≤ f F − f j → j ∈ S
17 1 2 3 gsumbagdiaglem ⊢ φ ∧ j ∈ S ∧ k ∈ x ∈ D | x ≤ f F − f j → k ∈ S ∧ j ∈ x ∈ D | x ≤ f F − f k
18 17 simpld ⊢ φ ∧ j ∈ S ∧ k ∈ x ∈ D | x ≤ f F − f j → k ∈ S
19 brxp ⊢ j S × S k ↔ j ∈ S ∧ k ∈ S
20 16 18 19 sylanbrc ⊢ φ ∧ j ∈ S ∧ k ∈ x ∈ D | x ≤ f F − f j → j S × S k
21 20 pm2.24d ⊢ φ ∧ j ∈ S ∧ k ∈ x ∈ D | x ≤ f F − f j → ¬ j S × S k → X = 0 G
22 21 impr ⊢ φ ∧ j ∈ S ∧ k ∈ x ∈ D | x ≤ f F − f j ∧ ¬ j S × S k → X = 0 G
23 1 2 3 gsumbagdiaglem ⊢ φ ∧ k ∈ S ∧ j ∈ x ∈ D | x ≤ f F − f k → j ∈ S ∧ k ∈ x ∈ D | x ≤ f F − f j
24 17 23 impbida ⊢ φ → j ∈ S ∧ k ∈ x ∈ D | x ≤ f F − f j ↔ k ∈ S ∧ j ∈ x ∈ D | x ≤ f F − f k
25 4 7 5 10 13 6 15 22 10 24 gsumcom2 ⊢ φ → ∑ G j ∈ S , k ∈ x ∈ D | x ≤ f F − f j ⟼ X = ∑ G k ∈ S , j ∈ x ∈ D | x ≤ f F − f k ⟼ X