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