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

Theorem psrass1lem 21911
Description: A group sum commutation used by psrass1 21943. (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 21909 . . . . 5 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}))
7 gsumbagdiag.x . . . . . . . . . . 11 ((𝜑 ∧ (𝑗𝑆𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → 𝑋𝐵)
87anassrs 466 . . . . . . . . . 10 (((𝜑𝑗𝑆) ∧ 𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑋𝐵)
98fmpttd 7124 . . . . . . . . 9 ((𝜑𝑗𝑆) → (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶𝐵)
102ssrab3 4076 . . . . . . . . . . . 12 𝑆𝐷
111, 2psrbagconcl 21901 . . . . . . . . . . . . 13 ((𝐹𝐷𝑗𝑆) → (𝐹f𝑗) ∈ 𝑆)
123, 11sylan 578 . . . . . . . . . . . 12 ((𝜑𝑗𝑆) → (𝐹f𝑗) ∈ 𝑆)
1310, 12sselid 3974 . . . . . . . . . . 11 ((𝜑𝑗𝑆) → (𝐹f𝑗) ∈ 𝐷)
14 eqid 2725 . . . . . . . . . . . 12 {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} = {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}
151, 14psrbagconf1o 21904 . . . . . . . . . . 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 6838 . . . . . . . . . 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 6749 . . . . . . . 8 ((𝜑𝑗𝑆) → ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚))):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶𝐵)
203adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑆) → 𝐹𝐷)
2120adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝐹𝐷)
221psrbagf 21885 . . . . . . . . . . . . . . . 16 (𝐹𝐷𝐹:𝐼⟶ℕ0)
2321, 22syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝐹:𝐼⟶ℕ0)
2423ffvelcdmda 7093 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → (𝐹𝑧) ∈ ℕ0)
25 simplr 767 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑗𝑆)
2610, 25sselid 3974 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑗𝐷)
271psrbagf 21885 . . . . . . . . . . . . . . . 16 (𝑗𝐷𝑗:𝐼⟶ℕ0)
2826, 27syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑗:𝐼⟶ℕ0)
2928ffvelcdmda 7093 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → (𝑗𝑧) ∈ ℕ0)
30 ssrab2 4073 . . . . . . . . . . . . . . . . 17 {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ⊆ 𝐷
31 simpr 483 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
3230, 31sselid 3974 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑚𝐷)
331psrbagf 21885 . . . . . . . . . . . . . . . 16 (𝑚𝐷𝑚:𝐼⟶ℕ0)
3432, 33syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑚:𝐼⟶ℕ0)
3534ffvelcdmda 7093 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → (𝑚𝑧) ∈ ℕ0)
36 nn0cn 12520 . . . . . . . . . . . . . . 15 ((𝐹𝑧) ∈ ℕ0 → (𝐹𝑧) ∈ ℂ)
37 nn0cn 12520 . . . . . . . . . . . . . . 15 ((𝑗𝑧) ∈ ℕ0 → (𝑗𝑧) ∈ ℂ)
38 nn0cn 12520 . . . . . . . . . . . . . . 15 ((𝑚𝑧) ∈ ℕ0 → (𝑚𝑧) ∈ ℂ)
39 sub32 11531 . . . . . . . . . . . . . . 15 (((𝐹𝑧) ∈ ℂ ∧ (𝑗𝑧) ∈ ℂ ∧ (𝑚𝑧) ∈ ℂ) → (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧)) = (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧)))
4036, 37, 38, 39syl3an 1157 . . . . . . . . . . . . . 14 (((𝐹𝑧) ∈ ℕ0 ∧ (𝑗𝑧) ∈ ℕ0 ∧ (𝑚𝑧) ∈ ℕ0) → (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧)) = (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧)))
4124, 29, 35, 40syl3anc 1368 . . . . . . . . . . . . 13 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧)) = (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧)))
4241mpteq2dva 5249 . . . . . . . . . . . 12 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → (𝑧𝐼 ↦ (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧))) = (𝑧𝐼 ↦ (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧))))
4334ffnd 6724 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑚 Fn 𝐼)
4431, 43fndmexd 7912 . . . . . . . . . . . . 13 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝐼 ∈ V)
45 ovexd 7454 . . . . . . . . . . . . 13 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → ((𝐹𝑧) − (𝑗𝑧)) ∈ V)
4623feqmptd 6966 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝐹 = (𝑧𝐼 ↦ (𝐹𝑧)))
4728feqmptd 6966 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑗 = (𝑧𝐼 ↦ (𝑗𝑧)))
4844, 24, 29, 46, 47offval2 7705 . . . . . . . . . . . . 13 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → (𝐹f𝑗) = (𝑧𝐼 ↦ ((𝐹𝑧) − (𝑗𝑧))))
4934feqmptd 6966 . . . . . . . . . . . . 13 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑚 = (𝑧𝐼 ↦ (𝑚𝑧)))
5044, 45, 35, 48, 49offval2 7705 . . . . . . . . . . . 12 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑗) ∘f𝑚) = (𝑧𝐼 ↦ (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧))))
51 ovexd 7454 . . . . . . . . . . . . 13 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → ((𝐹𝑧) − (𝑚𝑧)) ∈ V)
5244, 24, 35, 46, 49offval2 7705 . . . . . . . . . . . . 13 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → (𝐹f𝑚) = (𝑧𝐼 ↦ ((𝐹𝑧) − (𝑚𝑧))))
5344, 51, 29, 52, 47offval2 7705 . . . . . . . . . . . 12 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑚) ∘f𝑗) = (𝑧𝐼 ↦ (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧))))
5442, 50, 533eqtr4d 2775 . . . . . . . . . . 11 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑗) ∘f𝑚) = ((𝐹f𝑚) ∘f𝑗))
551, 14psrbagconcl 21901 . . . . . . . . . . . 12 (((𝐹f𝑗) ∈ 𝐷𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑗) ∘f𝑚) ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
5613, 55sylan 578 . . . . . . . . . . 11 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑗) ∘f𝑚) ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
5754, 56eqeltrrd 2826 . . . . . . . . . 10 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑚) ∘f𝑗) ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
5854mpteq2dva 5249 . . . . . . . . . 10 ((𝜑𝑗𝑆) → (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)) = (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗)))
59 nfcv 2891 . . . . . . . . . . . 12 𝑛𝑋
60 nfcsb1v 3914 . . . . . . . . . . . 12 𝑘𝑛 / 𝑘𝑋
61 csbeq1a 3903 . . . . . . . . . . . 12 (𝑘 = 𝑛𝑋 = 𝑛 / 𝑘𝑋)
6259, 60, 61cbvmpt 5260 . . . . . . . . . . 11 (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑛 / 𝑘𝑋)
6362a1i 11 . . . . . . . . . 10 ((𝜑𝑗𝑆) → (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑛 / 𝑘𝑋))
64 csbeq1 3892 . . . . . . . . . 10 (𝑛 = ((𝐹f𝑚) ∘f𝑗) → 𝑛 / 𝑘𝑋 = ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
6557, 58, 63, 64fmptco 7138 . . . . . . . . 9 ((𝜑𝑗𝑆) → ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚))) = (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))
6665feq1d 6708 . . . . . . . 8 ((𝜑𝑗𝑆) → (((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚))):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶𝐵 ↔ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶𝐵))
6719, 66mpbid 231 . . . . . . 7 ((𝜑𝑗𝑆) → (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶𝐵)
6867fvmptelcdm 7122 . . . . . 6 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋𝐵)
6968anasss 465 . . . . 5 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋𝐵)
706, 69syldan 589 . . . 4 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋𝐵)
711, 2, 3, 4, 5, 70gsumbagdiag 21910 . . 3 (𝜑 → (𝐺 Σg (𝑚𝑆, 𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)) = (𝐺 Σg (𝑗𝑆, 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))
72 eqid 2725 . . . 4 (0g𝐺) = (0g𝐺)
731psrbaglefi 21899 . . . . . 6 (𝐹𝐷 → {𝑦𝐷𝑦r𝐹} ∈ Fin)
743, 73syl 17 . . . . 5 (𝜑 → {𝑦𝐷𝑦r𝐹} ∈ Fin)
752, 74eqeltrid 2829 . . . 4 (𝜑𝑆 ∈ Fin)
761, 2psrbagconcl 21901 . . . . . . 7 ((𝐹𝐷𝑚𝑆) → (𝐹f𝑚) ∈ 𝑆)
773, 76sylan 578 . . . . . 6 ((𝜑𝑚𝑆) → (𝐹f𝑚) ∈ 𝑆)
7810, 77sselid 3974 . . . . 5 ((𝜑𝑚𝑆) → (𝐹f𝑚) ∈ 𝐷)
791psrbaglefi 21899 . . . . 5 ((𝐹f𝑚) ∈ 𝐷 → {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ∈ Fin)
8078, 79syl 17 . . . 4 ((𝜑𝑚𝑆) → {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ∈ Fin)
81 xpfi 9346 . . . . 5 ((𝑆 ∈ Fin ∧ 𝑆 ∈ Fin) → (𝑆 × 𝑆) ∈ Fin)
8275, 75, 81syl2anc 582 . . . 4 (𝜑 → (𝑆 × 𝑆) ∈ Fin)
83 simprl 769 . . . . . . 7 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → 𝑚𝑆)
846simpld 493 . . . . . . 7 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → 𝑗𝑆)
85 brxp 5727 . . . . . . 7 (𝑚(𝑆 × 𝑆)𝑗 ↔ (𝑚𝑆𝑗𝑆))
8683, 84, 85sylanbrc 581 . . . . . 6 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → 𝑚(𝑆 × 𝑆)𝑗)
8786pm2.24d 151 . . . . 5 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → (¬ 𝑚(𝑆 × 𝑆)𝑗((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋 = (0g𝐺)))
8887impr 453 . . . 4 ((𝜑 ∧ ((𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)}) ∧ ¬ 𝑚(𝑆 × 𝑆)𝑗)) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋 = (0g𝐺))
894, 72, 5, 75, 80, 70, 82, 88gsum2d2 19958 . . 3 (𝜑 → (𝐺 Σg (𝑚𝑆, 𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)) = (𝐺 Σg (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
901psrbaglefi 21899 . . . . 5 ((𝐹f𝑗) ∈ 𝐷 → {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ∈ Fin)
9113, 90syl 17 . . . 4 ((𝜑𝑗𝑆) → {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ∈ Fin)
92 simprl 769 . . . . . . 7 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → 𝑗𝑆)
931, 2, 3gsumbagdiaglem 21909 . . . . . . . 8 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)}))
9493simpld 493 . . . . . . 7 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → 𝑚𝑆)
95 brxp 5727 . . . . . . 7 (𝑗(𝑆 × 𝑆)𝑚 ↔ (𝑗𝑆𝑚𝑆))
9692, 94, 95sylanbrc 581 . . . . . 6 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → 𝑗(𝑆 × 𝑆)𝑚)
9796pm2.24d 151 . . . . 5 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → (¬ 𝑗(𝑆 × 𝑆)𝑚((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋 = (0g𝐺)))
9897impr 453 . . . 4 ((𝜑 ∧ ((𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ ¬ 𝑗(𝑆 × 𝑆)𝑚)) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋 = (0g𝐺))
994, 72, 5, 75, 91, 69, 82, 98gsum2d2 19958 . . 3 (𝜑 → (𝐺 Σg (𝑗𝑆, 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
10071, 89, 993eqtr3d 2773 . 2 (𝜑 → (𝐺 Σg (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
1015adantr 479 . . . . . . . 8 ((𝜑𝑚𝑆) → 𝐺 ∈ CMnd)
10270anassrs 466 . . . . . . . . 9 (((𝜑𝑚𝑆) ∧ 𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)}) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋𝐵)
103102fmpttd 7124 . . . . . . . 8 ((𝜑𝑚𝑆) → (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋):{𝑥𝐷𝑥r ≤ (𝐹f𝑚)}⟶𝐵)
104 ovex 7452 . . . . . . . . . . . 12 (ℕ0m 𝐼) ∈ V
1051, 104rabex2 5337 . . . . . . . . . . 11 𝐷 ∈ V
106105a1i 11 . . . . . . . . . 10 ((𝜑𝑚𝑆) → 𝐷 ∈ V)
107 rabexg 5334 . . . . . . . . . 10 (𝐷 ∈ V → {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ∈ V)
108 mptexg 7233 . . . . . . . . . 10 ({𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ∈ V → (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) ∈ V)
109106, 107, 1083syl 18 . . . . . . . . 9 ((𝜑𝑚𝑆) → (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) ∈ V)
110 funmpt 6592 . . . . . . . . . 10 Fun (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
111110a1i 11 . . . . . . . . 9 ((𝜑𝑚𝑆) → Fun (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))
112 fvexd 6911 . . . . . . . . 9 ((𝜑𝑚𝑆) → (0g𝐺) ∈ V)
113 suppssdm 8182 . . . . . . . . . . 11 ((𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) supp (0g𝐺)) ⊆ dom (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
114 eqid 2725 . . . . . . . . . . . 12 (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) = (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
115114dmmptss 6247 . . . . . . . . . . 11 dom (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)}
116113, 115sstri 3986 . . . . . . . . . 10 ((𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)}
117116a1i 11 . . . . . . . . 9 ((𝜑𝑚𝑆) → ((𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})
118 suppssfifsupp 9410 . . . . . . . . 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 1375 . . . . . . . 8 ((𝜑𝑚𝑆) → (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) finSupp (0g𝐺))
1204, 72, 101, 80, 103, 119gsumcl 19899 . . . . . . 7 ((𝜑𝑚𝑆) → (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)) ∈ 𝐵)
121120fmpttd 7124 . . . . . 6 (𝜑 → (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))):𝑆𝐵)
1221, 2psrbagconf1o 21904 . . . . . . . 8 (𝐹𝐷 → (𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆)
1233, 122syl 17 . . . . . . 7 (𝜑 → (𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆)
124 f1ocnv 6850 . . . . . . 7 ((𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆(𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆)
125 f1of 6838 . . . . . . 7 ((𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆(𝑚𝑆 ↦ (𝐹f𝑚)):𝑆𝑆)
126123, 124, 1253syl 18 . . . . . 6 (𝜑(𝑚𝑆 ↦ (𝐹f𝑚)):𝑆𝑆)
127121, 126fcod 6749 . . . . 5 (𝜑 → ((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))):𝑆𝐵)
128 coass 6271 . . . . . . . 8 (((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ((𝑚𝑆 ↦ (𝐹f𝑚)) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))))
129 f1ococnv2 6865 . . . . . . . . . 10 ((𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆 → ((𝑚𝑆 ↦ (𝐹f𝑚)) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = ( I ↾ 𝑆))
130123, 129syl 17 . . . . . . . . 9 (𝜑 → ((𝑚𝑆 ↦ (𝐹f𝑚)) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = ( I ↾ 𝑆))
131130coeq2d 5865 . . . . . . . 8 (𝜑 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ((𝑚𝑆 ↦ (𝐹f𝑚)) ∘ (𝑚𝑆 ↦ (𝐹f𝑚)))) = ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)))
132128, 131eqtrid 2777 . . . . . . 7 (𝜑 → (((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)))
133 eqidd 2726 . . . . . . . . 9 (𝜑 → (𝑚𝑆 ↦ (𝐹f𝑚)) = (𝑚𝑆 ↦ (𝐹f𝑚)))
134 eqidd 2726 . . . . . . . . 9 (𝜑 → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))))
135 breq2 5153 . . . . . . . . . . . 12 (𝑛 = (𝐹f𝑚) → (𝑥r𝑛𝑥r ≤ (𝐹f𝑚)))
136135rabbidv 3426 . . . . . . . . . . 11 (𝑛 = (𝐹f𝑚) → {𝑥𝐷𝑥r𝑛} = {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})
137 ovex 7452 . . . . . . . . . . . . 13 (𝑛f𝑗) ∈ V
138 psrass1lem.y . . . . . . . . . . . . 13 (𝑘 = (𝑛f𝑗) → 𝑋 = 𝑌)
139137, 138csbie 3925 . . . . . . . . . . . 12 (𝑛f𝑗) / 𝑘𝑋 = 𝑌
140 oveq1 7426 . . . . . . . . . . . . 13 (𝑛 = (𝐹f𝑚) → (𝑛f𝑗) = ((𝐹f𝑚) ∘f𝑗))
141140csbeq1d 3893 . . . . . . . . . . . 12 (𝑛 = (𝐹f𝑚) → (𝑛f𝑗) / 𝑘𝑋 = ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
142139, 141eqtr3id 2779 . . . . . . . . . . 11 (𝑛 = (𝐹f𝑚) → 𝑌 = ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
143136, 142mpteq12dv 5240 . . . . . . . . . 10 (𝑛 = (𝐹f𝑚) → (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌) = (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))
144143oveq2d 7435 . . . . . . . . 9 (𝑛 = (𝐹f𝑚) → (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)) = (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))
14577, 133, 134, 144fmptco 7138 . . . . . . . 8 (𝜑 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))))
146145coeq1d 5864 . . . . . . 7 (𝜑 → (((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = ((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))))
147 coires1 6270 . . . . . . . . 9 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ↾ 𝑆)
148 ssid 3999 . . . . . . . . . 10 𝑆𝑆
149 resmpt 6042 . . . . . . . . . 10 (𝑆𝑆 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))))
150148, 149ax-mp 5 . . . . . . . . 9 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))
151147, 150eqtri 2753 . . . . . . . 8 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))
152151a1i 11 . . . . . . 7 (𝜑 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))))
153132, 146, 1523eqtr3d 2773 . . . . . 6 (𝜑 → ((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))))
154153feq1d 6708 . . . . 5 (𝜑 → (((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))):𝑆𝐵 ↔ (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))):𝑆𝐵))
155127, 154mpbid 231 . . . 4 (𝜑 → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))):𝑆𝐵)
156 rabexg 5334 . . . . . . . 8 (𝐷 ∈ V → {𝑦𝐷𝑦r𝐹} ∈ V)
157105, 156mp1i 13 . . . . . . 7 (𝜑 → {𝑦𝐷𝑦r𝐹} ∈ V)
1582, 157eqeltrid 2829 . . . . . 6 (𝜑𝑆 ∈ V)
159158mptexd 7236 . . . . 5 (𝜑 → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∈ V)
160 funmpt 6592 . . . . . 6 Fun (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))
161160a1i 11 . . . . 5 (𝜑 → Fun (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))))
162 fvexd 6911 . . . . 5 (𝜑 → (0g𝐺) ∈ V)
163 suppssdm 8182 . . . . . . 7 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) supp (0g𝐺)) ⊆ dom (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))
164 eqid 2725 . . . . . . . 8 (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))
165164dmmptss 6247 . . . . . . 7 dom (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ⊆ 𝑆
166163, 165sstri 3986 . . . . . 6 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) supp (0g𝐺)) ⊆ 𝑆
167166a1i 11 . . . . 5 (𝜑 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) supp (0g𝐺)) ⊆ 𝑆)
168 suppssfifsupp 9410 . . . . 5 ((((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∈ V ∧ Fun (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∧ (0g𝐺) ∈ V) ∧ (𝑆 ∈ Fin ∧ ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) supp (0g𝐺)) ⊆ 𝑆)) → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) finSupp (0g𝐺))
169159, 161, 162, 75, 167, 168syl32anc 1375 . . . 4 (𝜑 → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) finSupp (0g𝐺))
1704, 72, 5, 75, 155, 169, 123gsumf1o 19900 . . 3 (𝜑 → (𝐺 Σg (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))) = (𝐺 Σg ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚)))))
171145oveq2d 7435 . . 3 (𝜑 → (𝐺 Σg ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚)))) = (𝐺 Σg (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
172170, 171eqtrd 2765 . 2 (𝜑 → (𝐺 Σg (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
1735adantr 479 . . . . . 6 ((𝜑𝑗𝑆) → 𝐺 ∈ CMnd)
174105a1i 11 . . . . . . . 8 ((𝜑𝑗𝑆) → 𝐷 ∈ V)
175 rabexg 5334 . . . . . . . 8 (𝐷 ∈ V → {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ∈ V)
176 mptexg 7233 . . . . . . . 8 ({𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ∈ V → (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∈ V)
177174, 175, 1763syl 18 . . . . . . 7 ((𝜑𝑗𝑆) → (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∈ V)
178 funmpt 6592 . . . . . . . 8 Fun (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)
179178a1i 11 . . . . . . 7 ((𝜑𝑗𝑆) → Fun (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋))
180 fvexd 6911 . . . . . . 7 ((𝜑𝑗𝑆) → (0g𝐺) ∈ V)
181 suppssdm 8182 . . . . . . . . 9 ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) supp (0g𝐺)) ⊆ dom (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)
182 eqid 2725 . . . . . . . . . 10 (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) = (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)
183182dmmptss 6247 . . . . . . . . 9 dom (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}
184181, 183sstri 3986 . . . . . . . 8 ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}
185184a1i 11 . . . . . . 7 ((𝜑𝑗𝑆) → ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
186 suppssfifsupp 9410 . . . . . . 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 1375 . . . . . 6 ((𝜑𝑗𝑆) → (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) finSupp (0g𝐺))
1884, 72, 173, 91, 9, 187, 16gsumf1o 19900 . . . . 5 ((𝜑𝑗𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)) = (𝐺 Σg ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)))))
18965oveq2d 7435 . . . . 5 ((𝜑𝑗𝑆) → (𝐺 Σg ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)))) = (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))
190188, 189eqtrd 2765 . . . 4 ((𝜑𝑗𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)) = (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))
191190mpteq2dva 5249 . . 3 (𝜑 → (𝑗𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋))) = (𝑗𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))))
192191oveq2d 7435 . 2 (𝜑 → (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)))) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
193100, 172, 1923eqtr4d 2775 1 (𝜑 → (𝐺 Σg (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394   = wceq 1533  wcel 2098  {crab 3418  Vcvv 3461  csb 3889  wss 3944   class class class wbr 5149  cmpt 5232   I cid 5575   × cxp 5676  ccnv 5677  dom cdm 5678  cres 5680  cima 5681  ccom 5682  Fun wfun 6543  wf 6545  1-1-ontowf1o 6548  cfv 6549  (class class class)co 7419  cmpo 7421  f cof 7683  r cofr 7684   supp csupp 8165  m cmap 8845  Fincfn 8964   finSupp cfsupp 9392  cc 11143  cle 11286  cmin 11481  cn 12250  0cn0 12510  Basecbs 17199  0gc0g 17440   Σg cgsu 17441  CMndccmn 19764
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 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11201  ax-resscn 11202  ax-1cn 11203  ax-icn 11204  ax-addcl 11205  ax-addrcl 11206  ax-mulcl 11207  ax-mulrcl 11208  ax-mulcom 11209  ax-addass 11210  ax-mulass 11211  ax-distr 11212  ax-i2m1 11213  ax-1ne0 11214  ax-1rid 11215  ax-rnegex 11216  ax-rrecex 11217  ax-cnre 11218  ax-pre-lttri 11219  ax-pre-lttrn 11220  ax-pre-ltadd 11221  ax-pre-mulgt0 11222
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 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-iin 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7685  df-ofr 7686  df-om 7872  df-1st 7994  df-2nd 7995  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-er 8725  df-map 8847  df-pm 8848  df-ixp 8917  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9393  df-oi 9540  df-card 9969  df-pnf 11287  df-mnf 11288  df-xr 11289  df-ltxr 11290  df-le 11291  df-sub 11483  df-neg 11484  df-nn 12251  df-2 12313  df-n0 12511  df-z 12597  df-uz 12861  df-fz 13525  df-fzo 13668  df-seq 14008  df-hash 14334  df-sets 17152  df-slot 17170  df-ndx 17182  df-base 17200  df-ress 17229  df-plusg 17265  df-0g 17442  df-gsum 17443  df-mre 17585  df-mrc 17586  df-acs 17588  df-mgm 18619  df-sgrp 18698  df-mnd 18714  df-submnd 18760  df-mulg 19048  df-cntz 19297  df-cmn 19766
This theorem is referenced by:  psrass1  21943
  Copyright terms: Public domain W3C validator