psrass1lem

Description: A group sum commutation used by psrass1 . (Contributed by Mario Carneiro, 5-Jan-2015)

	Ref	Expression
Hypotheses	psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	psrbagconf1o.1	$⊢ S = \{y \in D \| y \leq_{f} F\}$
	gsumbagdiag.i	$⊢ φ \to I \in V$
	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		psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
2		psrbagconf1o.1	$⊢ S = \{y \in D \| y \leq_{f} F\}$
3		gsumbagdiag.i	$⊢ φ \to I \in V$
4		gsumbagdiag.f	$⊢ φ \to F \in D$
5		gsumbagdiag.b	$⊢ B = {Base}_{G}$
6		gsumbagdiag.g	$⊢ φ \to G \in CMnd$
7		gsumbagdiag.x	$⊢ (φ \land (j \in S \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to X \in B$
8		psrass1lem.y	$⊢ k = n -_{f} j \to X = Y$
9	1 2 3 4	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)\})$
10	7	anassrs	$⊢ ((φ \land j \in S) \land k \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to X \in B$
11	10	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$
12	3	adantr	$⊢ (φ \land j \in S) \to I \in V$
13	2	ssrab3	$⊢ S \subseteq D$
14	4	adantr	$⊢ (φ \land j \in S) \to F \in D$
15		simpr	$⊢ (φ \land j \in S) \to j \in S$
16	1 2	psrbagconcl	$⊢ (I \in V \land F \in D \land j \in S) \to F -_{f} j \in S$
17	12 14 15 16	syl3anc	$⊢ (φ \land j \in S) \to F -_{f} j \in S$
18	13 17	sseldi	$⊢ (φ \land j \in S) \to F -_{f} j \in D$
19		eqid	$⊢ \{x \in D \| x \leq_{f} (F -_{f} j)\} = \{x \in D \| x \leq_{f} (F -_{f} j)\}$
20	1 19	psrbagconf1o	$⊢ (I \in V \land 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)\}$
21	12 18 20	syl2anc	$⊢ (φ \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)\}$
22		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)\}$
23	21 22	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)\}$
24		fco	$⊢ ((k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) : \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟶ B \land (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)\}) \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$
25	11 23 24	syl2anc	$⊢ (φ \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$
26	12	adantr	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to I \in V$
27	14	adantr	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to F \in D$
28	1	psrbagf	$⊢ (I \in V \land F \in D) \to F : I ⟶ ℕ_{0}$
29	26 27 28	syl2anc	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to F : 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 F (z) \in ℕ_{0}$
31	15	adantr	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to j \in S$
32	13 31	sseldi	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to j \in D$
33	1	psrbagf	$⊢ (I \in V \land j \in D) \to j : I ⟶ ℕ_{0}$
34	26 32 33	syl2anc	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to j : I ⟶ ℕ_{0}$
35	34	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}$
36		ssrab2	$⊢ \{x \in D \| x \leq_{f} (F -_{f} j)\} \subseteq D$
37		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)\}$
38	36 37	sseldi	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to m \in D$
39	1	psrbagf	$⊢ (I \in V \land m \in D) \to m : I ⟶ ℕ_{0}$
40	26 38 39	syl2anc	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to m : I ⟶ ℕ_{0}$
41	40	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}$
42		nn0cn	$⊢ F (z) \in ℕ_{0} \to F (z) \in ℂ$
43		nn0cn	$⊢ j (z) \in ℕ_{0} \to j (z) \in ℂ$
44		nn0cn	$⊢ m (z) \in ℕ_{0} \to m (z) \in ℂ$
45		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)$
46	42 43 44 45	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)$
47	30 35 41 46	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)$
48	47	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))$
49		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$
50	29	feqmptd	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to F = (z \in I ⟼ F (z))$
51	34	feqmptd	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to j = (z \in I ⟼ j (z))$
52	26 30 35 50 51	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))$
53	40	feqmptd	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to m = (z \in I ⟼ m (z))$
54	26 49 41 52 53	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))$
55		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$
56	26 30 41 50 53	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))$
57	26 55 35 56 51	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))$
58	48 54 57	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$
59	18	adantr	$⊢ ((φ \land j \in S) \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\}) \to F -_{f} j \in D$
60	1 19	psrbagconcl	$⊢ (I \in V \land 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)\}$
61	26 59 37 60	syl3anc	$⊢ ((φ \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)\}$
62	58 61	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)\}$
63	58	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)$
64		nfcv	$⊢ \underline{Ⅎ} n X$
65		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ n / k ⦌ X$
66		csbeq1a	$⊢ k = n \to X = ⦋ n / k ⦌ X$
67	64 65 66	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)$
68	67	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)$
69		csbeq1	$⊢ n = (F -_{f} m) -_{f} j \to ⦋ n / k ⦌ X = ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X$
70	62 63 68 69	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)$
71	70	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)$
72	25 71	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$
73	72	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$
74	73	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$
75	9 74	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$
76	1 2 3 4 5 6 75	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)$
77		eqid	$⊢ 0_{G} = 0_{G}$
78	1	psrbaglefi	$⊢ (I \in V \land F \in D) \to \{y \in D \| y \leq_{f} F\} \in Fin$
79	3 4 78	syl2anc	$⊢ φ \to \{y \in D \| y \leq_{f} F\} \in Fin$
80	2 79	eqeltrid	$⊢ φ \to S \in Fin$
81	3	adantr	$⊢ (φ \land m \in S) \to I \in V$
82	4	adantr	$⊢ (φ \land m \in S) \to F \in D$
83		simpr	$⊢ (φ \land m \in S) \to m \in S$
84	1 2	psrbagconcl	$⊢ (I \in V \land F \in D \land m \in S) \to F -_{f} m \in S$
85	81 82 83 84	syl3anc	$⊢ (φ \land m \in S) \to F -_{f} m \in S$
86	13 85	sseldi	$⊢ (φ \land m \in S) \to F -_{f} m \in D$
87	1	psrbaglefi	$⊢ (I \in V \land F -_{f} m \in D) \to \{x \in D \| x \leq_{f} (F -_{f} m)\} \in Fin$
88	81 86 87	syl2anc	$⊢ (φ \land m \in S) \to \{x \in D \| x \leq_{f} (F -_{f} m)\} \in Fin$
89		xpfi	$⊢ (S \in Fin \land S \in Fin) \to S \times S \in Fin$
90	80 80 89	syl2anc	$⊢ φ \to S \times S \in Fin$
91		simprl	$⊢ (φ \land (m \in S \land j \in \{x \in D \| x \leq_{f} (F -_{f} m)\})) \to m \in S$
92	9	simpld	$⊢ (φ \land (m \in S \land j \in \{x \in D \| x \leq_{f} (F -_{f} m)\})) \to j \in S$
93		brxp	$⊢ m (S \times S) j \leftrightarrow (m \in S \land j \in S)$
94	91 92 93	sylanbrc	$⊢ (φ \land (m \in S \land j \in \{x \in D \| x \leq_{f} (F -_{f} m)\})) \to m (S \times S) j$
95	94	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})$
96	95	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}$
97	5 77 6 80 88 75 90 96	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)$
98	1	psrbaglefi	$⊢ (I \in V \land F -_{f} j \in D) \to \{x \in D \| x \leq_{f} (F -_{f} j)\} \in Fin$
99	12 18 98	syl2anc	$⊢ (φ \land j \in S) \to \{x \in D \| x \leq_{f} (F -_{f} j)\} \in Fin$
100		simprl	$⊢ (φ \land (j \in S \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to j \in S$
101	1 2 3 4	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)\})$
102	101	simpld	$⊢ (φ \land (j \in S \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to m \in S$
103		brxp	$⊢ j (S \times S) m \leftrightarrow (j \in S \land m \in S)$
104	100 102 103	sylanbrc	$⊢ (φ \land (j \in S \land m \in \{x \in D \| x \leq_{f} (F -_{f} j)\})) \to j (S \times S) m$
105	104	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})$
106	105	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}$
107	5 77 6 80 99 74 90 106	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)$
108	76 97 107	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)$
109	6	adantr	$⊢ (φ \land m \in S) \to G \in CMnd$
110	75	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$
111	110	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$
112		ovex	$⊢ {ℕ_{0}}^{I} \in V$
113	1 112	rabex2	$⊢ D \in V$
114	113	a1i	$⊢ (φ \land m \in S) \to D \in V$
115		rabexg	$⊢ D \in V \to \{x \in D \| x \leq_{f} (F -_{f} m)\} \in V$
116		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$
117	114 115 116	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$
118		funmpt	$⊢ Fun (j \in \{x \in D \| x \leq_{f} (F -_{f} m)\} ⟼ ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X)$
119	118	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)$
120		fvexd	$⊢ (φ \land m \in S) \to 0_{G} \in V$
121		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)$
122		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)$
123	122	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)\}$
124	121 123	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)\}$
125	124	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)\}$
126		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))$
127	117 119 120 88 125 126	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))$
128	5 77 109 88 111 127	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$
129	128	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$
130	1 2	psrbagconf1o	$⊢ (I \in V \land F \in D) \to (m \in S ⟼ F -_{f} m) : S \underset{1-1 onto}{⟶} S$
131	3 4 130	syl2anc	$⊢ φ \to (m \in S ⟼ F -_{f} m) : S \underset{1-1 onto}{⟶} S$
132		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$
133		f1of	$⊢ {(m \in S ⟼ F -_{f} m)}^{-1} : S \underset{1-1 onto}{⟶} S \to {(m \in S ⟼ F -_{f} m)}^{-1} : S ⟶ S$
134	131 132 133	3syl	$⊢ φ \to {(m \in S ⟼ F -_{f} m)}^{-1} : S ⟶ S$
135		fco	$⊢ ((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 \land {(m \in S ⟼ F -_{f} m)}^{-1} : S ⟶ S) \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$
136	129 134 135	syl2anc	$⊢ φ \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$
137		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})$
138		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}$
139	131 138	syl	$⊢ φ \to (m \in S ⟼ F -_{f} m) \circ {(m \in S ⟼ F -_{f} m)}^{-1} = {I ↾}_{S}$
140	139	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})$
141	137 140	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})$
142		eqidd	$⊢ φ \to (m \in S ⟼ F -_{f} m) = (m \in S ⟼ F -_{f} m)$
143		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)$
144		breq2	$⊢ n = F -_{f} m \to (x \leq_{f} n \leftrightarrow x \leq_{f} (F -_{f} m))$
145	144	rabbidv	$⊢ n = F -_{f} m \to \{x \in D \| x \leq_{f} n\} = \{x \in D \| x \leq_{f} (F -_{f} m)\}$
146		ovex	$⊢ n -_{f} j \in V$
147	146 8	csbie	$⊢ ⦋ (n -_{f} j) / k ⦌ X = Y$
148		oveq1	$⊢ n = F -_{f} m \to n -_{f} j = (F -_{f} m) -_{f} j$
149	148	csbeq1d	$⊢ n = F -_{f} m \to ⦋ (n -_{f} j) / k ⦌ X = ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X$
150	147 149	syl5eqr	$⊢ n = F -_{f} m \to Y = ⦋ ((F -_{f} m) -_{f} j) / k ⦌ X$
151	145 150	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)$
152	151	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$
153	85 142 143 152	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)$
154	153	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}$
155		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}$
156		ssid	$⊢ S \subseteq S$
157		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)$
158	156 157	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)$
159	155 158	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)$
160	159	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)$
161	141 154 160	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)$
162	161	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)$
163	136 162	mpbid	$⊢ φ \to (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) : S ⟶ B$
164		rabexg	$⊢ D \in V \to \{y \in D \| y \leq_{f} F\} \in V$
165	113 164	mp1i	$⊢ φ \to \{y \in D \| y \leq_{f} F\} \in V$
166	2 165	eqeltrid	$⊢ φ \to S \in V$
167	166	mptexd	$⊢ φ \to (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \in V$
168		funmpt	$⊢ Fun (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y)$
169	168	a1i	$⊢ φ \to Fun (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y)$
170		fvexd	$⊢ φ \to 0_{G} \in V$
171		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)$
172		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)$
173	172	dmmptss	$⊢ dom (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) \subseteq S$
174	171 173	sstri	$⊢ (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) supp 0_{G} \subseteq S$
175	174	a1i	$⊢ φ \to (n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y) supp 0_{G} \subseteq S$
176		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))$
177	167 169 170 80 175 176	syl32anc	$⊢ φ \to {finSupp}_{0_{G}} ((n \in S ⟼ \underset{j \in \{x \in D \| x \leq_{f} n\}}{\sum_{G}} Y))$
178	5 77 6 80 163 177 131	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))$
179	153	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)$
180	178 179	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)$
181	6	adantr	$⊢ (φ \land j \in S) \to G \in CMnd$
182	113	a1i	$⊢ (φ \land j \in S) \to D \in V$
183		rabexg	$⊢ D \in V \to \{x \in D \| x \leq_{f} (F -_{f} j)\} \in V$
184		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$
185	182 183 184	3syl	$⊢ (φ \land j \in S) \to (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) \in V$
186		funmpt	$⊢ Fun (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X)$
187	186	a1i	$⊢ (φ \land j \in S) \to Fun (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X)$
188		fvexd	$⊢ (φ \land j \in S) \to 0_{G} \in V$
189		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)$
190		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)$
191	190	dmmptss	$⊢ dom (k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X) \subseteq \{x \in D \| x \leq_{f} (F -_{f} j)\}$
192	189 191	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)\}$
193	192	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)\}$
194		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))$
195	185 187 188 99 193 194	syl32anc	$⊢ (φ \land j \in S) \to {finSupp}_{0_{G}} ((k \in \{x \in D \| x \leq_{f} (F -_{f} j)\} ⟼ X))$
196	5 77 181 99 11 195 21	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))$
197	70	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$
198	196 197	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$
199	198	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)$
200	199	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)$
201	108 180 200	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