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 \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	gsumbagdiag.s	$⊢ S = \{y \in D \| y \leq_{f} F\}$
	gsumbagdiag.f	$⊢ φ \to F \in D$
	gsumbagdiag.b	$⊢ B = {Base}_{G}$
	gsumbagdiag.g	$⊢ φ \to G \in CMnd$
	gsumbagdiag.x	$⊢ (φ \land (j \in S \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to X \in B$
Assertion	gsumbagdiag	$⊢ φ \to \sum_{G} (j \in S, k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) = \sum_{G} (k \in S, j \in \{x \in D \| x \leq_{f} (F -_{f} k)\} ⟼ X)$

Proof

Step	Hyp	Ref	Expression
1		gsumbagdiag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
2		gsumbagdiag.s	$⊢ S = \{y \in D \| y \leq_{f} F\}$
3		gsumbagdiag.f	$⊢ φ \to F \in D$
4		gsumbagdiag.b	$⊢ B = {Base}_{G}$
5		gsumbagdiag.g	$⊢ φ \to G \in CMnd$
6		gsumbagdiag.x	$⊢ (φ \land (j \in S \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to X \in B$
7		eqid	$⊢ 0_{G} = 0_{G}$
8	1	psrbaglefi	$⊢ F \in D \to \{y \in D \| y \leq_{f} F\} \in Fin$
9	3 8	syl	$⊢ φ \to \{y \in D \| y \leq_{f} F\} \in Fin$
10	2 9	eqeltrid	$⊢ φ \to S \in Fin$
11		ovex	$⊢ {ℕ_{0}}^{I} \in V$
12	1 11	rab2ex	$⊢ \{x \in D \| x \leq_{f} (F -_{f} j)\} \in V$
13	12	a1i	$⊢ (φ \land j \in S) \to \{x \in D \| x \leq_{f} (F -_{f} j)\} \in V$
14		xpfi	$⊢ (S \in Fin \land S \in Fin) \to S \times S \in Fin$
15	10 10 14	syl2anc	$⊢ φ \to S \times S \in Fin$
16		simprl	$⊢ (φ \land (j \in S \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to j \in S$
17	1 2 3	gsumbagdiaglem	$⊢ (φ \land (j \in S \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to (k \in S \land j \in \{x \in D \| x \leq_{f} (F -_{f} k)\})$
18	17	simpld	$⊢ (φ \land (j \in S \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to k \in S$
19		brxp	$⊢ j (S \times S) k \leftrightarrow (j \in S \land k \in S)$
20	16 18 19	sylanbrc	$⊢ (φ \land (j \in S \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to j (S \times S) k$
21	20	pm2.24d	$⊢ (φ \land (j \in S \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to (\neg j (S \times S) k \to X = 0_{G})$
22	21	impr	$⊢ (φ \land ((j \in S \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \land \neg j (S \times S) k)) \to X = 0_{G}$
23	1 2 3	gsumbagdiaglem	$⊢ (φ \land (k \in S \land j \in \{x \in D \| x \leq_{f} (F -_{f} k)\})) \to (j \in S \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\})$
24	17 23	impbida	$⊢ φ \to ((j \in S \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \leftrightarrow (k \in S \land j \in \{x \in D \| x \leq_{f} (F -_{f} k)\}))$
25	4 7 5 10 13 6 15 22 10 24	gsumcom2	$⊢ φ \to \sum_{G} (j \in S, k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) = \sum_{G} (k \in S, j \in \{x \in D \| x \leq_{f} (F -_{f} k)\} ⟼ X)$

Metamath Proof Explorer

Theorem gsumbagdiag

Proof