Theorem psrass1lemOLD 21873

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

Hypotheses

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

Assertion

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

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

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

Proof of Theorem psrass1lemOLD

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

Step	Hyp	Ref	Expression
1		psrbag.d	. . . 4 ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
2		psrbagconf1o.s	. . . 4 ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹}
3		gsumbagdiagOLD.i	. . . 4 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
4		gsumbagdiagOLD.f	. . . 4 ⊢ (𝜑 → 𝐹 ∈ 𝐷)
5		gsumbagdiagOLD.b	. . . 4 ⊢ 𝐵 = (Base‘𝐺)
6		gsumbagdiagOLD.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ CMnd)
7	1, 2, 3, 4	gsumbagdiaglemOLD 21871	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}))
8		gsumbagdiagOLD.x	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑋 ∈ 𝐵)
9	8	anassrs 466	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑋 ∈ 𝐵)
10	9	fmpttd 7118	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵)
11	3	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐼 ∈ 𝑉)
12	2	ssrab3 4073	. . . . . . . . . . . 12 ⊢ 𝑆 ⊆ 𝐷
13	4	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐹 ∈ 𝐷)
14		simpr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝑗 ∈ 𝑆)
15	1, 2	psrbagconclOLD 21867	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘f − 𝑗) ∈ 𝑆)
16	11, 13, 14, 15	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘f − 𝑗) ∈ 𝑆)
17	12, 16	sselid 3971	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘f − 𝑗) ∈ 𝐷)
18		eqid 2725	. . . . . . . . . . . 12 ⊢ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} = {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}
19	1, 18	psrbagconf1oOLD 21870	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘f − 𝑗) ∈ 𝐷) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}–1-1-onto→{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
20	11, 17, 19	syl2anc 582	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}–1-1-onto→{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
21		f1of 6832	. . . . . . . . . 10 ⊢ ((𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}–1-1-onto→{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
22	20, 21	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
23		fco 6741	. . . . . . . . 9 ⊢ (((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵 ∧ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚))):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵)
24	10, 22, 23	syl2anc 582	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚))):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵)
25	11	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐼 ∈ 𝑉)
26	13	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐹 ∈ 𝐷)
27	1	psrbagfOLD 21851	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → 𝐹:𝐼⟶ℕ0)
28	25, 26, 27	syl2anc 582	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐹:𝐼⟶ℕ0)
29	28	ffvelcdmda 7087	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈ ℕ0)
30	14	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗 ∈ 𝑆)
31	12, 30	sselid 3971	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗 ∈ 𝐷)
32	1	psrbagfOLD 21851	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐷) → 𝑗:𝐼⟶ℕ0)
33	25, 31, 32	syl2anc 582	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗:𝐼⟶ℕ0)
34	33	ffvelcdmda 7087	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝑗‘𝑧) ∈ ℕ0)
35		ssrab2 4070	. . . . . . . . . . . . . . . . 17 ⊢ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ⊆ 𝐷
36		simpr 483	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
37	35, 36	sselid 3971	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚 ∈ 𝐷)
38	1	psrbagfOLD 21851	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑚 ∈ 𝐷) → 𝑚:𝐼⟶ℕ0)
39	25, 37, 38	syl2anc 582	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚:𝐼⟶ℕ0)
40	39	ffvelcdmda 7087	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝑚‘𝑧) ∈ ℕ0)
41		nn0cn 12507	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑧) ∈ ℕ0 → (𝐹‘𝑧) ∈ ℂ)
42		nn0cn 12507	. . . . . . . . . . . . . . 15 ⊢ ((𝑗‘𝑧) ∈ ℕ0 → (𝑗‘𝑧) ∈ ℂ)
43		nn0cn 12507	. . . . . . . . . . . . . . 15 ⊢ ((𝑚‘𝑧) ∈ ℕ0 → (𝑚‘𝑧) ∈ ℂ)
44		sub32 11519	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑧) ∈ ℂ ∧ (𝑗‘𝑧) ∈ ℂ ∧ (𝑚‘𝑧) ∈ ℂ) → (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧)) = (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧)))
45	41, 42, 43, 44	syl3an 1157	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑧) ∈ ℕ0 ∧ (𝑗‘𝑧) ∈ ℕ0 ∧ (𝑚‘𝑧) ∈ ℕ0) → (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧)) = (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧)))
46	29, 34, 40, 45	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧)) = (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧)))
47	46	mpteq2dva 5244	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧))) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧))))
48		ovexd 7448	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑗‘𝑧)) ∈ V)
49	28	feqmptd 6960	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐹 = (𝑧 ∈ 𝐼 ↦ (𝐹‘𝑧)))
50	33	feqmptd 6960	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗 = (𝑧 ∈ 𝐼 ↦ (𝑗‘𝑧)))
51	25, 29, 34, 49, 50	offval2 7699	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝐹 ∘f − 𝑗) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑗‘𝑧))))
52	39	feqmptd 6960	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚 = (𝑧 ∈ 𝐼 ↦ (𝑚‘𝑧)))
53	25, 48, 40, 51, 52	offval2 7699	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f − 𝑚) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧))))
54		ovexd 7448	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑚‘𝑧)) ∈ V)
55	25, 29, 40, 49, 52	offval2 7699	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝐹 ∘f − 𝑚) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑚‘𝑧))))
56	25, 54, 34, 55, 50	offval2 7699	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑚) ∘f − 𝑗) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧))))
57	47, 53, 56	3eqtr4d 2775	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f − 𝑚) = ((𝐹 ∘f − 𝑚) ∘f − 𝑗))
58	17	adantr 479	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝐹 ∘f − 𝑗) ∈ 𝐷)
59	1, 18	psrbagconclOLD 21867	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘f − 𝑗) ∈ 𝐷 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f − 𝑚) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
60	25, 58, 36, 59	syl3anc 1368	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f − 𝑚) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
61	57, 60	eqeltrrd 2826	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑚) ∘f − 𝑗) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
62	57	mpteq2dva 5244	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)) = (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑚) ∘f − 𝑗)))
63		nfcv 2892	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛𝑋
64		nfcsb1v 3911	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⦋𝑛 / 𝑘⦌𝑋
65		csbeq1a 3900	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → 𝑋 = ⦋𝑛 / 𝑘⦌𝑋)
66	63, 64, 65	cbvmpt 5255	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋𝑛 / 𝑘⦌𝑋)
67	66	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋𝑛 / 𝑘⦌𝑋))
68		csbeq1 3889	. . . . . . . . . 10 ⊢ (𝑛 = ((𝐹 ∘f − 𝑚) ∘f − 𝑗) → ⦋𝑛 / 𝑘⦌𝑋 = ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
69	61, 62, 67, 68	fmptco 7132	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚))) = (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))
70	69	feq1d 6702	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚))):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵 ↔ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵))
71	24, 70	mpbid 231	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵)
72	71	fvmptelcdm 7116	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵)
73	72	anasss 465	. . . . 5 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵)
74	7, 73	syldan 589	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵)
75	1, 2, 3, 4, 5, 6, 74	gsumbagdiagOLD 21872	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆, 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑗 ∈ 𝑆, 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))
76		eqid 2725	. . . 4 ⊢ (0g‘𝐺) = (0g‘𝐺)
77	1	psrbaglefiOLD 21865	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ Fin)
78	3, 4, 77	syl2anc 582	. . . . 5 ⊢ (𝜑 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ Fin)
79	2, 78	eqeltrid 2829	. . . 4 ⊢ (𝜑 → 𝑆 ∈ Fin)
80	3	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐼 ∈ 𝑉)
81	4	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐹 ∈ 𝐷)
82		simpr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝑚 ∈ 𝑆)
83	1, 2	psrbagconclOLD 21867	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘f − 𝑚) ∈ 𝑆)
84	80, 81, 82, 83	syl3anc 1368	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘f − 𝑚) ∈ 𝑆)
85	12, 84	sselid 3971	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘f − 𝑚) ∈ 𝐷)
86	1	psrbaglefiOLD 21865	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘f − 𝑚) ∈ 𝐷) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ Fin)
87	80, 85, 86	syl2anc 582	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ Fin)
88		xpfi 9336	. . . . 5 ⊢ ((𝑆 ∈ Fin ∧ 𝑆 ∈ Fin) → (𝑆 × 𝑆) ∈ Fin)
89	79, 79, 88	syl2anc 582	. . . 4 ⊢ (𝜑 → (𝑆 × 𝑆) ∈ Fin)
90		simprl 769	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → 𝑚 ∈ 𝑆)
91	7	simpld 493	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → 𝑗 ∈ 𝑆)
92		brxp 5722	. . . . . . 7 ⊢ (𝑚(𝑆 × 𝑆)𝑗 ↔ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ 𝑆))
93	90, 91, 92	sylanbrc 581	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → 𝑚(𝑆 × 𝑆)𝑗)
94	93	pm2.24d 151	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → (¬ 𝑚(𝑆 × 𝑆)𝑗 → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺)))
95	94	impr 453	. . . 4 ⊢ ((𝜑 ∧ ((𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}) ∧ ¬ 𝑚(𝑆 × 𝑆)𝑗)) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺))
96	5, 76, 6, 79, 87, 74, 89, 95	gsum2d2 19928	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆, 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
97	1	psrbaglefiOLD 21865	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘f − 𝑗) ∈ 𝐷) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ Fin)
98	11, 17, 97	syl2anc 582	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ Fin)
99		simprl 769	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑗 ∈ 𝑆)
100	1, 2, 3, 4	gsumbagdiaglemOLD 21871	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}))
101	100	simpld 493	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑚 ∈ 𝑆)
102		brxp 5722	. . . . . . 7 ⊢ (𝑗(𝑆 × 𝑆)𝑚 ↔ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ 𝑆))
103	99, 101, 102	sylanbrc 581	. . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑗(𝑆 × 𝑆)𝑚)
104	103	pm2.24d 151	. . . . 5 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → (¬ 𝑗(𝑆 × 𝑆)𝑚 → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺)))
105	104	impr 453	. . . 4 ⊢ ((𝜑 ∧ ((𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ ¬ 𝑗(𝑆 × 𝑆)𝑚)) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺))
106	5, 76, 6, 79, 98, 73, 89, 105	gsum2d2 19928	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝑆, 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
107	75, 96, 106	3eqtr3d 2773	. 2 ⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
108	6	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐺 ∈ CMnd)
109	74	anassrs 466	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ 𝑆) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵)
110	109	fmpttd 7118	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}⟶𝐵)
111		ovex 7446	. . . . . . . . . . . 12 ⊢ (ℕ0 ↑m 𝐼) ∈ V
112	1, 111	rabex2 5332	. . . . . . . . . . 11 ⊢ 𝐷 ∈ V
113	112	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐷 ∈ V)
114		rabexg 5329	. . . . . . . . . 10 ⊢ (𝐷 ∈ V → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ V)
115		mptexg 7227	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ V → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ∈ V)
116	113, 114, 115	3syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ∈ V)
117		funmpt 6586	. . . . . . . . . 10 ⊢ Fun (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
118	117	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → Fun (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))
119		fvexd 6905	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (0g‘𝐺) ∈ V)
120		suppssdm 8175	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ dom (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
121		eqid 2725	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) = (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
122	121	dmmptss 6241	. . . . . . . . . . 11 ⊢ dom (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}
123	120, 122	sstri 3983	. . . . . . . . . 10 ⊢ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}
124	123	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})
125		suppssfifsupp 9398	. . . . . . . . 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‘𝐺))
126	116, 118, 119, 87, 124, 125	syl32anc 1375	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) finSupp (0g‘𝐺))
127	5, 76, 108, 87, 110, 126	gsumcl 19869	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) ∈ 𝐵)
128	127	fmpttd 7118	. . . . . 6 ⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))):𝑆⟶𝐵)
129	1, 2	psrbagconf1oOLD 21870	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆)
130	3, 4, 129	syl2anc 582	. . . . . . 7 ⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆)
131		f1ocnv 6844	. . . . . . 7 ⊢ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆)
132		f1of 6832	. . . . . . 7 ⊢ (◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆⟶𝑆)
133	130, 131, 132	3syl 18	. . . . . 6 ⊢ (𝜑 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆⟶𝑆)
134		fco 6741	. . . . . 6 ⊢ (((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))):𝑆⟶𝐵 ∧ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆⟶𝑆) → ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))):𝑆⟶𝐵)
135	128, 133, 134	syl2anc 582	. . . . 5 ⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))):𝑆⟶𝐵)
136		coass 6265	. . . . . . . 8 ⊢ (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))))
137		f1ococnv2 6859	. . . . . . . . . 10 ⊢ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆 → ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ( I ↾ 𝑆))
138	130, 137	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ( I ↾ 𝑆))
139	138	coeq2d 5860	. . . . . . . 8 ⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)))
140	136, 139	eqtrid 2777	. . . . . . 7 ⊢ (𝜑 → (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)))
141		eqidd 2726	. . . . . . . . 9 ⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) = (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))
142		eqidd 2726	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
143		breq2 5148	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝑥 ∘r ≤ 𝑛 ↔ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)))
144	143	rabbidv 3427	. . . . . . . . . . 11 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} = {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})
145		ovex 7446	. . . . . . . . . . . . 13 ⊢ (𝑛 ∘f − 𝑗) ∈ V
146		psrass1lemOLD.y	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 ∘f − 𝑗) → 𝑋 = 𝑌)
147	145, 146	csbie 3922	. . . . . . . . . . . 12 ⊢ ⦋(𝑛 ∘f − 𝑗) / 𝑘⦌𝑋 = 𝑌
148		oveq1 7420	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝑛 ∘f − 𝑗) = ((𝐹 ∘f − 𝑚) ∘f − 𝑗))
149	148	csbeq1d 3890	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → ⦋(𝑛 ∘f − 𝑗) / 𝑘⦌𝑋 = ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
150	147, 149	eqtr3id 2779	. . . . . . . . . . 11 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → 𝑌 = ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
151	144, 150	mpteq12dv 5235	. . . . . . . . . 10 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌) = (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))
152	151	oveq2d 7429	. . . . . . . . 9 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)) = (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))
153	84, 141, 142, 152	fmptco 7132	. . . . . . . 8 ⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))))
154	153	coeq1d 5859	. . . . . . 7 ⊢ (𝜑 → (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))))
155		coires1 6264	. . . . . . . . 9 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆)
156		ssid 3996	. . . . . . . . . 10 ⊢ 𝑆 ⊆ 𝑆
157		resmpt 6037	. . . . . . . . . 10 ⊢ (𝑆 ⊆ 𝑆 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
158	156, 157	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
159	155, 158	eqtri 2753	. . . . . . . 8 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
160	159	a1i 11	. . . . . . 7 ⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
161	140, 154, 160	3eqtr3d 2773	. . . . . 6 ⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
162	161	feq1d 6702	. . . . 5 ⊢ (𝜑 → (((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))):𝑆⟶𝐵 ↔ (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))):𝑆⟶𝐵))
163	135, 162	mpbid 231	. . . 4 ⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))):𝑆⟶𝐵)
164		rabexg 5329	. . . . . . . 8 ⊢ (𝐷 ∈ V → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ V)
165	112, 164	mp1i 13	. . . . . . 7 ⊢ (𝜑 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ V)
166	2, 165	eqeltrid 2829	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ V)
167	166	mptexd 7230	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∈ V)
168		funmpt 6586	. . . . . 6 ⊢ Fun (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
169	168	a1i 11	. . . . 5 ⊢ (𝜑 → Fun (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
170		fvexd 6905	. . . . 5 ⊢ (𝜑 → (0g‘𝐺) ∈ V)
171		suppssdm 8175	. . . . . . 7 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ dom (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
172		eqid 2725	. . . . . . . 8 ⊢ (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
173	172	dmmptss 6241	. . . . . . 7 ⊢ dom (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ⊆ 𝑆
174	171, 173	sstri 3983	. . . . . 6 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ 𝑆
175	174	a1i 11	. . . . 5 ⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ 𝑆)
176		suppssfifsupp 9398	. . . . 5 ⊢ ((((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∈ V ∧ Fun (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∧ (0g‘𝐺) ∈ V) ∧ (𝑆 ∈ Fin ∧ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ 𝑆)) → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) finSupp (0g‘𝐺))
177	167, 169, 170, 79, 175, 176	syl32anc 1375	. . . 4 ⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) finSupp (0g‘𝐺))
178	5, 76, 6, 79, 163, 177, 130	gsumf1o 19870	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))))
179	153	oveq2d 7429	. . 3 ⊢ (𝜑 → (𝐺 Σg ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
180	178, 179	eqtrd 2765	. 2 ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
181	6	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐺 ∈ CMnd)
182	112	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐷 ∈ V)
183		rabexg 5329	. . . . . . . 8 ⊢ (𝐷 ∈ V → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ V)
184		mptexg 7227	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ V → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∈ V)
185	182, 183, 184	3syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∈ V)
186		funmpt 6586	. . . . . . . 8 ⊢ Fun (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)
187	186	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → Fun (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋))
188		fvexd 6905	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (0g‘𝐺) ∈ V)
189		suppssdm 8175	. . . . . . . . 9 ⊢ ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ dom (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)
190		eqid 2725	. . . . . . . . . 10 ⊢ (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) = (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)
191	190	dmmptss 6241	. . . . . . . . 9 ⊢ dom (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}
192	189, 191	sstri 3983	. . . . . . . 8 ⊢ ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}
193	192	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
194		suppssfifsupp 9398	. . . . . . 7 ⊢ ((((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∈ V ∧ Fun (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∧ (0g‘𝐺) ∈ V) ∧ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ Fin ∧ ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) finSupp (0g‘𝐺))
195	185, 187, 188, 98, 193, 194	syl32anc 1375	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) finSupp (0g‘𝐺))
196	5, 76, 181, 98, 10, 195, 20	gsumf1o 19870	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)) = (𝐺 Σg ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)))))
197	69	oveq2d 7429	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)))) = (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))
198	196, 197	eqtrd 2765	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)) = (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))
199	198	mpteq2dva 5244	. . 3 ⊢ (𝜑 → (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋))) = (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))))
200	199	oveq2d 7429	. 2 ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
201	107, 180, 200	3eqtr4d 2775	1 ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098  {crab 3419  Vcvv 3463  ⦋csb 3886   ⊆ wss 3941   class class class wbr 5144   ↦ cmpt 5227   I cid 5570   × cxp 5671  ^◡ccnv 5672  dom cdm 5673   ↾ cres 5675   “ cima 5676   ∘ ccom 5677  Fun wfun 6537  ⟶wf 6539  –1-1-onto→wf1o 6542  ‘cfv 6543  (class class class)co 7413   ∈ cmpo 7415   ∘_f cof 7677   ∘_r cofr 7678   supp csupp 8158   ↑_m cmap 8838  Fincfn 8957   finSupp cfsupp 9380  ℂcc 11131   ≤ cle 11274   − cmin 11469  ℕcn 12237  ℕ₀cn0 12497  Basecbs 17174  0_gc0g 17415   Σ_g cgsu 17416  CMndccmn 19734

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-int 4946  df-iun 4994  df-iin 4995  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-se 5629  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7679  df-ofr 7680  df-om 7866  df-1st 7987  df-2nd 7988  df-supp 8159  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-map 8840  df-pm 8841  df-ixp 8910  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fsupp 9381  df-oi 9528  df-card 9957  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-nn 12238  df-2 12300  df-n0 12498  df-z 12584  df-uz 12848  df-fz 13512  df-fzo 13655  df-seq 13994  df-hash 14317  df-sets 17127  df-slot 17145  df-ndx 17157  df-base 17175  df-ress 17204  df-plusg 17240  df-0g 17417  df-gsum 17418  df-mre 17560  df-mrc 17561  df-acs 17563  df-mgm 18594  df-sgrp 18673  df-mnd 18689  df-submnd 18735  df-mulg 19023  df-cntz 19267  df-cmn 19736

This theorem is referenced by: (None)