Theorem psrass1lem 20615

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

Hypotheses

Ref	Expression
psrbag.d	⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
psrbagconf1o.1	⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹}
gsumbagdiag.i	⊢ (𝜑 → 𝐼 ∈ 𝑉)
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		psrbag.d	. . . 4 ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
2		psrbagconf1o.1	. . . 4 ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹}
3		gsumbagdiag.i	. . . 4 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
4		gsumbagdiag.f	. . . 4 ⊢ (𝜑 → 𝐹 ∈ 𝐷)
5		gsumbagdiag.b	. . . 4 ⊢ 𝐵 = (Base‘𝐺)
6		gsumbagdiag.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ CMnd)
7	1, 2, 3, 4	gsumbagdiaglem 20613	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}))
8		gsumbagdiag.x	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑋 ∈ 𝐵)
9	8	anassrs 471	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑋 ∈ 𝐵)
10	9	fmpttd 6856	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵)
11	3	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐼 ∈ 𝑉)
12	2	ssrab3 4008	. . . . . . . . . . . 12 ⊢ 𝑆 ⊆ 𝐷
13	4	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐹 ∈ 𝐷)
14		simpr 488	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝑗 ∈ 𝑆)
15	1, 2	psrbagconcl 20611	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘f − 𝑗) ∈ 𝑆)
16	11, 13, 14, 15	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘f − 𝑗) ∈ 𝑆)
17	12, 16	sseldi 3913	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘f − 𝑗) ∈ 𝐷)
18		eqid 2798	. . . . . . . . . . . 12 ⊢ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} = {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}
19	1, 18	psrbagconf1o 20612	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘f − 𝑗) ∈ 𝐷) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}–1-1-onto→{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
20	11, 17, 19	syl2anc 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}–1-1-onto→{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
21		f1of 6590	. . . . . . . . . 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 6505	. . . . . . . . 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 587	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚))):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵)
25	11	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐼 ∈ 𝑉)
26	13	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐹 ∈ 𝐷)
27	1	psrbagf 20603	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → 𝐹:𝐼⟶ℕ0)
28	25, 26, 27	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐹:𝐼⟶ℕ0)
29	28	ffvelrnda 6828	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈ ℕ0)
30	14	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗 ∈ 𝑆)
31	12, 30	sseldi 3913	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗 ∈ 𝐷)
32	1	psrbagf 20603	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐷) → 𝑗:𝐼⟶ℕ0)
33	25, 31, 32	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗:𝐼⟶ℕ0)
34	33	ffvelrnda 6828	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝑗‘𝑧) ∈ ℕ0)
35		ssrab2 4007	. . . . . . . . . . . . . . . . 17 ⊢ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ⊆ 𝐷
36		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
37	35, 36	sseldi 3913	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚 ∈ 𝐷)
38	1	psrbagf 20603	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑚 ∈ 𝐷) → 𝑚:𝐼⟶ℕ0)
39	25, 37, 38	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚:𝐼⟶ℕ0)
40	39	ffvelrnda 6828	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝑚‘𝑧) ∈ ℕ0)
41		nn0cn 11895	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑧) ∈ ℕ0 → (𝐹‘𝑧) ∈ ℂ)
42		nn0cn 11895	. . . . . . . . . . . . . . 15 ⊢ ((𝑗‘𝑧) ∈ ℕ0 → (𝑗‘𝑧) ∈ ℂ)
43		nn0cn 11895	. . . . . . . . . . . . . . 15 ⊢ ((𝑚‘𝑧) ∈ ℕ0 → (𝑚‘𝑧) ∈ ℂ)
44		sub32 10909	. . . . . . . . . . . . . . 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 5125	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧))) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧))))
48		ovexd 7170	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑗‘𝑧)) ∈ V)
49	28	feqmptd 6708	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐹 = (𝑧 ∈ 𝐼 ↦ (𝐹‘𝑧)))
50	33	feqmptd 6708	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗 = (𝑧 ∈ 𝐼 ↦ (𝑗‘𝑧)))
51	25, 29, 34, 49, 50	offval2 7406	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝐹 ∘f − 𝑗) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑗‘𝑧))))
52	39	feqmptd 6708	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚 = (𝑧 ∈ 𝐼 ↦ (𝑚‘𝑧)))
53	25, 48, 40, 51, 52	offval2 7406	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f − 𝑚) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧))))
54		ovexd 7170	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑚‘𝑧)) ∈ V)
55	25, 29, 40, 49, 52	offval2 7406	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝐹 ∘f − 𝑚) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑚‘𝑧))))
56	25, 54, 34, 55, 50	offval2 7406	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑚) ∘f − 𝑗) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧))))
57	47, 53, 56	3eqtr4d 2843	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f − 𝑚) = ((𝐹 ∘f − 𝑚) ∘f − 𝑗))
58	17	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝐹 ∘f − 𝑗) ∈ 𝐷)
59	1, 18	psrbagconcl 20611	. . . . . . . . . . . 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 2891	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑚) ∘f − 𝑗) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
62	57	mpteq2dva 5125	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)) = (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑚) ∘f − 𝑗)))
63		nfcv 2955	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛𝑋
64		nfcsb1v 3852	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⦋𝑛 / 𝑘⦌𝑋
65		csbeq1a 3842	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → 𝑋 = ⦋𝑛 / 𝑘⦌𝑋)
66	63, 64, 65	cbvmpt 5131	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋𝑛 / 𝑘⦌𝑋)
67	66	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋𝑛 / 𝑘⦌𝑋))
68		csbeq1 3831	. . . . . . . . . 10 ⊢ (𝑛 = ((𝐹 ∘f − 𝑚) ∘f − 𝑗) → ⦋𝑛 / 𝑘⦌𝑋 = ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
69	61, 62, 67, 68	fmptco 6868	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚))) = (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))
70	69	feq1d 6472	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚))):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵 ↔ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵))
71	24, 70	mpbid 235	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵)
72	71	fvmptelrn 6854	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵)
73	72	anasss 470	. . . . 5 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵)
74	7, 73	syldan 594	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵)
75	1, 2, 3, 4, 5, 6, 74	gsumbagdiag 20614	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆, 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑗 ∈ 𝑆, 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))
76		eqid 2798	. . . 4 ⊢ (0g‘𝐺) = (0g‘𝐺)
77	1	psrbaglefi 20610	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ Fin)
78	3, 4, 77	syl2anc 587	. . . . 5 ⊢ (𝜑 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ Fin)
79	2, 78	eqeltrid 2894	. . . 4 ⊢ (𝜑 → 𝑆 ∈ Fin)
80	3	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐼 ∈ 𝑉)
81	4	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐹 ∈ 𝐷)
82		simpr 488	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝑚 ∈ 𝑆)
83	1, 2	psrbagconcl 20611	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘f − 𝑚) ∈ 𝑆)
84	80, 81, 82, 83	syl3anc 1368	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘f − 𝑚) ∈ 𝑆)
85	12, 84	sseldi 3913	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘f − 𝑚) ∈ 𝐷)
86	1	psrbaglefi 20610	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘f − 𝑚) ∈ 𝐷) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ Fin)
87	80, 85, 86	syl2anc 587	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ Fin)
88		xpfi 8773	. . . . 5 ⊢ ((𝑆 ∈ Fin ∧ 𝑆 ∈ Fin) → (𝑆 × 𝑆) ∈ Fin)
89	79, 79, 88	syl2anc 587	. . . 4 ⊢ (𝜑 → (𝑆 × 𝑆) ∈ Fin)
90		simprl 770	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → 𝑚 ∈ 𝑆)
91	7	simpld 498	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → 𝑗 ∈ 𝑆)
92		brxp 5565	. . . . . . 7 ⊢ (𝑚(𝑆 × 𝑆)𝑗 ↔ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ 𝑆))
93	90, 91, 92	sylanbrc 586	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → 𝑚(𝑆 × 𝑆)𝑗)
94	93	pm2.24d 154	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → (¬ 𝑚(𝑆 × 𝑆)𝑗 → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺)))
95	94	impr 458	. . . 4 ⊢ ((𝜑 ∧ ((𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}) ∧ ¬ 𝑚(𝑆 × 𝑆)𝑗)) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺))
96	5, 76, 6, 79, 87, 74, 89, 95	gsum2d2 19087	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆, 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
97	1	psrbaglefi 20610	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘f − 𝑗) ∈ 𝐷) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ Fin)
98	11, 17, 97	syl2anc 587	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ Fin)
99		simprl 770	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑗 ∈ 𝑆)
100	1, 2, 3, 4	gsumbagdiaglem 20613	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}))
101	100	simpld 498	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑚 ∈ 𝑆)
102		brxp 5565	. . . . . . 7 ⊢ (𝑗(𝑆 × 𝑆)𝑚 ↔ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ 𝑆))
103	99, 101, 102	sylanbrc 586	. . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑗(𝑆 × 𝑆)𝑚)
104	103	pm2.24d 154	. . . . 5 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → (¬ 𝑗(𝑆 × 𝑆)𝑚 → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺)))
105	104	impr 458	. . . 4 ⊢ ((𝜑 ∧ ((𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ ¬ 𝑗(𝑆 × 𝑆)𝑚)) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺))
106	5, 76, 6, 79, 98, 73, 89, 105	gsum2d2 19087	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝑆, 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
107	75, 96, 106	3eqtr3d 2841	. 2 ⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
108	6	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐺 ∈ CMnd)
109	74	anassrs 471	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ 𝑆) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵)
110	109	fmpttd 6856	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}⟶𝐵)
111		ovex 7168	. . . . . . . . . . . 12 ⊢ (ℕ0 ↑m 𝐼) ∈ V
112	1, 111	rabex2 5201	. . . . . . . . . . 11 ⊢ 𝐷 ∈ V
113	112	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐷 ∈ V)
114		rabexg 5198	. . . . . . . . . 10 ⊢ (𝐷 ∈ V → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ V)
115		mptexg 6961	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ V → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ∈ V)
116	113, 114, 115	3syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ∈ V)
117		funmpt 6362	. . . . . . . . . 10 ⊢ Fun (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
118	117	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → Fun (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))
119		fvexd 6660	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (0g‘𝐺) ∈ V)
120		suppssdm 7826	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ dom (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
121		eqid 2798	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) = (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
122	121	dmmptss 6062	. . . . . . . . . . 11 ⊢ dom (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}
123	120, 122	sstri 3924	. . . . . . . . . 10 ⊢ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}
124	123	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})
125		suppssfifsupp 8832	. . . . . . . . 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 19028	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) ∈ 𝐵)
128	127	fmpttd 6856	. . . . . 6 ⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))):𝑆⟶𝐵)
129	1, 2	psrbagconf1o 20612	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆)
130	3, 4, 129	syl2anc 587	. . . . . . 7 ⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆)
131		f1ocnv 6602	. . . . . . 7 ⊢ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆)
132		f1of 6590	. . . . . . 7 ⊢ (◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆⟶𝑆)
133	130, 131, 132	3syl 18	. . . . . 6 ⊢ (𝜑 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆⟶𝑆)
134		fco 6505	. . . . . 6 ⊢ (((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))):𝑆⟶𝐵 ∧ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆⟶𝑆) → ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))):𝑆⟶𝐵)
135	128, 133, 134	syl2anc 587	. . . . 5 ⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))):𝑆⟶𝐵)
136		coass 6085	. . . . . . . 8 ⊢ (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))))
137		f1ococnv2 6616	. . . . . . . . . 10 ⊢ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆 → ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ( I ↾ 𝑆))
138	130, 137	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ( I ↾ 𝑆))
139	138	coeq2d 5697	. . . . . . . 8 ⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)))
140	136, 139	syl5eq 2845	. . . . . . 7 ⊢ (𝜑 → (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)))
141		eqidd 2799	. . . . . . . . 9 ⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) = (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))
142		eqidd 2799	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
143		breq2 5034	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝑥 ∘r ≤ 𝑛 ↔ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)))
144	143	rabbidv 3427	. . . . . . . . . . 11 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} = {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})
145		ovex 7168	. . . . . . . . . . . . 13 ⊢ (𝑛 ∘f − 𝑗) ∈ V
146		psrass1lem.y	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 ∘f − 𝑗) → 𝑋 = 𝑌)
147	145, 146	csbie 3863	. . . . . . . . . . . 12 ⊢ ⦋(𝑛 ∘f − 𝑗) / 𝑘⦌𝑋 = 𝑌
148		oveq1 7142	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝑛 ∘f − 𝑗) = ((𝐹 ∘f − 𝑚) ∘f − 𝑗))
149	148	csbeq1d 3832	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → ⦋(𝑛 ∘f − 𝑗) / 𝑘⦌𝑋 = ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
150	147, 149	syl5eqr 2847	. . . . . . . . . . 11 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → 𝑌 = ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
151	144, 150	mpteq12dv 5115	. . . . . . . . . 10 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌) = (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))
152	151	oveq2d 7151	. . . . . . . . 9 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)) = (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))
153	84, 141, 142, 152	fmptco 6868	. . . . . . . 8 ⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))))
154	153	coeq1d 5696	. . . . . . 7 ⊢ (𝜑 → (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))))
155		coires1 6084	. . . . . . . . 9 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆)
156		ssid 3937	. . . . . . . . . 10 ⊢ 𝑆 ⊆ 𝑆
157		resmpt 5872	. . . . . . . . . 10 ⊢ (𝑆 ⊆ 𝑆 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
158	156, 157	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
159	155, 158	eqtri 2821	. . . . . . . 8 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
160	159	a1i 11	. . . . . . 7 ⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
161	140, 154, 160	3eqtr3d 2841	. . . . . 6 ⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
162	161	feq1d 6472	. . . . 5 ⊢ (𝜑 → (((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))):𝑆⟶𝐵 ↔ (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))):𝑆⟶𝐵))
163	135, 162	mpbid 235	. . . 4 ⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))):𝑆⟶𝐵)
164		rabexg 5198	. . . . . . . 8 ⊢ (𝐷 ∈ V → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ V)
165	112, 164	mp1i 13	. . . . . . 7 ⊢ (𝜑 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ V)
166	2, 165	eqeltrid 2894	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ V)
167	166	mptexd 6964	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∈ V)
168		funmpt 6362	. . . . . 6 ⊢ Fun (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
169	168	a1i 11	. . . . 5 ⊢ (𝜑 → Fun (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
170		fvexd 6660	. . . . 5 ⊢ (𝜑 → (0g‘𝐺) ∈ V)
171		suppssdm 7826	. . . . . . 7 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ dom (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
172		eqid 2798	. . . . . . . 8 ⊢ (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
173	172	dmmptss 6062	. . . . . . 7 ⊢ dom (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ⊆ 𝑆
174	171, 173	sstri 3924	. . . . . 6 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ 𝑆
175	174	a1i 11	. . . . 5 ⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ 𝑆)
176		suppssfifsupp 8832	. . . . 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 19029	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))))
179	153	oveq2d 7151	. . 3 ⊢ (𝜑 → (𝐺 Σg ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
180	178, 179	eqtrd 2833	. 2 ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
181	6	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐺 ∈ CMnd)
182	112	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐷 ∈ V)
183		rabexg 5198	. . . . . . . 8 ⊢ (𝐷 ∈ V → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ V)
184		mptexg 6961	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ V → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∈ V)
185	182, 183, 184	3syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∈ V)
186		funmpt 6362	. . . . . . . 8 ⊢ Fun (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)
187	186	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → Fun (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋))
188		fvexd 6660	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (0g‘𝐺) ∈ V)
189		suppssdm 7826	. . . . . . . . 9 ⊢ ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ dom (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)
190		eqid 2798	. . . . . . . . . 10 ⊢ (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) = (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)
191	190	dmmptss 6062	. . . . . . . . 9 ⊢ dom (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}
192	189, 191	sstri 3924	. . . . . . . 8 ⊢ ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}
193	192	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
194		suppssfifsupp 8832	. . . . . . 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 19029	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)) = (𝐺 Σg ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)))))
197	69	oveq2d 7151	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)))) = (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))
198	196, 197	eqtrd 2833	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)) = (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))
199	198	mpteq2dva 5125	. . 3 ⊢ (𝜑 → (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋))) = (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))))
200	199	oveq2d 7151	. 2 ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
201	107, 180, 200	3eqtr4d 2843	1 ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {crab 3110  Vcvv 3441  ⦋csb 3828   ⊆ wss 3881   class class class wbr 5030   ↦ cmpt 5110   I cid 5424   × cxp 5517  ^◡ccnv 5518  dom cdm 5519   ↾ cres 5521   “ cima 5522   ∘ ccom 5523  Fun wfun 6318  ⟶wf 6320  –1-1-onto→wf1o 6323  ‘cfv 6324  (class class class)co 7135   ∈ cmpo 7137   ∘_f cof 7387   ∘_r cofr 7388   supp csupp 7813   ↑_m cmap 8389  Fincfn 8492   finSupp cfsupp 8817  ℂcc 10524   ≤ cle 10665   − cmin 10859  ℕcn 11625  ℕ₀cn0 11885  Basecbs 16475  0_gc0g 16705   Σ_g cgsu 16706  CMndccmn 18898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-of 7389  df-ofr 7390  df-om 7561  df-1st 7671  df-2nd 7672  df-supp 7814  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-2o 8086  df-oadd 8089  df-er 8272  df-map 8391  df-pm 8392  df-ixp 8445  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-fsupp 8818  df-oi 8958  df-card 9352  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11626  df-2 11688  df-n0 11886  df-z 11970  df-uz 12232  df-fz 12886  df-fzo 13029  df-seq 13365  df-hash 13687  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-0g 16707  df-gsum 16708  df-mre 16849  df-mrc 16850  df-acs 16852  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-submnd 17949  df-mulg 18217  df-cntz 18439  df-cmn 18900

This theorem is referenced by:  psrass1  20643