psrass1lem

Description: A group sum commutation used by psrass1 . (Contributed by Mario Carneiro, 5-Jan-2015) Remove a sethood hypothesis. (Revised by SN, 7-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$
	psrass1lem.y	$⊢ k = n -_{f} j \to X = Y$
Assertion	psrass1lem	$⊢ φ \to \underset{n \in S}{\sum_{G}} (\underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}}, Y) = \underset{j \in S}{\sum_{G}} (\underset{k \in \{x \in D \| x \leq_{f} (F -_{f} j)\}}{\sum_{G}}, 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		psrass1lem.y	$⊢ k = n -_{f} j \to X = Y$
8	1 2 3	gsumbagdiaglem	$⊢ (φ \land (m \in S \land j \in \{x \in D \| x \leq_{f} (F -_{f} m)\})) \to (j \in S \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\})$
9	6	anassrs	$⊢ ((φ \land j \in S) \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to X \in B$
10	9	fmpttd	$⊢ (φ \land j \in S) \to (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) : \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟶ B$
11	2	ssrab3	$⊢ S \subseteq D$
12	1 2	psrbagconcl	$⊢ (F \in D \land j \in S) \to F -_{f} j \in S$
13	3 12	sylan	$⊢ (φ \land j \in S) \to F -_{f} j \in S$
14	11 13	sselid	$⊢ (φ \land j \in S) \to F -_{f} j \in D$
15		eqid	$⊢ \{x \in D \| x \leq_{f} (F -_{f} j)\} = \{x \in D \| x \leq_{f} (F -_{f} j)\}$
16	1 15	psrbagconf1o	$⊢ F -_{f} j \in D \to (m \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ (F -_{f} j) -_{f} m) : \{x \in D \| x \leq_{f} (F -_{f} j)\} \underset{1-1 onto}{⟶} \{x \in D \| x \leq_{f} (F -_{f} j)\}$
17	14 16	syl	$⊢ (φ \land j \in S) \to (m \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ (F -_{f} j) -_{f} m) : \{x \in D \| x \leq_{f} (F -_{f} j)\} \underset{1-1 onto}{⟶} \{x \in D \| x \leq_{f} (F -_{f} j)\}$
18		f1of	$⊢ (m \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ (F -_{f} j) -_{f} m) : \{x \in D \| x \leq_{f} (F -_{f} j)\} \underset{1-1 onto}{⟶} \{x \in D \| x \leq_{f} (F -_{f} j)\} \to (m \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ (F -_{f} j) -_{f} m) : \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟶ \{x \in D \| x \leq_{f} (F -_{f} j)\}$
19	17 18	syl	$⊢ (φ \land j \in S) \to (m \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ (F -_{f} j) -_{f} m) : \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟶ \{x \in D \| x \leq_{f} (F -_{f} j)\}$
20	10 19	fcod	$⊢ (φ \land j \in S) \to ((k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) \circ (m \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ (F -_{f} j) -_{f} m)) : \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟶ B$
21	3	adantr	$⊢ (φ \land j \in S) \to F \in D$
22	21	adantr	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to F \in D$
23	1	psrbagf	$⊢ F \in D \to F : I ⟶ ℕ_{0}$
24	22 23	syl	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to F : I ⟶ ℕ_{0}$
25	24	ffvelrnda	$⊢ (((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \land z \in I) \to F (z) \in ℕ_{0}$
26		simplr	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to j \in S$
27	11 26	sselid	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to j \in D$
28	1	psrbagf	$⊢ j \in D \to j : I ⟶ ℕ_{0}$
29	27 28	syl	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to j : I ⟶ ℕ_{0}$
30	29	ffvelrnda	$⊢ (((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \land z \in I) \to j (z) \in ℕ_{0}$
31		ssrab2	$⊢ \{x \in D \| x \leq_{f} (F -_{f} j)\} \subseteq D$
32		simpr	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}$
33	31 32	sselid	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to m \in D$
34	1	psrbagf	$⊢ m \in D \to m : I ⟶ ℕ_{0}$
35	33 34	syl	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to m : I ⟶ ℕ_{0}$
36	35	ffvelrnda	$⊢ (((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \land z \in I) \to m (z) \in ℕ_{0}$
37		nn0cn	$⊢ F (z) \in ℕ_{0} \to F (z) \in ℂ$
38		nn0cn	$⊢ j (z) \in ℕ_{0} \to j (z) \in ℂ$
39		nn0cn	$⊢ m (z) \in ℕ_{0} \to m (z) \in ℂ$
40		sub32	$⊢ (F (z) \in ℂ \land j (z) \in ℂ \land m (z) \in ℂ) \to F (z) - j (z) - m (z) = F (z) - m (z) - j (z)$
41	37 38 39 40	syl3an	$⊢ (F (z) \in ℕ_{0} \land j (z) \in ℕ_{0} \land m (z) \in ℕ_{0}) \to F (z) - j (z) - m (z) = F (z) - m (z) - j (z)$
42	25 30 36 41	syl3anc	$⊢ (((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \land z \in I) \to F (z) - j (z) - m (z) = F (z) - m (z) - j (z)$
43	42	mpteq2dva	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to (z \in I ⟼ F (z) - j (z) - m (z)) = (z \in I ⟼ F (z) - m (z) - j (z))$
44	35	ffnd	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to m Fn I$
45	32 44	fndmexd	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to I \in V$
46		ovexd	$⊢ (((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \land z \in I) \to F (z) - j (z) \in V$
47	24	feqmptd	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to F = (z \in I ⟼ F (z))$
48	29	feqmptd	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to j = (z \in I ⟼ j (z))$
49	45 25 30 47 48	offval2	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to F -_{f} j = (z \in I ⟼ F (z) - j (z))$
50	35	feqmptd	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to m = (z \in I ⟼ m (z))$
51	45 46 36 49 50	offval2	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to (F -_{f} j) -_{f} m = (z \in I ⟼ F (z) - j (z) - m (z))$
52		ovexd	$⊢ (((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \land z \in I) \to F (z) - m (z) \in V$
53	45 25 36 47 50	offval2	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to F -_{f} m = (z \in I ⟼ F (z) - m (z))$
54	45 52 30 53 48	offval2	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to (F -_{f} m) -_{f} j = (z \in I ⟼ F (z) - m (z) - j (z))$
55	43 51 54	3eqtr4d	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to (F -_{f} j) -_{f} m = (F -_{f} m) -_{f} j$
56	1 15	psrbagconcl	$⊢ (F -_{f} j \in D \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to (F -_{f} j) -_{f} m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}$
57	14 56	sylan	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to (F -_{f} j) -_{f} m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}$
58	55 57	eqeltrrd	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to (F -_{f} m) -_{f} j \in \{x \in D \| x \leq_{f} (F -_{f} j)\}$
59	55	mpteq2dva	$⊢ (φ \land j \in S) \to (m \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ (F -_{f} j) -_{f} m) = (m \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ (F -_{f} m) -_{f} j)$
60		nfcv	$⊢ \underline{Ⅎ} n X$
61		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ n / k ⦌ X$
62		csbeq1a	$⊢ k = n \to X = ⦋ n / k ⦌ X$
63	60 61 62	cbvmpt	$⊢ (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) = (n \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ ⦋ n / k ⦌ X)$
64	63	a1i	$⊢ (φ \land j \in S) \to (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) = (n \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ ⦋ n / k ⦌ X)$
65		csbeq1	$⊢ n = (F -_{f} m) -_{f} j \to ⦋ n / k ⦌ X = ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X$
66	58 59 64 65	fmptco	$⊢ (φ \land j \in S) \to (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) \circ (m \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ (F -_{f} j) -_{f} m) = (m \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X)$
67	66	feq1d	$⊢ (φ \land j \in S) \to (((k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) \circ (m \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ (F -_{f} j) -_{f} m)) : \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟶ B \leftrightarrow (m \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) : \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟶ B)$
68	20 67	mpbid	$⊢ (φ \land j \in S) \to (m \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) : \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟶ B$
69	68	fvmptelrn	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X \in B$
70	69	anasss	$⊢ (φ \land (j \in S \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X \in B$
71	8 70	syldan	$⊢ (φ \land (m \in S \land j \in \{x \in D \| x \leq_{f} (F -_{f} m)\})) \to ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X \in B$
72	1 2 3 4 5 71	gsumbagdiag	$⊢ φ \to \sum_{G} (m \in S, j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) = \sum_{G} (j \in S, m \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X)$
73		eqid	$⊢ 0_{G} = 0_{G}$
74	1	psrbaglefi	$⊢ F \in D \to \{y \in D \| y \leq_{f} F\} \in Fin$
75	3 74	syl	$⊢ φ \to \{y \in D \| y \leq_{f} F\} \in Fin$
76	2 75	eqeltrid	$⊢ φ \to S \in Fin$
77	1 2	psrbagconcl	$⊢ (F \in D \land m \in S) \to F -_{f} m \in S$
78	3 77	sylan	$⊢ (φ \land m \in S) \to F -_{f} m \in S$
79	11 78	sselid	$⊢ (φ \land m \in S) \to F -_{f} m \in D$
80	1	psrbaglefi	$⊢ F -_{f} m \in D \to \{x \in D \| x \leq_{f} (F -_{f} m)\} \in Fin$
81	79 80	syl	$⊢ (φ \land m \in S) \to \{x \in D \| x \leq_{f} (F -_{f} m)\} \in Fin$
82		xpfi	$⊢ (S \in Fin \land S \in Fin) \to S \times S \in Fin$
83	76 76 82	syl2anc	$⊢ φ \to S \times S \in Fin$
84		simprl	$⊢ (φ \land (m \in S \land j \in \{x \in D \| x \leq_{f} (F -_{f} m)\})) \to m \in S$
85	8	simpld	$⊢ (φ \land (m \in S \land j \in \{x \in D \| x \leq_{f} (F -_{f} m)\})) \to j \in S$
86		brxp	$⊢ m (S \times S) j \leftrightarrow (m \in S \land j \in S)$
87	84 85 86	sylanbrc	$⊢ (φ \land (m \in S \land j \in \{x \in D \| x \leq_{f} (F -_{f} m)\})) \to m (S \times S) j$
88	87	pm2.24d	$⊢ (φ \land (m \in S \land j \in \{x \in D \| x \leq_{f} (F -_{f} m)\})) \to (\neg m (S \times S) j \to ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X = 0_{G})$
89	88	impr	$⊢ (φ \land ((m \in S \land j \in \{x \in D \| x \leq_{f} (F -_{f} m)\}) \land \neg m (S \times S) j)) \to ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X = 0_{G}$
90	4 73 5 76 81 71 83 89	gsum2d2	$⊢ φ \to \sum_{G} (m \in S, j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) = \underset{m \in S}{\sum_{G}} (\underset{j \in \{x \in D \| x \leq_{f} (F -_{f} m)\}}{\sum_{G}}, ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X)$
91	1	psrbaglefi	$⊢ F -_{f} j \in D \to \{x \in D \| x \leq_{f} (F -_{f} j)\} \in Fin$
92	14 91	syl	$⊢ (φ \land j \in S) \to \{x \in D \| x \leq_{f} (F -_{f} j)\} \in Fin$
93		simprl	$⊢ (φ \land (j \in S \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to j \in S$
94	1 2 3	gsumbagdiaglem	$⊢ (φ \land (j \in S \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to (m \in S \land j \in \{x \in D \| x \leq_{f} (F -_{f} m)\})$
95	94	simpld	$⊢ (φ \land (j \in S \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to m \in S$
96		brxp	$⊢ j (S \times S) m \leftrightarrow (j \in S \land m \in S)$
97	93 95 96	sylanbrc	$⊢ (φ \land (j \in S \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to j (S \times S) m$
98	97	pm2.24d	$⊢ (φ \land (j \in S \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to (\neg j (S \times S) m \to ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X = 0_{G})$
99	98	impr	$⊢ (φ \land ((j \in S \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \land \neg j (S \times S) m)) \to ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X = 0_{G}$
100	4 73 5 76 92 70 83 99	gsum2d2	$⊢ φ \to \sum_{G} (j \in S, m \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) = \underset{j \in S}{\sum_{G}} (\underset{m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}}{\sum_{G}}, ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X)$
101	72 90 100	3eqtr3d	$⊢ φ \to \underset{m \in S}{\sum_{G}} (\underset{j \in \{x \in D \| x \leq_{f} (F -_{f} m)\}}{\sum_{G}}, ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) = \underset{j \in S}{\sum_{G}} (\underset{m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}}{\sum_{G}}, ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X)$
102	5	adantr	$⊢ (φ \land m \in S) \to G \in CMnd$
103	71	anassrs	$⊢ ((φ \land m \in S) \land j \in \{x \in D \| x \leq_{f} (F -_{f} m)\}) \to ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X \in B$
104	103	fmpttd	$⊢ (φ \land m \in S) \to (j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) : \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟶ B$
105		ovex	$⊢ {ℕ_{0}}^{I} \in V$
106	1 105	rabex2	$⊢ D \in V$
107	106	a1i	$⊢ (φ \land m \in S) \to D \in V$
108		rabexg	$⊢ D \in V \to \{x \in D \| x \leq_{f} (F -_{f} m)\} \in V$
109		mptexg	$⊢ \{x \in D \| x \leq_{f} (F -_{f} m)\} \in V \to (j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) \in V$
110	107 108 109	3syl	$⊢ (φ \land m \in S) \to (j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) \in V$
111		funmpt	$⊢ Fun (j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X)$
112	111	a1i	$⊢ (φ \land m \in S) \to Fun (j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X)$
113		fvexd	$⊢ (φ \land m \in S) \to 0_{G} \in V$
114		suppssdm	$⊢ (j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) supp 0_{G} \subseteq dom (j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X)$
115		eqid	$⊢ (j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) = (j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X)$
116	115	dmmptss	$⊢ dom (j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) \subseteq \{x \in D \| x \leq_{f} (F -_{f} m)\}$
117	114 116	sstri	$⊢ (j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) supp 0_{G} \subseteq \{x \in D \| x \leq_{f} (F -_{f} m)\}$
118	117	a1i	$⊢ (φ \land m \in S) \to (j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) supp 0_{G} \subseteq \{x \in D \| x \leq_{f} (F -_{f} m)\}$
119		suppssfifsupp	$⊢ (((j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) \in V \land Fun (j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) \land 0_{G} \in V) \land (\{x \in D \| x \leq_{f} (F -_{f} m)\} \in Fin \land (j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) supp 0_{G} \subseteq \{x \in D \| x \leq_{f} (F -_{f} m)\})) \to {finSupp}_{0_{G}} ((j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X))$
120	110 112 113 81 118 119	syl32anc	$⊢ (φ \land m \in S) \to {finSupp}_{0_{G}} ((j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X))$
121	4 73 102 81 104 120	gsumcl	$⊢ (φ \land m \in S) \to \underset{j \in \{x \in D \| x \leq_{f} (F -_{f} m)\}}{\sum_{G}} ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X \in B$
122	121	fmpttd	$⊢ φ \to (m \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} (F -_{f} m)\}}{\sum_{G}} ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) : S ⟶ B$
123	1 2	psrbagconf1o	$⊢ F \in D \to (m \in S ⟼ F -_{f} m) : S \underset{1-1 onto}{⟶} S$
124	3 123	syl	$⊢ φ \to (m \in S ⟼ F -_{f} m) : S \underset{1-1 onto}{⟶} S$
125		f1ocnv	$⊢ (m \in S ⟼ F -_{f} m) : S \underset{1-1 onto}{⟶} S \to {(m \in S ⟼ F -_{f} m)}^{-1} : S \underset{1-1 onto}{⟶} S$
126		f1of	$⊢ {(m \in S ⟼ F -_{f} m)}^{-1} : S \underset{1-1 onto}{⟶} S \to {(m \in S ⟼ F -_{f} m)}^{-1} : S ⟶ S$
127	124 125 126	3syl	$⊢ φ \to {(m \in S ⟼ F -_{f} m)}^{-1} : S ⟶ S$
128	122 127	fcod	$⊢ φ \to ((m \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} (F -_{f} m)\}}{\sum_{G}} ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) \circ {(m \in S ⟼ F -_{f} m)}^{-1}) : S ⟶ B$
129		coass	$⊢ ((n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \circ (m \in S ⟼ F -_{f} m)) \circ {(m \in S ⟼ F -_{f} m)}^{-1} = (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \circ ((m \in S ⟼ F -_{f} m) \circ {(m \in S ⟼ F -_{f} m)}^{-1})$
130		f1ococnv2	$⊢ (m \in S ⟼ F -_{f} m) : S \underset{1-1 onto}{⟶} S \to (m \in S ⟼ F -_{f} m) \circ {(m \in S ⟼ F -_{f} m)}^{-1} = {I ↾}_{S}$
131	124 130	syl	$⊢ φ \to (m \in S ⟼ F -_{f} m) \circ {(m \in S ⟼ F -_{f} m)}^{-1} = {I ↾}_{S}$
132	131	coeq2d	$⊢ φ \to (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \circ ((m \in S ⟼ F -_{f} m) \circ {(m \in S ⟼ F -_{f} m)}^{-1}) = (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \circ ({I ↾}_{S})$
133	129 132	syl5eq	$⊢ φ \to ((n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \circ (m \in S ⟼ F -_{f} m)) \circ {(m \in S ⟼ F -_{f} m)}^{-1} = (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \circ ({I ↾}_{S})$
134		eqidd	$⊢ φ \to (m \in S ⟼ F -_{f} m) = (m \in S ⟼ F -_{f} m)$
135		eqidd	$⊢ φ \to (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) = (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y)$
136		breq2	$⊢ n = F -_{f} m \to (x \leq_{f} n \leftrightarrow x \leq_{f} (F -_{f} m))$
137	136	rabbidv	$⊢ n = F -_{f} m \to \{x \in D \| x \leq_{f} n\} = \{x \in D \| x \leq_{f} (F -_{f} m)\}$
138		ovex	$⊢ n -_{f} j \in V$
139	138 7	csbie	$⊢ ⦋ (n -_{f} j) / k ⦌ X = Y$
140		oveq1	$⊢ n = F -_{f} m \to n -_{f} j = (F -_{f} m) -_{f} j$
141	140	csbeq1d	$⊢ n = F -_{f} m \to ⦋ (n -_{f} j) / k ⦌ X = ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X$
142	139 141	eqtr3id	$⊢ n = F -_{f} m \to Y = ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X$
143	137 142	mpteq12dv	$⊢ n = F -_{f} m \to (j \in \{x \in D \| x \leq_{f} n\} ⟼ Y) = (j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X)$
144	143	oveq2d	$⊢ n = F -_{f} m \to \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y = \underset{j \in \{x \in D \| x \leq_{f} (F -_{f} m)\}}{\sum_{G}} ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X$
145	78 134 135 144	fmptco	$⊢ φ \to (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \circ (m \in S ⟼ F -_{f} m) = (m \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} (F -_{f} m)\}}{\sum_{G}} ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X)$
146	145	coeq1d	$⊢ φ \to ((n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \circ (m \in S ⟼ F -_{f} m)) \circ {(m \in S ⟼ F -_{f} m)}^{-1} = (m \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} (F -_{f} m)\}}{\sum_{G}} ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) \circ {(m \in S ⟼ F -_{f} m)}^{-1}$
147		coires1	$⊢ (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \circ ({I ↾}_{S}) = {(n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) ↾}_{S}$
148		ssid	$⊢ S \subseteq S$
149		resmpt	$⊢ S \subseteq S \to {(n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) ↾}_{S} = (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y)$
150	148 149	ax-mp	$⊢ {(n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) ↾}_{S} = (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y)$
151	147 150	eqtri	$⊢ (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \circ ({I ↾}_{S}) = (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y)$
152	151	a1i	$⊢ φ \to (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \circ ({I ↾}_{S}) = (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y)$
153	133 146 152	3eqtr3d	$⊢ φ \to (m \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} (F -_{f} m)\}}{\sum_{G}} ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) \circ {(m \in S ⟼ F -_{f} m)}^{-1} = (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y)$
154	153	feq1d	$⊢ φ \to (((m \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} (F -_{f} m)\}}{\sum_{G}} ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X) \circ {(m \in S ⟼ F -_{f} m)}^{-1}) : S ⟶ B \leftrightarrow (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) : S ⟶ B)$
155	128 154	mpbid	$⊢ φ \to (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) : S ⟶ B$
156		rabexg	$⊢ D \in V \to \{y \in D \| y \leq_{f} F\} \in V$
157	106 156	mp1i	$⊢ φ \to \{y \in D \| y \leq_{f} F\} \in V$
158	2 157	eqeltrid	$⊢ φ \to S \in V$
159	158	mptexd	$⊢ φ \to (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \in V$
160		funmpt	$⊢ Fun (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y)$
161	160	a1i	$⊢ φ \to Fun (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y)$
162		fvexd	$⊢ φ \to 0_{G} \in V$
163		suppssdm	$⊢ (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) supp 0_{G} \subseteq dom (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y)$
164		eqid	$⊢ (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) = (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y)$
165	164	dmmptss	$⊢ dom (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \subseteq S$
166	163 165	sstri	$⊢ (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) supp 0_{G} \subseteq S$
167	166	a1i	$⊢ φ \to (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) supp 0_{G} \subseteq S$
168		suppssfifsupp	$⊢ (((n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \in V \land Fun (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \land 0_{G} \in V) \land (S \in Fin \land (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) supp 0_{G} \subseteq S)) \to {finSupp}_{0_{G}} ((n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y))$
169	159 161 162 76 167 168	syl32anc	$⊢ φ \to {finSupp}_{0_{G}} ((n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y))$
170	4 73 5 76 155 169 124	gsumf1o	$⊢ φ \to \underset{n \in S}{\sum_{G}} (\underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}}, Y) = \sum_{G} ((n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \circ (m \in S ⟼ F -_{f} m))$
171	145	oveq2d	$⊢ φ \to \sum_{G} ((n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \circ (m \in S ⟼ F -_{f} m)) = \underset{m \in S}{\sum_{G}} (\underset{j \in \{x \in D \| x \leq_{f} (F -_{f} m)\}}{\sum_{G}}, ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X)$
172	170 171	eqtrd	$⊢ φ \to \underset{n \in S}{\sum_{G}} (\underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}}, Y) = \underset{m \in S}{\sum_{G}} (\underset{j \in \{x \in D \| x \leq_{f} (F -_{f} m)\}}{\sum_{G}}, ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X)$
173	5	adantr	$⊢ (φ \land j \in S) \to G \in CMnd$
174	106	a1i	$⊢ (φ \land j \in S) \to D \in V$
175		rabexg	$⊢ D \in V \to \{x \in D \| x \leq_{f} (F -_{f} j)\} \in V$
176		mptexg	$⊢ \{x \in D \| x \leq_{f} (F -_{f} j)\} \in V \to (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) \in V$
177	174 175 176	3syl	$⊢ (φ \land j \in S) \to (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) \in V$
178		funmpt	$⊢ Fun (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X)$
179	178	a1i	$⊢ (φ \land j \in S) \to Fun (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X)$
180		fvexd	$⊢ (φ \land j \in S) \to 0_{G} \in V$
181		suppssdm	$⊢ (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) supp 0_{G} \subseteq dom (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X)$
182		eqid	$⊢ (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) = (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X)$
183	182	dmmptss	$⊢ dom (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) \subseteq \{x \in D \| x \leq_{f} (F -_{f} j)\}$
184	181 183	sstri	$⊢ (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) supp 0_{G} \subseteq \{x \in D \| x \leq_{f} (F -_{f} j)\}$
185	184	a1i	$⊢ (φ \land j \in S) \to (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) supp 0_{G} \subseteq \{x \in D \| x \leq_{f} (F -_{f} j)\}$
186		suppssfifsupp	$⊢ (((k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) \in V \land Fun (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) \land 0_{G} \in V) \land (\{x \in D \| x \leq_{f} (F -_{f} j)\} \in Fin \land (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) supp 0_{G} \subseteq \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to {finSupp}_{0_{G}} ((k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X))$
187	177 179 180 92 185 186	syl32anc	$⊢ (φ \land j \in S) \to {finSupp}_{0_{G}} ((k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X))$
188	4 73 173 92 10 187 17	gsumf1o	$⊢ (φ \land j \in S) \to \underset{k \in \{x \in D \| x \leq_{f} (F -_{f} j)\}}{\sum_{G}} X = \sum_{G} ((k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) \circ (m \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ (F -_{f} j) -_{f} m))$
189	66	oveq2d	$⊢ (φ \land j \in S) \to \sum_{G} ((k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) \circ (m \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ (F -_{f} j) -_{f} m)) = \underset{m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}}{\sum_{G}} ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X$
190	188 189	eqtrd	$⊢ (φ \land j \in S) \to \underset{k \in \{x \in D \| x \leq_{f} (F -_{f} j)\}}{\sum_{G}} X = \underset{m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}}{\sum_{G}} ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X$
191	190	mpteq2dva	$⊢ φ \to (j \in S ⟼ \underset{k \in \{x \in D \| x \leq_{f} (F -_{f} j)\}}{\sum_{G}} X) = (j \in S ⟼ \underset{m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}}{\sum_{G}} ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X)$
192	191	oveq2d	$⊢ φ \to \underset{j \in S}{\sum_{G}} (\underset{k \in \{x \in D \| x \leq_{f} (F -_{f} j)\}}{\sum_{G}}, X) = \underset{j \in S}{\sum_{G}} (\underset{m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}}{\sum_{G}}, ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X)$
193	101 172 192	3eqtr4d	$⊢ φ \to \underset{n \in S}{\sum_{G}} (\underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}}, Y) = \underset{j \in S}{\sum_{G}} (\underset{k \in \{x \in D \| x \leq_{f} (F -_{f} j)\}}{\sum_{G}}, X)$

Metamath Proof Explorer

Theorem psrass1lem

Proof