Theorem psrass1lem 20157

Description: A group sum commutation used by psrass1 20185. (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 20155	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}))
8		gsumbagdiag.x	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑋 ∈ 𝐵)
9	8	anassrs 470	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑋 ∈ 𝐵)
10	9	fmpttd 6879	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵)
11	3	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐼 ∈ 𝑉)
12	2	ssrab3 4057	. . . . . . . . . . . 12 ⊢ 𝑆 ⊆ 𝐷
13	4	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐹 ∈ 𝐷)
14		simpr 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝑗 ∈ 𝑆)
15	1, 2	psrbagconcl 20153	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘f − 𝑗) ∈ 𝑆)
16	11, 13, 14, 15	syl3anc 1367	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘f − 𝑗) ∈ 𝑆)
17	12, 16	sseldi 3965	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘f − 𝑗) ∈ 𝐷)
18		eqid 2821	. . . . . . . . . . . 12 ⊢ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} = {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}
19	1, 18	psrbagconf1o 20154	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘f − 𝑗) ∈ 𝐷) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}–1-1-onto→{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
20	11, 17, 19	syl2anc 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}–1-1-onto→{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
21		f1of 6615	. . . . . . . . . 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 6531	. . . . . . . . 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 586	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚))):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵)
25	11	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐼 ∈ 𝑉)
26	13	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐹 ∈ 𝐷)
27	1	psrbagf 20145	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → 𝐹:𝐼⟶ℕ0)
28	25, 26, 27	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐹:𝐼⟶ℕ0)
29	28	ffvelrnda 6851	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈ ℕ0)
30	14	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗 ∈ 𝑆)
31	12, 30	sseldi 3965	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗 ∈ 𝐷)
32	1	psrbagf 20145	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐷) → 𝑗:𝐼⟶ℕ0)
33	25, 31, 32	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗:𝐼⟶ℕ0)
34	33	ffvelrnda 6851	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝑗‘𝑧) ∈ ℕ0)
35		ssrab2 4056	. . . . . . . . . . . . . . . . 17 ⊢ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ⊆ 𝐷
36		simpr 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
37	35, 36	sseldi 3965	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚 ∈ 𝐷)
38	1	psrbagf 20145	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑚 ∈ 𝐷) → 𝑚:𝐼⟶ℕ0)
39	25, 37, 38	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚:𝐼⟶ℕ0)
40	39	ffvelrnda 6851	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝑚‘𝑧) ∈ ℕ0)
41		nn0cn 11908	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑧) ∈ ℕ0 → (𝐹‘𝑧) ∈ ℂ)
42		nn0cn 11908	. . . . . . . . . . . . . . 15 ⊢ ((𝑗‘𝑧) ∈ ℕ0 → (𝑗‘𝑧) ∈ ℂ)
43		nn0cn 11908	. . . . . . . . . . . . . . 15 ⊢ ((𝑚‘𝑧) ∈ ℕ0 → (𝑚‘𝑧) ∈ ℂ)
44		sub32 10920	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑧) ∈ ℂ ∧ (𝑗‘𝑧) ∈ ℂ ∧ (𝑚‘𝑧) ∈ ℂ) → (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧)) = (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧)))
45	41, 42, 43, 44	syl3an 1156	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑧) ∈ ℕ0 ∧ (𝑗‘𝑧) ∈ ℕ0 ∧ (𝑚‘𝑧) ∈ ℕ0) → (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧)) = (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧)))
46	29, 34, 40, 45	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧)) = (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧)))
47	46	mpteq2dva 5161	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧))) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧))))
48		ovexd 7191	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑗‘𝑧)) ∈ V)
49	28	feqmptd 6733	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐹 = (𝑧 ∈ 𝐼 ↦ (𝐹‘𝑧)))
50	33	feqmptd 6733	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗 = (𝑧 ∈ 𝐼 ↦ (𝑗‘𝑧)))
51	25, 29, 34, 49, 50	offval2 7426	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝐹 ∘f − 𝑗) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑗‘𝑧))))
52	39	feqmptd 6733	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚 = (𝑧 ∈ 𝐼 ↦ (𝑚‘𝑧)))
53	25, 48, 40, 51, 52	offval2 7426	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f − 𝑚) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧))))
54		ovexd 7191	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑚‘𝑧)) ∈ V)
55	25, 29, 40, 49, 52	offval2 7426	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝐹 ∘f − 𝑚) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑚‘𝑧))))
56	25, 54, 34, 55, 50	offval2 7426	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑚) ∘f − 𝑗) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧))))
57	47, 53, 56	3eqtr4d 2866	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f − 𝑚) = ((𝐹 ∘f − 𝑚) ∘f − 𝑗))
58	17	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝐹 ∘f − 𝑗) ∈ 𝐷)
59	1, 18	psrbagconcl 20153	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘f − 𝑗) ∈ 𝐷 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f − 𝑚) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
60	25, 58, 36, 59	syl3anc 1367	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f − 𝑚) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
61	57, 60	eqeltrrd 2914	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑚) ∘f − 𝑗) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
62	57	mpteq2dva 5161	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)) = (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑚) ∘f − 𝑗)))
63		nfcv 2977	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛𝑋
64		nfcsb1v 3907	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⦋𝑛 / 𝑘⦌𝑋
65		csbeq1a 3897	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → 𝑋 = ⦋𝑛 / 𝑘⦌𝑋)
66	63, 64, 65	cbvmpt 5167	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋𝑛 / 𝑘⦌𝑋)
67	66	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋𝑛 / 𝑘⦌𝑋))
68		csbeq1 3886	. . . . . . . . . 10 ⊢ (𝑛 = ((𝐹 ∘f − 𝑚) ∘f − 𝑗) → ⦋𝑛 / 𝑘⦌𝑋 = ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
69	61, 62, 67, 68	fmptco 6891	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚))) = (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))
70	69	feq1d 6499	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚))):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵 ↔ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵))
71	24, 70	mpbid 234	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵)
72	71	fvmptelrn 6877	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵)
73	72	anasss 469	. . . . 5 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵)
74	7, 73	syldan 593	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵)
75	1, 2, 3, 4, 5, 6, 74	gsumbagdiag 20156	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆, 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑗 ∈ 𝑆, 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))
76		eqid 2821	. . . 4 ⊢ (0g‘𝐺) = (0g‘𝐺)
77	1	psrbaglefi 20152	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ Fin)
78	3, 4, 77	syl2anc 586	. . . . 5 ⊢ (𝜑 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ Fin)
79	2, 78	eqeltrid 2917	. . . 4 ⊢ (𝜑 → 𝑆 ∈ Fin)
80	3	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐼 ∈ 𝑉)
81	4	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐹 ∈ 𝐷)
82		simpr 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝑚 ∈ 𝑆)
83	1, 2	psrbagconcl 20153	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘f − 𝑚) ∈ 𝑆)
84	80, 81, 82, 83	syl3anc 1367	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘f − 𝑚) ∈ 𝑆)
85	12, 84	sseldi 3965	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘f − 𝑚) ∈ 𝐷)
86	1	psrbaglefi 20152	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘f − 𝑚) ∈ 𝐷) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ Fin)
87	80, 85, 86	syl2anc 586	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ Fin)
88		xpfi 8789	. . . . 5 ⊢ ((𝑆 ∈ Fin ∧ 𝑆 ∈ Fin) → (𝑆 × 𝑆) ∈ Fin)
89	79, 79, 88	syl2anc 586	. . . 4 ⊢ (𝜑 → (𝑆 × 𝑆) ∈ Fin)
90		simprl 769	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → 𝑚 ∈ 𝑆)
91	7	simpld 497	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → 𝑗 ∈ 𝑆)
92		brxp 5601	. . . . . . 7 ⊢ (𝑚(𝑆 × 𝑆)𝑗 ↔ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ 𝑆))
93	90, 91, 92	sylanbrc 585	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → 𝑚(𝑆 × 𝑆)𝑗)
94	93	pm2.24d 154	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → (¬ 𝑚(𝑆 × 𝑆)𝑗 → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺)))
95	94	impr 457	. . . 4 ⊢ ((𝜑 ∧ ((𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}) ∧ ¬ 𝑚(𝑆 × 𝑆)𝑗)) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺))
96	5, 76, 6, 79, 87, 74, 89, 95	gsum2d2 19094	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆, 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
97	1	psrbaglefi 20152	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘f − 𝑗) ∈ 𝐷) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ Fin)
98	11, 17, 97	syl2anc 586	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ Fin)
99		simprl 769	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑗 ∈ 𝑆)
100	1, 2, 3, 4	gsumbagdiaglem 20155	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}))
101	100	simpld 497	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑚 ∈ 𝑆)
102		brxp 5601	. . . . . . 7 ⊢ (𝑗(𝑆 × 𝑆)𝑚 ↔ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ 𝑆))
103	99, 101, 102	sylanbrc 585	. . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑗(𝑆 × 𝑆)𝑚)
104	103	pm2.24d 154	. . . . 5 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → (¬ 𝑗(𝑆 × 𝑆)𝑚 → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺)))
105	104	impr 457	. . . 4 ⊢ ((𝜑 ∧ ((𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ ¬ 𝑗(𝑆 × 𝑆)𝑚)) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺))
106	5, 76, 6, 79, 98, 73, 89, 105	gsum2d2 19094	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝑆, 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
107	75, 96, 106	3eqtr3d 2864	. 2 ⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
108	6	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐺 ∈ CMnd)
109	74	anassrs 470	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ 𝑆) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}) → ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵)
110	109	fmpttd 6879	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}⟶𝐵)
111		ovex 7189	. . . . . . . . . . . 12 ⊢ (ℕ0 ↑m 𝐼) ∈ V
112	1, 111	rabex2 5237	. . . . . . . . . . 11 ⊢ 𝐷 ∈ V
113	112	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐷 ∈ V)
114		rabexg 5234	. . . . . . . . . 10 ⊢ (𝐷 ∈ V → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ V)
115		mptexg 6984	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ V → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ∈ V)
116	113, 114, 115	3syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ∈ V)
117		funmpt 6393	. . . . . . . . . 10 ⊢ Fun (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
118	117	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → Fun (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))
119		fvexd 6685	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (0g‘𝐺) ∈ V)
120		suppssdm 7843	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ dom (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
121		eqid 2821	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) = (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
122	121	dmmptss 6095	. . . . . . . . . . 11 ⊢ dom (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}
123	120, 122	sstri 3976	. . . . . . . . . 10 ⊢ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}
124	123	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})
125		suppssfifsupp 8848	. . . . . . . . 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 1374	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) finSupp (0g‘𝐺))
127	5, 76, 108, 87, 110, 126	gsumcl 19035	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) ∈ 𝐵)
128	127	fmpttd 6879	. . . . . 6 ⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))):𝑆⟶𝐵)
129	1, 2	psrbagconf1o 20154	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆)
130	3, 4, 129	syl2anc 586	. . . . . . 7 ⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆)
131		f1ocnv 6627	. . . . . . 7 ⊢ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆)
132		f1of 6615	. . . . . . 7 ⊢ (◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆⟶𝑆)
133	130, 131, 132	3syl 18	. . . . . 6 ⊢ (𝜑 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆⟶𝑆)
134		fco 6531	. . . . . 6 ⊢ (((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))):𝑆⟶𝐵 ∧ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆⟶𝑆) → ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))):𝑆⟶𝐵)
135	128, 133, 134	syl2anc 586	. . . . 5 ⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))):𝑆⟶𝐵)
136		coass 6118	. . . . . . . 8 ⊢ (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))))
137		f1ococnv2 6641	. . . . . . . . . 10 ⊢ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆 → ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ( I ↾ 𝑆))
138	130, 137	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ( I ↾ 𝑆))
139	138	coeq2d 5733	. . . . . . . 8 ⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)))
140	136, 139	syl5eq 2868	. . . . . . 7 ⊢ (𝜑 → (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)))
141		eqidd 2822	. . . . . . . . 9 ⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) = (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))
142		eqidd 2822	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
143		breq2 5070	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝑥 ∘r ≤ 𝑛 ↔ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)))
144	143	rabbidv 3480	. . . . . . . . . . 11 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} = {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})
145		ovex 7189	. . . . . . . . . . . . 13 ⊢ (𝑛 ∘f − 𝑗) ∈ V
146		psrass1lem.y	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 ∘f − 𝑗) → 𝑋 = 𝑌)
147	145, 146	csbie 3918	. . . . . . . . . . . 12 ⊢ ⦋(𝑛 ∘f − 𝑗) / 𝑘⦌𝑋 = 𝑌
148		oveq1 7163	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝑛 ∘f − 𝑗) = ((𝐹 ∘f − 𝑚) ∘f − 𝑗))
149	148	csbeq1d 3887	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → ⦋(𝑛 ∘f − 𝑗) / 𝑘⦌𝑋 = ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
150	147, 149	syl5eqr 2870	. . . . . . . . . . 11 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → 𝑌 = ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)
151	144, 150	mpteq12dv 5151	. . . . . . . . . 10 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌) = (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))
152	151	oveq2d 7172	. . . . . . . . 9 ⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)) = (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))
153	84, 141, 142, 152	fmptco 6891	. . . . . . . 8 ⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))))
154	153	coeq1d 5732	. . . . . . 7 ⊢ (𝜑 → (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))))
155		coires1 6117	. . . . . . . . 9 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆)
156		ssid 3989	. . . . . . . . . 10 ⊢ 𝑆 ⊆ 𝑆
157		resmpt 5905	. . . . . . . . . 10 ⊢ (𝑆 ⊆ 𝑆 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
158	156, 157	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
159	155, 158	eqtri 2844	. . . . . . . 8 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
160	159	a1i 11	. . . . . . 7 ⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
161	140, 154, 160	3eqtr3d 2864	. . . . . 6 ⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
162	161	feq1d 6499	. . . . 5 ⊢ (𝜑 → (((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))):𝑆⟶𝐵 ↔ (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))):𝑆⟶𝐵))
163	135, 162	mpbid 234	. . . 4 ⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))):𝑆⟶𝐵)
164		rabexg 5234	. . . . . . . 8 ⊢ (𝐷 ∈ V → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ V)
165	112, 164	mp1i 13	. . . . . . 7 ⊢ (𝜑 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ V)
166	2, 165	eqeltrid 2917	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ V)
167	166	mptexd 6987	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∈ V)
168		funmpt 6393	. . . . . 6 ⊢ Fun (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
169	168	a1i 11	. . . . 5 ⊢ (𝜑 → Fun (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))))
170		fvexd 6685	. . . . 5 ⊢ (𝜑 → (0g‘𝐺) ∈ V)
171		suppssdm 7843	. . . . . . 7 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ dom (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
172		eqid 2821	. . . . . . . 8 ⊢ (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))
173	172	dmmptss 6095	. . . . . . 7 ⊢ dom (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ⊆ 𝑆
174	171, 173	sstri 3976	. . . . . 6 ⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ 𝑆
175	174	a1i 11	. . . . 5 ⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ 𝑆)
176		suppssfifsupp 8848	. . . . 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 1374	. . . 4 ⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) finSupp (0g‘𝐺))
178	5, 76, 6, 79, 163, 177, 130	gsumf1o 19036	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))))
179	153	oveq2d 7172	. . 3 ⊢ (𝜑 → (𝐺 Σg ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
180	178, 179	eqtrd 2856	. 2 ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
181	6	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐺 ∈ CMnd)
182	112	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐷 ∈ V)
183		rabexg 5234	. . . . . . . 8 ⊢ (𝐷 ∈ V → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ V)
184		mptexg 6984	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ V → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∈ V)
185	182, 183, 184	3syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∈ V)
186		funmpt 6393	. . . . . . . 8 ⊢ Fun (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)
187	186	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → Fun (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋))
188		fvexd 6685	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (0g‘𝐺) ∈ V)
189		suppssdm 7843	. . . . . . . . 9 ⊢ ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ dom (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)
190		eqid 2821	. . . . . . . . . 10 ⊢ (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) = (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)
191	190	dmmptss 6095	. . . . . . . . 9 ⊢ dom (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}
192	189, 191	sstri 3976	. . . . . . . 8 ⊢ ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}
193	192	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})
194		suppssfifsupp 8848	. . . . . . 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 1374	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) finSupp (0g‘𝐺))
196	5, 76, 181, 98, 10, 195, 20	gsumf1o 19036	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)) = (𝐺 Σg ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)))))
197	69	oveq2d 7172	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f − 𝑚)))) = (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))
198	196, 197	eqtrd 2856	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)) = (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))
199	198	mpteq2dva 5161	. . 3 ⊢ (𝜑 → (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋))) = (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))))
200	199	oveq2d 7172	. 2 ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋((𝐹 ∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))))
201	107, 180, 200	3eqtr4d 2866	1 ⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  {crab 3142  Vcvv 3494  ⦋csb 3883   ⊆ wss 3936   class class class wbr 5066   ↦ cmpt 5146   I cid 5459   × cxp 5553  ^◡ccnv 5554  dom cdm 5555   ↾ cres 5557   “ cima 5558   ∘ ccom 5559  Fun wfun 6349  ⟶wf 6351  –1-1-onto→wf1o 6354  ‘cfv 6355  (class class class)co 7156   ∈ cmpo 7158   ∘_f cof 7407   ∘_r cofr 7408   supp csupp 7830   ↑_m cmap 8406  Fincfn 8509   finSupp cfsupp 8833  ℂcc 10535   ≤ cle 10676   − cmin 10870  ℕcn 11638  ℕ₀cn0 11898  Basecbs 16483  0_gc0g 16713   Σ_g cgsu 16714  CMndccmn 18906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-int 4877  df-iun 4921  df-iin 4922  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-se 5515  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-isom 6364  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-of 7409  df-ofr 7410  df-om 7581  df-1st 7689  df-2nd 7690  df-supp 7831  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-1o 8102  df-2o 8103  df-oadd 8106  df-er 8289  df-map 8408  df-pm 8409  df-ixp 8462  df-en 8510  df-dom 8511  df-sdom 8512  df-fin 8513  df-fsupp 8834  df-oi 8974  df-card 9368  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-nn 11639  df-2 11701  df-n0 11899  df-z 11983  df-uz 12245  df-fz 12894  df-fzo 13035  df-seq 13371  df-hash 13692  df-ndx 16486  df-slot 16487  df-base 16489  df-sets 16490  df-ress 16491  df-plusg 16578  df-0g 16715  df-gsum 16716  df-mre 16857  df-mrc 16858  df-acs 16860  df-mgm 17852  df-sgrp 17901  df-mnd 17912  df-submnd 17957  df-mulg 18225  df-cntz 18447  df-cmn 18908

This theorem is referenced by:  psrass1  20185