gsumbagdiagOLD

Description: Obsolete version of gsumbagdiag as of 6-Aug-2024. (Contributed by Mario Carneiro, 5-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	psrbagconf1o.s	$⊢ S = \{y \in D \| y \leq_{f} F\}$
	gsumbagdiagOLD.i	$⊢ φ \to I \in V$
	gsumbagdiagOLD.f	$⊢ φ \to F \in D$
	gsumbagdiagOLD.b	$⊢ B = {Base}_{G}$
	gsumbagdiagOLD.g	$⊢ φ \to G \in CMnd$
	gsumbagdiagOLD.x	$⊢ (φ \land (j \in S \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to X \in B$
Assertion	gsumbagdiagOLD	$⊢ φ \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		psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
2		psrbagconf1o.s	$⊢ S = \{y \in D \| y \leq_{f} F\}$
3		gsumbagdiagOLD.i	$⊢ φ \to I \in V$
4		gsumbagdiagOLD.f	$⊢ φ \to F \in D$
5		gsumbagdiagOLD.b	$⊢ B = {Base}_{G}$
6		gsumbagdiagOLD.g	$⊢ φ \to G \in CMnd$
7		gsumbagdiagOLD.x	$⊢ (φ \land (j \in S \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to X \in B$
8		eqid	$⊢ 0_{G} = 0_{G}$
9	1	psrbaglefiOLD	$⊢ (I \in V \land F \in D) \to \{y \in D \| y \leq_{f} F\} \in Fin$
10	3 4 9	syl2anc	$⊢ φ \to \{y \in D \| y \leq_{f} F\} \in Fin$
11	2 10	eqeltrid	$⊢ φ \to S \in Fin$
12		ovex	$⊢ {ℕ_{0}}^{I} \in V$
13	1 12	rab2ex	$⊢ \{x \in D \| x \leq_{f} (F -_{f} j)\} \in V$
14	13	a1i	$⊢ (φ \land j \in S) \to \{x \in D \| x \leq_{f} (F -_{f} j)\} \in V$
15		xpfi	$⊢ (S \in Fin \land S \in Fin) \to S \times S \in Fin$
16	11 11 15	syl2anc	$⊢ φ \to S \times S \in Fin$
17		simprl	$⊢ (φ \land (j \in S \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to j \in S$
18	1 2 3 4	gsumbagdiaglemOLD	$⊢ (φ \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)\})$
19	18	simpld	$⊢ (φ \land (j \in S \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to k \in S$
20		brxp	$⊢ j (S \times S) k \leftrightarrow (j \in S \land k \in S)$
21	17 19 20	sylanbrc	$⊢ (φ \land (j \in S \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to j (S \times S) k$
22	21	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})$
23	22	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}$
24	1 2 3 4	gsumbagdiaglemOLD	$⊢ (φ \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)\})$
25	18 24	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)\}))$
26	5 8 6 11 14 7 16 23 11 25	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 gsumbagdiagOLD

Proof