Theorem psrass1lem 21975

Description: A group sum commutation used by psrass1 22007. (Contributed by Mario Carneiro, 5-Jan-2015.) Remove a sethood hypothesis. (Revised by SN, 7-Aug-2024.)

Hypotheses

Ref	Expression
gsumbagdiag.d	⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
gsumbagdiag.s	⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹}
gsumbagdiag.f	⊢ (𝜑 → 𝐹 ∈ 𝐷)
gsumbagdiag.b	⊢ 𝐵 = (Base‘𝐺)
gsumbagdiag.g	⊢ (𝜑 → 𝐺 ∈ CMnd)
gsumbagdiag.x	⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑋 ∈ 𝐵)
psrass1lem.y	⊢ (𝑘 = (𝑛 ∘f − 𝑗) → 𝑋 = 𝑌)

Assertion

Ref	Expression
psrass1lem	⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)))))

Distinct variable groups:   𝑥,𝐷   𝑦,𝐷   𝑓,𝐹,𝑥   𝑦,𝐹   𝑓,𝐼   𝑓,𝑋,𝑥   𝑦,𝑋   𝑓,𝑌,𝑥   𝑦,𝑌   𝐵,𝑗,𝑘   𝐷,𝑗,𝑘   𝑗,𝐹,𝑘   𝑗,𝐺,𝑘   𝑦,𝐼,𝑓   𝑆,𝑗,𝑘   𝜑,𝑗,𝑘   𝑓,𝑗,𝑘,𝑦   𝑥,𝑗,𝑘   𝐷,𝑛,𝑗,𝑘,𝑥   𝑥,𝑓   𝑛,𝐹   𝑛,𝐺   𝑥,𝐼   𝑆,𝑛   𝑛,𝑋   𝑘,𝑌

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑓,𝑛)   𝐵(𝑥,𝑦,𝑓,𝑛)   𝐷(𝑓)   𝑆(𝑥,𝑦,𝑓)   𝐺(𝑥,𝑦,𝑓)   𝐼(𝑗,𝑘,𝑛)   𝑋(𝑗,𝑘)   𝑌(𝑗,𝑛)

Proof of Theorem psrass1lem

