MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  psrass1lem Structured version   Visualization version   GIF version

Theorem psrass1lem 21952
Description: A group sum commutation used by psrass1 21984. (Contributed by Mario Carneiro, 5-Jan-2015.) Remove a sethood hypothesis. (Revised by SN, 7-Aug-2024.)
Hypotheses
Ref Expression
gsumbagdiag.d 𝐷 = {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ 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.
StepHypRef Expression
1 gsumbagdiag.d . . . 4 𝐷 = {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
2 gsumbagdiag.s . . . 4 𝑆 = {𝑦𝐷𝑦r𝐹}
3 gsumbagdiag.f . . . 4 (𝜑𝐹𝐷)
4 gsumbagdiag.b . . . 4 𝐵 = (Base‘𝐺)
5 gsumbagdiag.g . . . 4 (𝜑𝐺 ∈ CMnd)
61, 2, 3gsumbagdiaglem 21950 . . . . 5 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}))
7 gsumbagdiag.x . . . . . . . . . . 11 ((𝜑 ∧ (𝑗𝑆𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → 𝑋𝐵)
87anassrs 467 . . . . . . . . . 10 (((𝜑𝑗𝑆) ∧ 𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑋𝐵)
98fmpttd 7135 . . . . . . . . 9 ((𝜑𝑗𝑆) → (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶𝐵)
102ssrab3 4082 . . . . . . . . . . . 12 𝑆𝐷
111, 2psrbagconcl 21947 . . . . . . . . . . . . 13 ((𝐹𝐷𝑗𝑆) → (𝐹f𝑗) ∈ 𝑆)
123, 11sylan 580 . . . . . . . . . . . 12 ((𝜑𝑗𝑆) → (𝐹f𝑗) ∈ 𝑆)
1310, 12sselid 3981 . . . . . . . . . . 11 ((𝜑𝑗𝑆) → (𝐹f𝑗) ∈ 𝐷)
14 eqid 2737 . . . . . . . . . . . 12 {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} = {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}
151, 14psrbagconf1o 21949 . . . . . . . . . . 11 ((𝐹f𝑗) ∈ 𝐷 → (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}–1-1-onto→{𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
1613, 15syl 17 . . . . . . . . . 10 ((𝜑𝑗𝑆) → (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}–1-1-onto→{𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
17 f1of 6848 . . . . . . . . . 10 ((𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}–1-1-onto→{𝑥𝐷𝑥r ≤ (𝐹f𝑗)} → (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶{𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
1816, 17syl 17 . . . . . . . . 9 ((𝜑𝑗𝑆) → (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶{𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
199, 18fcod 6761 . . . . . . . 8 ((𝜑𝑗𝑆) → ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚))):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶𝐵)
203adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑆) → 𝐹𝐷)
2120adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝐹𝐷)
221psrbagf 21938 . . . . . . . . . . . . . . . 16 (𝐹𝐷𝐹:𝐼⟶ℕ0)
2321, 22syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝐹:𝐼⟶ℕ0)
2423ffvelcdmda 7104 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → (𝐹𝑧) ∈ ℕ0)
25 simplr 769 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑗𝑆)
2610, 25sselid 3981 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑗𝐷)
271psrbagf 21938 . . . . . . . . . . . . . . . 16 (𝑗𝐷𝑗:𝐼⟶ℕ0)
2826, 27syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑗:𝐼⟶ℕ0)
2928ffvelcdmda 7104 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → (𝑗𝑧) ∈ ℕ0)
30 ssrab2 4080 . . . . . . . . . . . . . . . . 17 {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ⊆ 𝐷
31 simpr 484 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
3230, 31sselid 3981 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑚𝐷)
331psrbagf 21938 . . . . . . . . . . . . . . . 16 (𝑚𝐷𝑚:𝐼⟶ℕ0)
3432, 33syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑚:𝐼⟶ℕ0)
3534ffvelcdmda 7104 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → (𝑚𝑧) ∈ ℕ0)
36 nn0cn 12536 . . . . . . . . . . . . . . 15 ((𝐹𝑧) ∈ ℕ0 → (𝐹𝑧) ∈ ℂ)
37 nn0cn 12536 . . . . . . . . . . . . . . 15 ((𝑗𝑧) ∈ ℕ0 → (𝑗𝑧) ∈ ℂ)
38 nn0cn 12536 . . . . . . . . . . . . . . 15 ((𝑚𝑧) ∈ ℕ0 → (𝑚𝑧) ∈ ℂ)
39 sub32 11543 . . . . . . . . . . . . . . 15 (((𝐹𝑧) ∈ ℂ ∧ (𝑗𝑧) ∈ ℂ ∧ (𝑚𝑧) ∈ ℂ) → (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧)) = (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧)))
4036, 37, 38, 39syl3an 1161 . . . . . . . . . . . . . 14 (((𝐹𝑧) ∈ ℕ0 ∧ (𝑗𝑧) ∈ ℕ0 ∧ (𝑚𝑧) ∈ ℕ0) → (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧)) = (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧)))
4124, 29, 35, 40syl3anc 1373 . . . . . . . . . . . . 13 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧)) = (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧)))
4241mpteq2dva 5242 . . . . . . . . . . . 12 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → (𝑧𝐼 ↦ (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧))) = (𝑧𝐼 ↦ (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧))))
4334ffnd 6737 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑚 Fn 𝐼)
4431, 43fndmexd 7926 . . . . . . . . . . . . 13 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝐼 ∈ V)
45 ovexd 7466 . . . . . . . . . . . . 13 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → ((𝐹𝑧) − (𝑗𝑧)) ∈ V)
4623feqmptd 6977 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝐹 = (𝑧𝐼 ↦ (𝐹𝑧)))
4728feqmptd 6977 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑗 = (𝑧𝐼 ↦ (𝑗𝑧)))
4844, 24, 29, 46, 47offval2 7717 . . . . . . . . . . . . 13 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → (𝐹f𝑗) = (𝑧𝐼 ↦ ((𝐹𝑧) − (𝑗𝑧))))
4934feqmptd 6977 . . . . . . . . . . . . 13 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑚 = (𝑧𝐼 ↦ (𝑚𝑧)))
5044, 45, 35, 48, 49offval2 7717 . . . . . . . . . . . 12 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑗) ∘f𝑚) = (𝑧𝐼 ↦ (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧))))
51 ovexd 7466 . . . . . . . . . . . . 13 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → ((𝐹𝑧) − (𝑚𝑧)) ∈ V)
5244, 24, 35, 46, 49offval2 7717 . . . . . . . . . . . . 13 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → (𝐹f𝑚) = (𝑧𝐼 ↦ ((𝐹𝑧) − (𝑚𝑧))))
5344, 51, 29, 52, 47offval2 7717 . . . . . . . . . . . 12 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑚) ∘f𝑗) = (𝑧𝐼 ↦ (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧))))
5442, 50, 533eqtr4d 2787 . . . . . . . . . . 11 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑗) ∘f𝑚) = ((𝐹f𝑚) ∘f𝑗))
551, 14psrbagconcl 21947 . . . . . . . . . . . 12 (((𝐹f𝑗) ∈ 𝐷𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑗) ∘f𝑚) ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
5613, 55sylan 580 . . . . . . . . . . 11 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑗) ∘f𝑚) ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
5754, 56eqeltrrd 2842 . . . . . . . . . 10 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑚) ∘f𝑗) ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
5854mpteq2dva 5242 . . . . . . . . . 10 ((𝜑𝑗𝑆) → (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)) = (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗)))
59 nfcv 2905 . . . . . . . . . . . 12 𝑛𝑋
60 nfcsb1v 3923 . . . . . . . . . . . 12 𝑘𝑛 / 𝑘𝑋
61 csbeq1a 3913 . . . . . . . . . . . 12 (𝑘 = 𝑛𝑋 = 𝑛 / 𝑘𝑋)
6259, 60, 61cbvmpt 5253 . . . . . . . . . . 11 (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑛 / 𝑘𝑋)
6362a1i 11 . . . . . . . . . 10 ((𝜑𝑗𝑆) → (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑛 / 𝑘𝑋))
64 csbeq1 3902 . . . . . . . . . 10 (𝑛 = ((𝐹f𝑚) ∘f𝑗) → 𝑛 / 𝑘𝑋 = ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
6557, 58, 63, 64fmptco 7149 . . . . . . . . 9 ((𝜑𝑗𝑆) → ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚))) = (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))
6665feq1d 6720 . . . . . . . 8 ((𝜑𝑗𝑆) → (((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚))):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶𝐵 ↔ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶𝐵))
6719, 66mpbid 232 . . . . . . 7 ((𝜑𝑗𝑆) → (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶𝐵)
6867fvmptelcdm 7133 . . . . . 6 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋𝐵)
6968anasss 466 . . . . 5 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋𝐵)
706, 69syldan 591 . . . 4 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋𝐵)
711, 2, 3, 4, 5, 70gsumbagdiag 21951 . . 3 (𝜑 → (𝐺 Σg (𝑚𝑆, 𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)) = (𝐺 Σg (𝑗𝑆, 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))
72 eqid 2737 . . . 4 (0g𝐺) = (0g𝐺)
731psrbaglefi 21946 . . . . . 6 (𝐹𝐷 → {𝑦𝐷𝑦r𝐹} ∈ Fin)
743, 73syl 17 . . . . 5 (𝜑 → {𝑦𝐷𝑦r𝐹} ∈ Fin)
752, 74eqeltrid 2845 . . . 4 (𝜑𝑆 ∈ Fin)
761, 2psrbagconcl 21947 . . . . . . 7 ((𝐹𝐷𝑚𝑆) → (𝐹f𝑚) ∈ 𝑆)
773, 76sylan 580 . . . . . 6 ((𝜑𝑚𝑆) → (𝐹f𝑚) ∈ 𝑆)
7810, 77sselid 3981 . . . . 5 ((𝜑𝑚𝑆) → (𝐹f𝑚) ∈ 𝐷)
791psrbaglefi 21946 . . . . 5 ((𝐹f𝑚) ∈ 𝐷 → {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ∈ Fin)
8078, 79syl 17 . . . 4 ((𝜑𝑚𝑆) → {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ∈ Fin)
81 xpfi 9358 . . . . 5 ((𝑆 ∈ Fin ∧ 𝑆 ∈ Fin) → (𝑆 × 𝑆) ∈ Fin)
8275, 75, 81syl2anc 584 . . . 4 (𝜑 → (𝑆 × 𝑆) ∈ Fin)
83 simprl 771 . . . . . . 7 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → 𝑚𝑆)
846simpld 494 . . . . . . 7 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → 𝑗𝑆)
85 brxp 5734 . . . . . . 7 (𝑚(𝑆 × 𝑆)𝑗 ↔ (𝑚𝑆𝑗𝑆))
8683, 84, 85sylanbrc 583 . . . . . 6 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → 𝑚(𝑆 × 𝑆)𝑗)
8786pm2.24d 151 . . . . 5 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → (¬ 𝑚(𝑆 × 𝑆)𝑗((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋 = (0g𝐺)))
8887impr 454 . . . 4 ((𝜑 ∧ ((𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)}) ∧ ¬ 𝑚(𝑆 × 𝑆)𝑗)) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋 = (0g𝐺))
894, 72, 5, 75, 80, 70, 82, 88gsum2d2 19992 . . 3 (𝜑 → (𝐺 Σg (𝑚𝑆, 𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)) = (𝐺 Σg (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
901psrbaglefi 21946 . . . . 5 ((𝐹f𝑗) ∈ 𝐷 → {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ∈ Fin)
9113, 90syl 17 . . . 4 ((𝜑𝑗𝑆) → {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ∈ Fin)
92 simprl 771 . . . . . . 7 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → 𝑗𝑆)
931, 2, 3gsumbagdiaglem 21950 . . . . . . . 8 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)}))
9493simpld 494 . . . . . . 7 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → 𝑚𝑆)
95 brxp 5734 . . . . . . 7 (𝑗(𝑆 × 𝑆)𝑚 ↔ (𝑗𝑆𝑚𝑆))
9692, 94, 95sylanbrc 583 . . . . . 6 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → 𝑗(𝑆 × 𝑆)𝑚)
9796pm2.24d 151 . . . . 5 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → (¬ 𝑗(𝑆 × 𝑆)𝑚((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋 = (0g𝐺)))
9897impr 454 . . . 4 ((𝜑 ∧ ((𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ ¬ 𝑗(𝑆 × 𝑆)𝑚)) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋 = (0g𝐺))
994, 72, 5, 75, 91, 69, 82, 98gsum2d2 19992 . . 3 (𝜑 → (𝐺 Σg (𝑗𝑆, 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
10071, 89, 993eqtr3d 2785 . 2 (𝜑 → (𝐺 Σg (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
1015adantr 480 . . . . . . . 8 ((𝜑𝑚𝑆) → 𝐺 ∈ CMnd)
10270anassrs 467 . . . . . . . . 9 (((𝜑𝑚𝑆) ∧ 𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)}) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋𝐵)
103102fmpttd 7135 . . . . . . . 8 ((𝜑𝑚𝑆) → (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋):{𝑥𝐷𝑥r ≤ (𝐹f𝑚)}⟶𝐵)
104 ovex 7464 . . . . . . . . . . . 12 (ℕ0m 𝐼) ∈ V
1051, 104rabex2 5341 . . . . . . . . . . 11 𝐷 ∈ V
106105a1i 11 . . . . . . . . . 10 ((𝜑𝑚𝑆) → 𝐷 ∈ V)
107 rabexg 5337 . . . . . . . . . 10 (𝐷 ∈ V → {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ∈ V)
108 mptexg 7241 . . . . . . . . . 10 ({𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ∈ V → (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) ∈ V)
109106, 107, 1083syl 18 . . . . . . . . 9 ((𝜑𝑚𝑆) → (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) ∈ V)
110 funmpt 6604 . . . . . . . . . 10 Fun (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
111110a1i 11 . . . . . . . . 9 ((𝜑𝑚𝑆) → Fun (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))
112 fvexd 6921 . . . . . . . . 9 ((𝜑𝑚𝑆) → (0g𝐺) ∈ V)
113 suppssdm 8202 . . . . . . . . . . 11 ((𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) supp (0g𝐺)) ⊆ dom (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
114 eqid 2737 . . . . . . . . . . . 12 (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) = (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
115114dmmptss 6261 . . . . . . . . . . 11 dom (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)}
116113, 115sstri 3993 . . . . . . . . . 10 ((𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)}
117116a1i 11 . . . . . . . . 9 ((𝜑𝑚𝑆) → ((𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})
118 suppssfifsupp 9420 . . . . . . . . 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𝐺))
119109, 111, 112, 80, 117, 118syl32anc 1380 . . . . . . . 8 ((𝜑𝑚𝑆) → (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) finSupp (0g𝐺))
1204, 72, 101, 80, 103, 119gsumcl 19933 . . . . . . 7 ((𝜑𝑚𝑆) → (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)) ∈ 𝐵)
121120fmpttd 7135 . . . . . 6 (𝜑 → (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))):𝑆𝐵)
1221, 2psrbagconf1o 21949 . . . . . . . 8 (𝐹𝐷 → (𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆)
1233, 122syl 17 . . . . . . 7 (𝜑 → (𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆)
124 f1ocnv 6860 . . . . . . 7 ((𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆(𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆)
125 f1of 6848 . . . . . . 7 ((𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆(𝑚𝑆 ↦ (𝐹f𝑚)):𝑆𝑆)
126123, 124, 1253syl 18 . . . . . 6 (𝜑(𝑚𝑆 ↦ (𝐹f𝑚)):𝑆𝑆)
127121, 126fcod 6761 . . . . 5 (𝜑 → ((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))):𝑆𝐵)
128 coass 6285 . . . . . . . 8 (((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ((𝑚𝑆 ↦ (𝐹f𝑚)) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))))
129 f1ococnv2 6875 . . . . . . . . . 10 ((𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆 → ((𝑚𝑆 ↦ (𝐹f𝑚)) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = ( I ↾ 𝑆))
130123, 129syl 17 . . . . . . . . 9 (𝜑 → ((𝑚𝑆 ↦ (𝐹f𝑚)) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = ( I ↾ 𝑆))
131130coeq2d 5873 . . . . . . . 8 (𝜑 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ((𝑚𝑆 ↦ (𝐹f𝑚)) ∘ (𝑚𝑆 ↦ (𝐹f𝑚)))) = ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)))
132128, 131eqtrid 2789 . . . . . . 7 (𝜑 → (((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)))
133 eqidd 2738 . . . . . . . . 9 (𝜑 → (𝑚𝑆 ↦ (𝐹f𝑚)) = (𝑚𝑆 ↦ (𝐹f𝑚)))
134 eqidd 2738 . . . . . . . . 9 (𝜑 → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))))
135 breq2 5147 . . . . . . . . . . . 12 (𝑛 = (𝐹f𝑚) → (𝑥r𝑛𝑥r ≤ (𝐹f𝑚)))
136135rabbidv 3444 . . . . . . . . . . 11 (𝑛 = (𝐹f𝑚) → {𝑥𝐷𝑥r𝑛} = {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})
137 ovex 7464 . . . . . . . . . . . . 13 (𝑛f𝑗) ∈ V
138 psrass1lem.y . . . . . . . . . . . . 13 (𝑘 = (𝑛f𝑗) → 𝑋 = 𝑌)
139137, 138csbie 3934 . . . . . . . . . . . 12 (𝑛f𝑗) / 𝑘𝑋 = 𝑌
140 oveq1 7438 . . . . . . . . . . . . 13 (𝑛 = (𝐹f𝑚) → (𝑛f𝑗) = ((𝐹f𝑚) ∘f𝑗))
141140csbeq1d 3903 . . . . . . . . . . . 12 (𝑛 = (𝐹f𝑚) → (𝑛f𝑗) / 𝑘𝑋 = ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
142139, 141eqtr3id 2791 . . . . . . . . . . 11 (𝑛 = (𝐹f𝑚) → 𝑌 = ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
143136, 142mpteq12dv 5233 . . . . . . . . . 10 (𝑛 = (𝐹f𝑚) → (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌) = (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))
144143oveq2d 7447 . . . . . . . . 9 (𝑛 = (𝐹f𝑚) → (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)) = (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))
14577, 133, 134, 144fmptco 7149 . . . . . . . 8 (𝜑 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))))
146145coeq1d 5872 . . . . . . 7 (𝜑 → (((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = ((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))))
147 coires1 6284 . . . . . . . . 9 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ↾ 𝑆)
148 ssid 4006 . . . . . . . . . 10 𝑆𝑆
149 resmpt 6055 . . . . . . . . . 10 (𝑆𝑆 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))))
150148, 149ax-mp 5 . . . . . . . . 9 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))
151147, 150eqtri 2765 . . . . . . . 8 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))
152151a1i 11 . . . . . . 7 (𝜑 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))))
153132, 146, 1523eqtr3d 2785 . . . . . 6 (𝜑 → ((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))))
154153feq1d 6720 . . . . 5 (𝜑 → (((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))):𝑆𝐵 ↔ (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))):𝑆𝐵))
155127, 154mpbid 232 . . . 4 (𝜑 → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))):𝑆𝐵)
156 rabexg 5337 . . . . . . . 8 (𝐷 ∈ V → {𝑦𝐷𝑦r𝐹} ∈ V)
157105, 156mp1i 13 . . . . . . 7 (𝜑 → {𝑦𝐷𝑦r𝐹} ∈ V)
1582, 157eqeltrid 2845 . . . . . 6 (𝜑𝑆 ∈ V)
159158mptexd 7244 . . . . 5 (𝜑 → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∈ V)
160 funmpt 6604 . . . . . 6 Fun (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))
161160a1i 11 . . . . 5 (𝜑 → Fun (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))))
162 fvexd 6921 . . . . 5 (𝜑 → (0g𝐺) ∈ V)
163 suppssdm 8202 . . . . . . 7 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) supp (0g𝐺)) ⊆ dom (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))
164 eqid 2737 . . . . . . . 8 (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))
165164dmmptss 6261 . . . . . . 7 dom (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ⊆ 𝑆
166163, 165sstri 3993 . . . . . 6 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) supp (0g𝐺)) ⊆ 𝑆
167166a1i 11 . . . . 5 (𝜑 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) supp (0g𝐺)) ⊆ 𝑆)
168 suppssfifsupp 9420 . . . . 5 ((((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∈ V ∧ Fun (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∧ (0g𝐺) ∈ V) ∧ (𝑆 ∈ Fin ∧ ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) supp (0g𝐺)) ⊆ 𝑆)) → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) finSupp (0g𝐺))
169159, 161, 162, 75, 167, 168syl32anc 1380 . . . 4 (𝜑 → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) finSupp (0g𝐺))
1704, 72, 5, 75, 155, 169, 123gsumf1o 19934 . . 3 (𝜑 → (𝐺 Σg (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))) = (𝐺 Σg ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚)))))
171145oveq2d 7447 . . 3 (𝜑 → (𝐺 Σg ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚)))) = (𝐺 Σg (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
172170, 171eqtrd 2777 . 2 (𝜑 → (𝐺 Σg (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
1735adantr 480 . . . . . 6 ((𝜑𝑗𝑆) → 𝐺 ∈ CMnd)
174105a1i 11 . . . . . . . 8 ((𝜑𝑗𝑆) → 𝐷 ∈ V)
175 rabexg 5337 . . . . . . . 8 (𝐷 ∈ V → {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ∈ V)
176 mptexg 7241 . . . . . . . 8 ({𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ∈ V → (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∈ V)
177174, 175, 1763syl 18 . . . . . . 7 ((𝜑𝑗𝑆) → (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∈ V)
178 funmpt 6604 . . . . . . . 8 Fun (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)
179178a1i 11 . . . . . . 7 ((𝜑𝑗𝑆) → Fun (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋))
180 fvexd 6921 . . . . . . 7 ((𝜑𝑗𝑆) → (0g𝐺) ∈ V)
181 suppssdm 8202 . . . . . . . . 9 ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) supp (0g𝐺)) ⊆ dom (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)
182 eqid 2737 . . . . . . . . . 10 (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) = (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)
183182dmmptss 6261 . . . . . . . . 9 dom (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}
184181, 183sstri 3993 . . . . . . . 8 ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}
185184a1i 11 . . . . . . 7 ((𝜑𝑗𝑆) → ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
186 suppssfifsupp 9420 . . . . . . 7 ((((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∈ V ∧ Fun (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∧ (0g𝐺) ∈ V) ∧ ({𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ∈ Fin ∧ ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) finSupp (0g𝐺))
187177, 179, 180, 91, 185, 186syl32anc 1380 . . . . . 6 ((𝜑𝑗𝑆) → (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) finSupp (0g𝐺))
1884, 72, 173, 91, 9, 187, 16gsumf1o 19934 . . . . 5 ((𝜑𝑗𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)) = (𝐺 Σg ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)))))
18965oveq2d 7447 . . . . 5 ((𝜑𝑗𝑆) → (𝐺 Σg ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)))) = (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))
190188, 189eqtrd 2777 . . . 4 ((𝜑𝑗𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)) = (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))
191190mpteq2dva 5242 . . 3 (𝜑 → (𝑗𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋))) = (𝑗𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))))
192191oveq2d 7447 . 2 (𝜑 → (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)))) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
193100, 172, 1923eqtr4d 2787 1 (𝜑 → (𝐺 Σg (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   = wceq 1540  wcel 2108  {crab 3436  Vcvv 3480  csb 3899  wss 3951   class class class wbr 5143  cmpt 5225   I cid 5577   × cxp 5683  ccnv 5684  dom cdm 5685  cres 5687  cima 5688  ccom 5689  Fun wfun 6555  wf 6557  1-1-ontowf1o 6560  cfv 6561  (class class class)co 7431  cmpo 7433  f cof 7695  r cofr 7696   supp csupp 8185  m cmap 8866  Fincfn 8985   finSupp cfsupp 9401  cc 11153  cle 11296  cmin 11492  cn 12266  0cn0 12526  Basecbs 17247  0gc0g 17484   Σg cgsu 17485  CMndccmn 19798
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-ofr 7698  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-n0 12527  df-z 12614  df-uz 12879  df-fz 13548  df-fzo 13695  df-seq 14043  df-hash 14370  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-0g 17486  df-gsum 17487  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-mulg 19086  df-cntz 19335  df-cmn 19800
This theorem is referenced by:  psrass1  21984
  Copyright terms: Public domain W3C validator