Dummy variables 𝑧 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsumbagdiag.d	. . . 4 ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
2		gsumbagdiag.s	. . . 4 ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹}
3		gsumbagdiag.f	. . . 4 ⊢ (𝜑 → 𝐹 ∈ 𝐷)
4		gsumbagdiag.b	. . . 4 ⊢ 𝐵 = (Base‘𝐺)
5		gsumbagdiag.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ CMnd)
6	1, 2, 3	gsumbagdiaglem 21973	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}))
7		gsumbagdiag.x	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑋 ∈ 𝐵)
8	7	anassrs 467	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑋 ∈ 𝐵)
9	8	fmpttd 7149	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵)
10	2	ssrab3 4105	. . . . . . . . . . . 12 ⊢ 𝑆 ⊆ 𝐷
11	1, 2	psrbagconcl 21970	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ 𝐷 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘f − 𝑗) ∈ 𝑆)
12	3, 11	sylan 579	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘f − 𝑗) ∈ 𝑆)
13	10, 12	sselid 4006	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘f − 𝑗) ∈ 𝐷)
14		eqid 2740	. . . . . . . . . . . 12 ⊢ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} = {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}
15	1, 14	psrbagconf1o 21972	. . . . . . . . . . 11 ⊢ ((𝐹 ∘f − 𝑗) ∈ 𝐷 → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}–1-1-onto→{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
16	13, 15	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}–1-1-onto→{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
17		f1of 6862	. . . . . . . . . 10 ⊢ ((𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}–1-1-onto→{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
18	16, 17	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
19	9, 18	fcod 6773	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚))):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵)
20	3	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐹 ∈ 𝐷)
21	20	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐹 ∈ 𝐷)
22	1	psrbagf 21961	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ 𝐷 → 𝐹:𝐼⟶ℕ0)
23	21, 22	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐹:𝐼⟶ℕ0)
24	23	ffvelcdmda 7118	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈ ℕ0)
25		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗 ∈ 𝑆)
26	10, 25	sselid 4006	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗 ∈ 𝐷)
27	1	psrbagf 21961	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ 𝐷 → 𝑗:𝐼⟶ℕ0)
28	26, 27	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗:𝐼⟶ℕ0)
29	28	ffvelcdmda 7118	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝑗‘𝑧) ∈ ℕ0)
30		ssrab2 4103	. . . . . . . . . . . . . . . . 17 ⊢ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ⊆ 𝐷
31		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
32	30, 31	sselid 4006	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚 ∈ 𝐷)
33	1	psrbagf 21961	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ 𝐷 → 𝑚:𝐼⟶ℕ0)
34	32, 33	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚:𝐼⟶ℕ0)
35	34	ffvelcdmda 7118	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝑚‘𝑧) ∈ ℕ0)
36		nn0cn 12563	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑧) ∈ ℕ0 → (𝐹‘𝑧) ∈ ℂ)
37		nn0cn 12563	. . . . . . . . . . . . . . 15 ⊢ ((𝑗‘𝑧) ∈ ℕ0 → (𝑗‘𝑧) ∈ ℂ)
38		nn0cn 12563	. . . . . . . . . . . . . . 15 ⊢ ((𝑚‘𝑧) ∈ ℕ0 → (𝑚‘𝑧) ∈ ℂ)
39		sub32 11570	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑧) ∈ ℂ ∧ (𝑗‘𝑧) ∈ ℂ ∧ (𝑚‘𝑧) ∈ ℂ) → (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧)) = (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧)))
40	36, 37, 38, 39	syl3an 1160	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑧) ∈ ℕ0 ∧ (𝑗‘𝑧) ∈ ℕ0 ∧ (𝑚‘𝑧) ∈ ℕ0) → (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧)) = (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧)))
41	24, 29, 35, 40	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧)) = (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧)))
42	41	mpteq2dva 5266	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧))) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧))))
43	34	ffnd 6748	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚 Fn 𝐼)
44	31, 43	fndmexd 7944	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐼 ∈ V)
45		ovexd 7483	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑗‘𝑧)) ∈ V)
46	23	feqmptd 6990	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐹 = (𝑧 ∈ 𝐼 ↦ (𝐹‘𝑧)))
47	28	feqmptd 6990	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗 = (𝑧 ∈ 𝐼 ↦ (𝑗‘𝑧)))
48	44, 24, 29, 46, 47	offval2 7734	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝐹 ∘f − 𝑗) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑗‘𝑧))))
49	34	feqmptd 6990	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚 = (𝑧 ∈ 𝐼 ↦ (𝑚‘𝑧)))
50	44, 45, 35, 48, 49	offval2 7734	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f − 𝑚) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧))))
51		ovexd 7483	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑚‘𝑧)) ∈ V)
52	44, 24, 35, 46, 49	offval2 7734	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝐹 ∘f − 𝑚) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑚‘𝑧))))
53	44, 51, 29, 52, 47	offval2 7734	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑚) ∘f − 𝑗) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧))))
54	42, 50, 53	3eqtr4d 2790	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f − 𝑚) = ((𝐹 ∘f − 𝑚) ∘f − 𝑗))
55	1, 14	psrbagconcl 21970	. . . . . . . . . . . 12 ⊢ (((𝐹 ∘f − 𝑗) ∈ 𝐷 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f − 𝑚) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
56	13, 55	sylan 579	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f − 𝑚) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
57	54, 56	eqeltrrd 2845	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑚) ∘f − 𝑗) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
58	54	mpteq2dva 5266	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)) = (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑚) ∘f − 𝑗)))
59		nfcv 2908	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛𝑋
60		nfcsb1v 3946	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⦋𝑛 / 𝑘⦌𝑋
61		csbeq1a 3935	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → 𝑋 = ⦋𝑛 / 𝑘⦌𝑋)
62	59, 60, 61	cbvmpt 5277	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋𝑛 / 𝑘⦌𝑋)
63	62	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋𝑛 / 𝑘⦌𝑋))
64		csbeq1 3924	. . . . . . . . . 10 ⊢ (𝑛 = ((𝐹 ∘f − 𝑚) ∘f − 𝑗) → ⦋𝑛 / 𝑘⦌𝑋 = ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
65	57, 58, 63, 64	fmptco 7163	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚))) = (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))
66	65	feq1d 6732	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚))):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵 ↔ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵))
67	19, 66	mpbid 232	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵)
68	67	fvmptelcdm 7147	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵)
69	68	anasss 466	. . . . 5 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵)
70	6, 69	syldan 590	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵)
71	1, 2, 3, 4, 5, 70	gsumbagdiag 21974	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆, 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑗 ∈ 𝑆, 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))
72		eqid 2740	. . . 4 ⊢ (0g‘𝐺) = (0g‘𝐺)
73	1	psrbaglefi 21969	. . . . . 6 ⊢ (𝐹 ∈ 𝐷 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ Fin)
74	3, 73	syl 17	. . . . 5 ⊢ (𝜑 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ Fin)
75	2, 74	eqeltrid 2848	. . . 4 ⊢ (𝜑 → 𝑆 ∈ Fin)
76	1, 2	psrbagconcl 21970	. . . . . . 7 ⊢ ((𝐹 ∈ 𝐷 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘f − 𝑚) ∈ 𝑆)
77	3, 76	sylan 579	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘f − 𝑚) ∈ 𝑆)
78	10, 77	sselid 4006	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘f − 𝑚) ∈ 𝐷)
79	1	psrbaglefi 21969	. . . . 5 ⊢ ((𝐹 ∘f − 𝑚) ∈ 𝐷 → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ Fin)
80	78, 79	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ Fin)
81		xpfi 9386	. . . . 5 ⊢ ((𝑆 ∈ Fin ∧ 𝑆 ∈ Fin) → (𝑆 × 𝑆) ∈ Fin)
82	75, 75, 81	syl2anc 583	. . . 4 ⊢ (𝜑 → (𝑆 × 𝑆) ∈ Fin)
83		simprl 770	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → 𝑚 ∈ 𝑆)
84	6	simpld 494	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → 𝑗 ∈ 𝑆)
85		brxp 5749	. . . . . . 7 ⊢ (𝑚(𝑆 × 𝑆)𝑗 ↔ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ 𝑆))
86	83, 84, 85	sylanbrc 582	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → 𝑚(𝑆 × 𝑆)𝑗)
87	86	pm2.24d 151	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → (¬ 𝑚(𝑆 × 𝑆)𝑗 → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺)))
88	87	impr 454	. . . 4 ⊢ ((𝜑 ∧ ((𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}) ∧ ¬ 𝑚(𝑆 × 𝑆)𝑗)) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺))
89	4, 72, 5, 75, 80, 70, 82, 88	gsum2d2 20016	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆, 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
90	1	psrbaglefi 21969	. . . . 5 ⊢ ((𝐹 ∘f − 𝑗) ∈ 𝐷 → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ Fin)
91	13, 90	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ Fin)
92		simprl 770	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑗 ∈ 𝑆)
93	1, 2, 3	gsumbagdiaglem 21973	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}))
94	93	simpld 494	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑚 ∈ 𝑆)
95		brxp 5749	. . . . . . 7 ⊢ (𝑗(𝑆 × 𝑆)𝑚 ↔ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ 𝑆))
96	92, 94, 95	sylanbrc 582	. . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑗(𝑆 × 𝑆)𝑚)
97	96	pm2.24d 151	. . . . 5 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → (¬ 𝑗(𝑆 × 𝑆)𝑚 → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺)))
98	97	impr 454	. . . 4 ⊢ ((𝜑 ∧ ((𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ ¬ 𝑗(𝑆 × 𝑆)𝑚)) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺))
99	4, 72, 5, 75, 91, 69, 82, 98	gsum2d2 20016	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝑆, 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
100	71, 89, 99	3eqtr3d 2788	. 2 ⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
101	5	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐺 ∈ CMnd)
102	70	anassrs 467	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ 𝑆) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵)
103	102	fmpttd 7149	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}⟶𝐵)
104		ovex 7481	. . . . . . . . . . . 12 ⊢ (ℕ0 ↑m 𝐼) ∈ V
105	1, 104	rabex2 5359	. . . . . . . . . . 11 ⊢ 𝐷 ∈ V
106	105	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐷 ∈ V)
107		rabexg 5355	. . . . . . . . . 10 ⊢ (𝐷 ∈ V → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ V)
108		mptexg 7258	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ V → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ∈ V)
109	106, 107, 108	3syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ∈ V)
110		funmpt 6616	. . . . . . . . . 10 ⊢ Fun (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
111	110	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → Fun (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))
112		fvexd 6935	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (0g‘𝐺) ∈ V)
113		suppssdm 8218	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ dom (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
114		eqid 2740	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) = (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
115	114	dmmptss 6272	. . . . . . . . . . 11 ⊢ dom (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}
116	113, 115	sstri 4018	. . . . . . . . . 10 ⊢ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}
117	116	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})
118		suppssfifsupp 9449	. . . . . . . . 9 ⊢ ((((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ∈ V ∧ Fun (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ∧ (0g‘𝐺) ∈ V) ∧ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ Fin ∧ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) finSupp (0g‘𝐺))
119	109, 111, 112, 80, 117, 118	syl32anc 1378	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) finSupp (0g‘𝐺))
120	4, 72, 101, 80, 103, 119	gsumcl 19957	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) ∈ 𝐵)
121	120	fmpttd 7149	. . . . . 6 ⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))):𝑆⟶𝐵)
122	1, 2	psrbagconf1o 21972	. . . . . . . 8 ⊢ (𝐹 ∈ 𝐷 → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆)
123	3, 122	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆)
124		f1ocnv 6874	. . . . . . 7 ⊢ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆)
125		f1of 6862	. . . . . . 7 ⊢ (◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆⟶𝑆)
126	123, 124, 125	3syl 18	. . . . . 6 ⊢ (𝜑 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆⟶𝑆)
127	121, 126	fcod 6773	. . . . 5 ⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))):𝑆⟶𝐵)
128		coass 6296	. . . . . . . 8 ⊢ (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))))
129		f1ococnv2 6889	. . . . . . . . . 10 ⊢ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆 → ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ( I ↾ 𝑆))
130	123, 129	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ( I ↾ 𝑆))
131	130	coeq2d 5887	. . . . . . . 8 ⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)))
132	128, 131	eqtrid 2792	. . . . . . 7 ⊢ (𝜑 → (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)))
133		eqidd 2741	. . . . . . . . 9 ⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) = (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))
134		eqidd 2741	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
135		breq2 5170	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝑥 ∘r ≤ 𝑛 ↔ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)))
136	135	rabbidv 3451	. . . . . . . . . . 11 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} = {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})
137		ovex 7481	. . . . . . . . . . . . 13 ⊢ (𝑛 ∘f − 𝑗) ∈ V
138		psrass1lem.y	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 ∘f − 𝑗) → 𝑋 = 𝑌)
139	137, 138	csbie 3957	. . . . . . . . . . . 12 ⊢ ⦋(𝑛 ∘f − 𝑗) / 𝑘⦌𝑋 = 𝑌
140		oveq1 7455	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝑛 ∘f − 𝑗) = ((𝐹 ∘f − 𝑚) ∘f − 𝑗))
141	140	csbeq1d 3925	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → ⦋(𝑛 ∘f − 𝑗) / 𝑘⦌𝑋 = ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
142	139, 141	eqtr3id 2794	. . . . . . . . . . 11 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → 𝑌 = ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
143	136, 142	mpteq12dv 5257	. . . . . . . . . 10 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌) = (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))
144	143	oveq2d 7464	. . . . . . . . 9 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)) = (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))
145	77, 133, 134, 144	fmptco 7163	. . . . . . . 8 ⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))))
146	145	coeq1d 5886	. . . . . . 7 ⊢ (𝜑 → (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))))
147		coires1 6295	. . . . . . . . 9 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆)
148		ssid 4031	. . . . . . . . . 10 ⊢ 𝑆 ⊆ 𝑆
149		resmpt 6066	. . . . . . . . . 10 ⊢ (𝑆 ⊆ 𝑆 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
150	148, 149	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
151	147, 150	eqtri 2768	. . . . . . . 8 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
152	151	a1i 11	. . . . . . 7 ⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
153	132, 146, 152	3eqtr3d 2788	. . . . . 6 ⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
154	153	feq1d 6732	. . . . 5 ⊢ (𝜑 → (((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))):𝑆⟶𝐵 ↔ (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))):𝑆⟶𝐵))
155	127, 154	mpbid 232	. . . 4 ⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))):𝑆⟶𝐵)
156		rabexg 5355	. . . . . . . 8 ⊢ (𝐷 ∈ V → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ V)
157	105, 156	mp1i 13	. . . . . . 7 ⊢ (𝜑 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ V)
158	2, 157	eqeltrid 2848	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ V)
159	158	mptexd 7261	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∈ V)
160		funmpt 6616	. . . . . 6 ⊢ Fun (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
161	160	a1i 11	. . . . 5 ⊢ (𝜑 → Fun (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
162		fvexd 6935	. . . . 5 ⊢ (𝜑 → (0g‘𝐺) ∈ V)
163		suppssdm 8218	. . . . . . 7 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ dom (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
164		eqid 2740	. . . . . . . 8 ⊢ (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
165	164	dmmptss 6272	. . . . . . 7 ⊢ dom (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ⊆ 𝑆
166	163, 165	sstri 4018	. . . . . 6 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ 𝑆
167	166	a1i 11	. . . . 5 ⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ 𝑆)
168		suppssfifsupp 9449	. . . . 5 ⊢ ((((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∈ V ∧ Fun (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∧ (0g‘𝐺) ∈ V) ∧ (𝑆 ∈ Fin ∧ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ 𝑆)) → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) finSupp (0g‘𝐺))
169	159, 161, 162, 75, 167, 168	syl32anc 1378	. . . 4 ⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) finSupp (0g‘𝐺))
170	4, 72, 5, 75, 155, 169, 123	gsumf1o 19958	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))))
171	145	oveq2d 7464	. . 3 ⊢ (𝜑 → (𝐺 Σg ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
172	170, 171	eqtrd 2780	. 2 ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
173	5	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐺 ∈ CMnd)
174	105	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐷 ∈ V)
175		rabexg 5355	. . . . . . . 8 ⊢ (𝐷 ∈ V → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ V)
176		mptexg 7258	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ V → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∈ V)
177	174, 175, 176	3syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∈ V)
178		funmpt 6616	. . . . . . . 8 ⊢ Fun (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)
179	178	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → Fun (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋))
180		fvexd 6935	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (0g‘𝐺) ∈ V)
181		suppssdm 8218	. . . . . . . . 9 ⊢ ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ dom (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)
182		eqid 2740	. . . . . . . . . 10 ⊢ (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) = (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)
183	182	dmmptss 6272	. . . . . . . . 9 ⊢ dom (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}
184	181, 183	sstri 4018	. . . . . . . 8 ⊢ ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}
185	184	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
186		suppssfifsupp 9449	. . . . . . 7 ⊢ ((((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∈ V ∧ Fun (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∧ (0g‘𝐺) ∈ V) ∧ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ Fin ∧ ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) finSupp (0g‘𝐺))
187	177, 179, 180, 91, 185, 186	syl32anc 1378	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) finSupp (0g‘𝐺))
188	4, 72, 173, 91, 9, 187, 16	gsumf1o 19958	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)) = (𝐺 Σg ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)))))
189	65	oveq2d 7464	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)))) = (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))
190	188, 189	eqtrd 2780	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)) = (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))
191	190	mpteq2dva 5266	. . 3 ⊢ (𝜑 → (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋))) = (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))))
192	191	oveq2d 7464	. 2 ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
193	100, 172, 192	3eqtr4d 2790	1 ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  {crab 3443  Vcvv 3488  ⦋csb 3921   ⊆ wss 3976   class class class wbr 5166   ↦ cmpt 5249   I cid 5592   × cxp 5698  ^◡ccnv 5699  dom cdm 5700   ↾ cres 5702   “ cima 5703   ∘ ccom 5704  Fun wfun 6567  ⟶wf 6569  –1-1-onto→wf1o 6572  ‘cfv 6573  (class class class)co 7448   ∈ cmpo 7450   ∘_f cof 7712   ∘_r cofr 7713   supp csupp 8201   ↑_m cmap 8884  Fincfn 9003   finSupp cfsupp 9431  ℂcc 11182   ≤ cle 11325   − cmin 11520  ℕcn 12293  ℕ₀cn0 12553  Basecbs 17258  0_gc0g 17499   Σ_g cgsu 17500  CMndccmn 19822

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-iin 5018  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-of 7714  df-ofr 7715  df-om 7904  df-1st 8030  df-2nd 8031  df-supp 8202  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-er 8763  df-map 8886  df-pm 8887  df-ixp 8956  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-fsupp 9432  df-oi 9579  df-card 10008  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-nn 12294  df-2 12356  df-n0 12554  df-z 12640  df-uz 12904  df-fz 13568  df-fzo 13712  df-seq 14053  df-hash 14380  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-ress 17288  df-plusg 17324  df-0g 17501  df-gsum 17502  df-mre 17644  df-mrc 17645  df-acs 17647  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-submnd 18819  df-mulg 19108  df-cntz 19357  df-cmn 19824

This theorem is referenced by:  psrass1  22007