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

Theorem psrass1lemOLD 20716
 Description: Obsolete version of psrass1lem 20719 as of 7-Aug-2024. (Contributed by Mario Carneiro, 5-Jan-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
psrbag.d 𝐷 = {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
psrbagconf1o.s 𝑆 = {𝑦𝐷𝑦r𝐹}
gsumbagdiagOLD.i (𝜑𝐼𝑉)
gsumbagdiagOLD.f (𝜑𝐹𝐷)
gsumbagdiagOLD.b 𝐵 = (Base‘𝐺)
gsumbagdiagOLD.g (𝜑𝐺 ∈ CMnd)
gsumbagdiagOLD.x ((𝜑 ∧ (𝑗𝑆𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → 𝑋𝐵)
psrass1lemOLD.y (𝑘 = (𝑛f𝑗) → 𝑋 = 𝑌)
Assertion
Ref Expression
psrass1lemOLD (𝜑 → (𝐺 Σg (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)))))
Distinct variable groups:   𝑓,𝑗,𝑘,𝑛,𝑥,𝑦,𝐹   𝑓,𝐺,𝑗,𝑘,𝑛,𝑥,𝑦   𝑛,𝑉,𝑥,𝑦   𝑓,𝐼,𝑛,𝑥,𝑦   𝜑,𝑗,𝑘   𝑆,𝑗,𝑘,𝑛,𝑥   𝐵,𝑗,𝑘   𝐷,𝑗,𝑘,𝑛,𝑥,𝑦   𝑓,𝑋,𝑛,𝑥,𝑦   𝑓,𝑌,𝑘,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑓,𝑛)   𝐵(𝑥,𝑦,𝑓,𝑛)   𝐷(𝑓)   𝑆(𝑦,𝑓)   𝐼(𝑗,𝑘)   𝑉(𝑓,𝑗,𝑘)   𝑋(𝑗,𝑘)   𝑌(𝑗,𝑛)

Proof of Theorem psrass1lemOLD
Dummy variables 𝑚 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 psrbag.d . . . 4 𝐷 = {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
2 psrbagconf1o.s . . . 4 𝑆 = {𝑦𝐷𝑦r𝐹}
3 gsumbagdiagOLD.i . . . 4 (𝜑𝐼𝑉)
4 gsumbagdiagOLD.f . . . 4 (𝜑𝐹𝐷)
5 gsumbagdiagOLD.b . . . 4 𝐵 = (Base‘𝐺)
6 gsumbagdiagOLD.g . . . 4 (𝜑𝐺 ∈ CMnd)
71, 2, 3, 4gsumbagdiaglemOLD 20714 . . . . 5 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}))
8 gsumbagdiagOLD.x . . . . . . . . . . 11 ((𝜑 ∧ (𝑗𝑆𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → 𝑋𝐵)
98anassrs 471 . . . . . . . . . 10 (((𝜑𝑗𝑆) ∧ 𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑋𝐵)
109fmpttd 6876 . . . . . . . . 9 ((𝜑𝑗𝑆) → (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶𝐵)
113adantr 484 . . . . . . . . . . 11 ((𝜑𝑗𝑆) → 𝐼𝑉)
122ssrab3 3988 . . . . . . . . . . . 12 𝑆𝐷
134adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑗𝑆) → 𝐹𝐷)
14 simpr 488 . . . . . . . . . . . . 13 ((𝜑𝑗𝑆) → 𝑗𝑆)
151, 2psrbagconclOLD 20711 . . . . . . . . . . . . 13 ((𝐼𝑉𝐹𝐷𝑗𝑆) → (𝐹f𝑗) ∈ 𝑆)
1611, 13, 14, 15syl3anc 1368 . . . . . . . . . . . 12 ((𝜑𝑗𝑆) → (𝐹f𝑗) ∈ 𝑆)
1712, 16sseldi 3892 . . . . . . . . . . 11 ((𝜑𝑗𝑆) → (𝐹f𝑗) ∈ 𝐷)
18 eqid 2758 . . . . . . . . . . . 12 {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} = {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}
191, 18psrbagconf1oOLD 20713 . . . . . . . . . . 11 ((𝐼𝑉 ∧ (𝐹f𝑗) ∈ 𝐷) → (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}–1-1-onto→{𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
2011, 17, 19syl2anc 587 . . . . . . . . . 10 ((𝜑𝑗𝑆) → (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}–1-1-onto→{𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
21 f1of 6607 . . . . . . . . . 10 ((𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}–1-1-onto→{𝑥𝐷𝑥r ≤ (𝐹f𝑗)} → (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶{𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
2220, 21syl 17 . . . . . . . . 9 ((𝜑𝑗𝑆) → (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶{𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
23 fco 6521 . . . . . . . . 9 (((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶𝐵 ∧ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚))):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶𝐵)
2410, 22, 23syl2anc 587 . . . . . . . 8 ((𝜑𝑗𝑆) → ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚))):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶𝐵)
2511adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝐼𝑉)
2613adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝐹𝐷)
271psrbagfOLD 20695 . . . . . . . . . . . . . . . 16 ((𝐼𝑉𝐹𝐷) → 𝐹:𝐼⟶ℕ0)
2825, 26, 27syl2anc 587 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝐹:𝐼⟶ℕ0)
2928ffvelrnda 6848 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → (𝐹𝑧) ∈ ℕ0)
3014adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑗𝑆)
3112, 30sseldi 3892 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑗𝐷)
321psrbagfOLD 20695 . . . . . . . . . . . . . . . 16 ((𝐼𝑉𝑗𝐷) → 𝑗:𝐼⟶ℕ0)
3325, 31, 32syl2anc 587 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑗:𝐼⟶ℕ0)
3433ffvelrnda 6848 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → (𝑗𝑧) ∈ ℕ0)
35 ssrab2 3986 . . . . . . . . . . . . . . . . 17 {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ⊆ 𝐷
36 simpr 488 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
3735, 36sseldi 3892 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑚𝐷)
381psrbagfOLD 20695 . . . . . . . . . . . . . . . 16 ((𝐼𝑉𝑚𝐷) → 𝑚:𝐼⟶ℕ0)
3925, 37, 38syl2anc 587 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑚:𝐼⟶ℕ0)
4039ffvelrnda 6848 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → (𝑚𝑧) ∈ ℕ0)
41 nn0cn 11957 . . . . . . . . . . . . . . 15 ((𝐹𝑧) ∈ ℕ0 → (𝐹𝑧) ∈ ℂ)
42 nn0cn 11957 . . . . . . . . . . . . . . 15 ((𝑗𝑧) ∈ ℕ0 → (𝑗𝑧) ∈ ℂ)
43 nn0cn 11957 . . . . . . . . . . . . . . 15 ((𝑚𝑧) ∈ ℕ0 → (𝑚𝑧) ∈ ℂ)
44 sub32 10971 . . . . . . . . . . . . . . 15 (((𝐹𝑧) ∈ ℂ ∧ (𝑗𝑧) ∈ ℂ ∧ (𝑚𝑧) ∈ ℂ) → (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧)) = (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧)))
4541, 42, 43, 44syl3an 1157 . . . . . . . . . . . . . 14 (((𝐹𝑧) ∈ ℕ0 ∧ (𝑗𝑧) ∈ ℕ0 ∧ (𝑚𝑧) ∈ ℕ0) → (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧)) = (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧)))
4629, 34, 40, 45syl3anc 1368 . . . . . . . . . . . . 13 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧)) = (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧)))
4746mpteq2dva 5131 . . . . . . . . . . . 12 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → (𝑧𝐼 ↦ (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧))) = (𝑧𝐼 ↦ (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧))))
48 ovexd 7191 . . . . . . . . . . . . 13 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → ((𝐹𝑧) − (𝑗𝑧)) ∈ V)
4928feqmptd 6726 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝐹 = (𝑧𝐼 ↦ (𝐹𝑧)))
5033feqmptd 6726 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑗 = (𝑧𝐼 ↦ (𝑗𝑧)))
5125, 29, 34, 49, 50offval2 7430 . . . . . . . . . . . . 13 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → (𝐹f𝑗) = (𝑧𝐼 ↦ ((𝐹𝑧) − (𝑗𝑧))))
5239feqmptd 6726 . . . . . . . . . . . . 13 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → 𝑚 = (𝑧𝐼 ↦ (𝑚𝑧)))
5325, 48, 40, 51, 52offval2 7430 . . . . . . . . . . . 12 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑗) ∘f𝑚) = (𝑧𝐼 ↦ (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧))))
54 ovexd 7191 . . . . . . . . . . . . 13 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ 𝑧𝐼) → ((𝐹𝑧) − (𝑚𝑧)) ∈ V)
5525, 29, 40, 49, 52offval2 7430 . . . . . . . . . . . . 13 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → (𝐹f𝑚) = (𝑧𝐼 ↦ ((𝐹𝑧) − (𝑚𝑧))))
5625, 54, 34, 55, 50offval2 7430 . . . . . . . . . . . 12 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑚) ∘f𝑗) = (𝑧𝐼 ↦ (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧))))
5747, 53, 563eqtr4d 2803 . . . . . . . . . . 11 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑗) ∘f𝑚) = ((𝐹f𝑚) ∘f𝑗))
5817adantr 484 . . . . . . . . . . . 12 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → (𝐹f𝑗) ∈ 𝐷)
591, 18psrbagconclOLD 20711 . . . . . . . . . . . 12 ((𝐼𝑉 ∧ (𝐹f𝑗) ∈ 𝐷𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑗) ∘f𝑚) ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
6025, 58, 36, 59syl3anc 1368 . . . . . . . . . . 11 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑗) ∘f𝑚) ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
6157, 60eqeltrrd 2853 . . . . . . . . . 10 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑚) ∘f𝑗) ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
6257mpteq2dva 5131 . . . . . . . . . 10 ((𝜑𝑗𝑆) → (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)) = (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗)))
63 nfcv 2919 . . . . . . . . . . . 12 𝑛𝑋
64 nfcsb1v 3831 . . . . . . . . . . . 12 𝑘𝑛 / 𝑘𝑋
65 csbeq1a 3821 . . . . . . . . . . . 12 (𝑘 = 𝑛𝑋 = 𝑛 / 𝑘𝑋)
6663, 64, 65cbvmpt 5137 . . . . . . . . . . 11 (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑛 / 𝑘𝑋)
6766a1i 11 . . . . . . . . . 10 ((𝜑𝑗𝑆) → (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑛 / 𝑘𝑋))
68 csbeq1 3810 . . . . . . . . . 10 (𝑛 = ((𝐹f𝑚) ∘f𝑗) → 𝑛 / 𝑘𝑋 = ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
6961, 62, 67, 68fmptco 6888 . . . . . . . . 9 ((𝜑𝑗𝑆) → ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚))) = (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))
7069feq1d 6488 . . . . . . . 8 ((𝜑𝑗𝑆) → (((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚))):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶𝐵 ↔ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶𝐵))
7124, 70mpbid 235 . . . . . . 7 ((𝜑𝑗𝑆) → (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋):{𝑥𝐷𝑥r ≤ (𝐹f𝑗)}⟶𝐵)
7271fvmptelrn 6874 . . . . . 6 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋𝐵)
7372anasss 470 . . . . 5 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋𝐵)
747, 73syldan 594 . . . 4 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋𝐵)
751, 2, 3, 4, 5, 6, 74gsumbagdiagOLD 20715 . . 3 (𝜑 → (𝐺 Σg (𝑚𝑆, 𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)) = (𝐺 Σg (𝑗𝑆, 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))
76 eqid 2758 . . . 4 (0g𝐺) = (0g𝐺)
771psrbaglefiOLD 20709 . . . . . 6 ((𝐼𝑉𝐹𝐷) → {𝑦𝐷𝑦r𝐹} ∈ Fin)
783, 4, 77syl2anc 587 . . . . 5 (𝜑 → {𝑦𝐷𝑦r𝐹} ∈ Fin)
792, 78eqeltrid 2856 . . . 4 (𝜑𝑆 ∈ Fin)
803adantr 484 . . . . 5 ((𝜑𝑚𝑆) → 𝐼𝑉)
814adantr 484 . . . . . . 7 ((𝜑𝑚𝑆) → 𝐹𝐷)
82 simpr 488 . . . . . . 7 ((𝜑𝑚𝑆) → 𝑚𝑆)
831, 2psrbagconclOLD 20711 . . . . . . 7 ((𝐼𝑉𝐹𝐷𝑚𝑆) → (𝐹f𝑚) ∈ 𝑆)
8480, 81, 82, 83syl3anc 1368 . . . . . 6 ((𝜑𝑚𝑆) → (𝐹f𝑚) ∈ 𝑆)
8512, 84sseldi 3892 . . . . 5 ((𝜑𝑚𝑆) → (𝐹f𝑚) ∈ 𝐷)
861psrbaglefiOLD 20709 . . . . 5 ((𝐼𝑉 ∧ (𝐹f𝑚) ∈ 𝐷) → {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ∈ Fin)
8780, 85, 86syl2anc 587 . . . 4 ((𝜑𝑚𝑆) → {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ∈ Fin)
88 xpfi 8835 . . . . 5 ((𝑆 ∈ Fin ∧ 𝑆 ∈ Fin) → (𝑆 × 𝑆) ∈ Fin)
8979, 79, 88syl2anc 587 . . . 4 (𝜑 → (𝑆 × 𝑆) ∈ Fin)
90 simprl 770 . . . . . . 7 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → 𝑚𝑆)
917simpld 498 . . . . . . 7 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → 𝑗𝑆)
92 brxp 5575 . . . . . . 7 (𝑚(𝑆 × 𝑆)𝑗 ↔ (𝑚𝑆𝑗𝑆))
9390, 91, 92sylanbrc 586 . . . . . 6 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → 𝑚(𝑆 × 𝑆)𝑗)
9493pm2.24d 154 . . . . 5 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})) → (¬ 𝑚(𝑆 × 𝑆)𝑗((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋 = (0g𝐺)))
9594impr 458 . . . 4 ((𝜑 ∧ ((𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)}) ∧ ¬ 𝑚(𝑆 × 𝑆)𝑗)) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋 = (0g𝐺))
965, 76, 6, 79, 87, 74, 89, 95gsum2d2 19176 . . 3 (𝜑 → (𝐺 Σg (𝑚𝑆, 𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)) = (𝐺 Σg (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
971psrbaglefiOLD 20709 . . . . 5 ((𝐼𝑉 ∧ (𝐹f𝑗) ∈ 𝐷) → {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ∈ Fin)
9811, 17, 97syl2anc 587 . . . 4 ((𝜑𝑗𝑆) → {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ∈ Fin)
99 simprl 770 . . . . . . 7 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → 𝑗𝑆)
1001, 2, 3, 4gsumbagdiaglemOLD 20714 . . . . . . . 8 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)}))
101100simpld 498 . . . . . . 7 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → 𝑚𝑆)
102 brxp 5575 . . . . . . 7 (𝑗(𝑆 × 𝑆)𝑚 ↔ (𝑗𝑆𝑚𝑆))
10399, 101, 102sylanbrc 586 . . . . . 6 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → 𝑗(𝑆 × 𝑆)𝑚)
104103pm2.24d 154 . . . . 5 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → (¬ 𝑗(𝑆 × 𝑆)𝑚((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋 = (0g𝐺)))
105104impr 458 . . . 4 ((𝜑 ∧ ((𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}) ∧ ¬ 𝑗(𝑆 × 𝑆)𝑚)) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋 = (0g𝐺))
1065, 76, 6, 79, 98, 73, 89, 105gsum2d2 19176 . . 3 (𝜑 → (𝐺 Σg (𝑗𝑆, 𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
10775, 96, 1063eqtr3d 2801 . 2 (𝜑 → (𝐺 Σg (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
1086adantr 484 . . . . . . . 8 ((𝜑𝑚𝑆) → 𝐺 ∈ CMnd)
10974anassrs 471 . . . . . . . . 9 (((𝜑𝑚𝑆) ∧ 𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)}) → ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋𝐵)
110109fmpttd 6876 . . . . . . . 8 ((𝜑𝑚𝑆) → (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋):{𝑥𝐷𝑥r ≤ (𝐹f𝑚)}⟶𝐵)
111 ovex 7189 . . . . . . . . . . . 12 (ℕ0m 𝐼) ∈ V
1121, 111rabex2 5208 . . . . . . . . . . 11 𝐷 ∈ V
113112a1i 11 . . . . . . . . . 10 ((𝜑𝑚𝑆) → 𝐷 ∈ V)
114 rabexg 5205 . . . . . . . . . 10 (𝐷 ∈ V → {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ∈ V)
115 mptexg 6981 . . . . . . . . . 10 ({𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ∈ V → (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) ∈ V)
116113, 114, 1153syl 18 . . . . . . . . 9 ((𝜑𝑚𝑆) → (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) ∈ V)
117 funmpt 6378 . . . . . . . . . 10 Fun (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
118117a1i 11 . . . . . . . . 9 ((𝜑𝑚𝑆) → Fun (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))
119 fvexd 6678 . . . . . . . . 9 ((𝜑𝑚𝑆) → (0g𝐺) ∈ V)
120 suppssdm 7857 . . . . . . . . . . 11 ((𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) supp (0g𝐺)) ⊆ dom (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
121 eqid 2758 . . . . . . . . . . . 12 (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) = (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
122121dmmptss 6075 . . . . . . . . . . 11 dom (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)}
123120, 122sstri 3903 . . . . . . . . . 10 ((𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)}
124123a1i 11 . . . . . . . . 9 ((𝜑𝑚𝑆) → ((𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})
125 suppssfifsupp 8894 . . . . . . . . 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𝐺))
126116, 118, 119, 87, 124, 125syl32anc 1375 . . . . . . . 8 ((𝜑𝑚𝑆) → (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋) finSupp (0g𝐺))
1275, 76, 108, 87, 110, 126gsumcl 19117 . . . . . . 7 ((𝜑𝑚𝑆) → (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)) ∈ 𝐵)
128127fmpttd 6876 . . . . . 6 (𝜑 → (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))):𝑆𝐵)
1291, 2psrbagconf1oOLD 20713 . . . . . . . 8 ((𝐼𝑉𝐹𝐷) → (𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆)
1303, 4, 129syl2anc 587 . . . . . . 7 (𝜑 → (𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆)
131 f1ocnv 6619 . . . . . . 7 ((𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆(𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆)
132 f1of 6607 . . . . . . 7 ((𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆(𝑚𝑆 ↦ (𝐹f𝑚)):𝑆𝑆)
133130, 131, 1323syl 18 . . . . . 6 (𝜑(𝑚𝑆 ↦ (𝐹f𝑚)):𝑆𝑆)
134 fco 6521 . . . . . 6 (((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))):𝑆𝐵(𝑚𝑆 ↦ (𝐹f𝑚)):𝑆𝑆) → ((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))):𝑆𝐵)
135128, 133, 134syl2anc 587 . . . . 5 (𝜑 → ((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))):𝑆𝐵)
136 coass 6100 . . . . . . . 8 (((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ((𝑚𝑆 ↦ (𝐹f𝑚)) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))))
137 f1ococnv2 6633 . . . . . . . . . 10 ((𝑚𝑆 ↦ (𝐹f𝑚)):𝑆1-1-onto𝑆 → ((𝑚𝑆 ↦ (𝐹f𝑚)) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = ( I ↾ 𝑆))
138130, 137syl 17 . . . . . . . . 9 (𝜑 → ((𝑚𝑆 ↦ (𝐹f𝑚)) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = ( I ↾ 𝑆))
139138coeq2d 5708 . . . . . . . 8 (𝜑 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ((𝑚𝑆 ↦ (𝐹f𝑚)) ∘ (𝑚𝑆 ↦ (𝐹f𝑚)))) = ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)))
140136, 139syl5eq 2805 . . . . . . 7 (𝜑 → (((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)))
141 eqidd 2759 . . . . . . . . 9 (𝜑 → (𝑚𝑆 ↦ (𝐹f𝑚)) = (𝑚𝑆 ↦ (𝐹f𝑚)))
142 eqidd 2759 . . . . . . . . 9 (𝜑 → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))))
143 breq2 5040 . . . . . . . . . . . 12 (𝑛 = (𝐹f𝑚) → (𝑥r𝑛𝑥r ≤ (𝐹f𝑚)))
144143rabbidv 3392 . . . . . . . . . . 11 (𝑛 = (𝐹f𝑚) → {𝑥𝐷𝑥r𝑛} = {𝑥𝐷𝑥r ≤ (𝐹f𝑚)})
145 ovex 7189 . . . . . . . . . . . . 13 (𝑛f𝑗) ∈ V
146 psrass1lemOLD.y . . . . . . . . . . . . 13 (𝑘 = (𝑛f𝑗) → 𝑋 = 𝑌)
147145, 146csbie 3842 . . . . . . . . . . . 12 (𝑛f𝑗) / 𝑘𝑋 = 𝑌
148 oveq1 7163 . . . . . . . . . . . . 13 (𝑛 = (𝐹f𝑚) → (𝑛f𝑗) = ((𝐹f𝑚) ∘f𝑗))
149148csbeq1d 3811 . . . . . . . . . . . 12 (𝑛 = (𝐹f𝑚) → (𝑛f𝑗) / 𝑘𝑋 = ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
150147, 149eqtr3id 2807 . . . . . . . . . . 11 (𝑛 = (𝐹f𝑚) → 𝑌 = ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)
151144, 150mpteq12dv 5121 . . . . . . . . . 10 (𝑛 = (𝐹f𝑚) → (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌) = (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))
152151oveq2d 7172 . . . . . . . . 9 (𝑛 = (𝐹f𝑚) → (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)) = (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))
15384, 141, 142, 152fmptco 6888 . . . . . . . 8 (𝜑 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))))
154153coeq1d 5707 . . . . . . 7 (𝜑 → (((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = ((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))))
155 coires1 6099 . . . . . . . . 9 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ↾ 𝑆)
156 ssid 3916 . . . . . . . . . 10 𝑆𝑆
157 resmpt 5882 . . . . . . . . . 10 (𝑆𝑆 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))))
158156, 157ax-mp 5 . . . . . . . . 9 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))
159155, 158eqtri 2781 . . . . . . . 8 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))
160159a1i 11 . . . . . . 7 (𝜑 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))))
161140, 154, 1603eqtr3d 2801 . . . . . 6 (𝜑 → ((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))))
162161feq1d 6488 . . . . 5 (𝜑 → (((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚))):𝑆𝐵 ↔ (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))):𝑆𝐵))
163135, 162mpbid 235 . . . 4 (𝜑 → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))):𝑆𝐵)
164 rabexg 5205 . . . . . . . 8 (𝐷 ∈ V → {𝑦𝐷𝑦r𝐹} ∈ V)
165112, 164mp1i 13 . . . . . . 7 (𝜑 → {𝑦𝐷𝑦r𝐹} ∈ V)
1662, 165eqeltrid 2856 . . . . . 6 (𝜑𝑆 ∈ V)
167166mptexd 6984 . . . . 5 (𝜑 → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∈ V)
168 funmpt 6378 . . . . . 6 Fun (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))
169168a1i 11 . . . . 5 (𝜑 → Fun (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))))
170 fvexd 6678 . . . . 5 (𝜑 → (0g𝐺) ∈ V)
171 suppssdm 7857 . . . . . . 7 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) supp (0g𝐺)) ⊆ dom (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))
172 eqid 2758 . . . . . . . 8 (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))
173172dmmptss 6075 . . . . . . 7 dom (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ⊆ 𝑆
174171, 173sstri 3903 . . . . . 6 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) supp (0g𝐺)) ⊆ 𝑆
175174a1i 11 . . . . 5 (𝜑 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) supp (0g𝐺)) ⊆ 𝑆)
176 suppssfifsupp 8894 . . . . 5 ((((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∈ V ∧ Fun (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∧ (0g𝐺) ∈ V) ∧ (𝑆 ∈ Fin ∧ ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) supp (0g𝐺)) ⊆ 𝑆)) → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) finSupp (0g𝐺))
177167, 169, 170, 79, 175, 176syl32anc 1375 . . . 4 (𝜑 → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) finSupp (0g𝐺))
1785, 76, 6, 79, 163, 177, 130gsumf1o 19118 . . 3 (𝜑 → (𝐺 Σg (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))) = (𝐺 Σg ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚)))))
179153oveq2d 7172 . . 3 (𝜑 → (𝐺 Σg ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹f𝑚)))) = (𝐺 Σg (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
180178, 179eqtrd 2793 . 2 (𝜑 → (𝐺 Σg (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑚)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
1816adantr 484 . . . . . 6 ((𝜑𝑗𝑆) → 𝐺 ∈ CMnd)
182112a1i 11 . . . . . . . 8 ((𝜑𝑗𝑆) → 𝐷 ∈ V)
183 rabexg 5205 . . . . . . . 8 (𝐷 ∈ V → {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ∈ V)
184 mptexg 6981 . . . . . . . 8 ({𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ∈ V → (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∈ V)
185182, 183, 1843syl 18 . . . . . . 7 ((𝜑𝑗𝑆) → (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∈ V)
186 funmpt 6378 . . . . . . . 8 Fun (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)
187186a1i 11 . . . . . . 7 ((𝜑𝑗𝑆) → Fun (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋))
188 fvexd 6678 . . . . . . 7 ((𝜑𝑗𝑆) → (0g𝐺) ∈ V)
189 suppssdm 7857 . . . . . . . . 9 ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) supp (0g𝐺)) ⊆ dom (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)
190 eqid 2758 . . . . . . . . . 10 (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) = (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)
191190dmmptss 6075 . . . . . . . . 9 dom (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}
192189, 191sstri 3903 . . . . . . . 8 ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)}
193192a1i 11 . . . . . . 7 ((𝜑𝑗𝑆) → ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})
194 suppssfifsupp 8894 . . . . . . 7 ((((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∈ V ∧ Fun (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∧ (0g𝐺) ∈ V) ∧ ({𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ∈ Fin ∧ ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)})) → (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) finSupp (0g𝐺))
195185, 187, 188, 98, 193, 194syl32anc 1375 . . . . . 6 ((𝜑𝑗𝑆) → (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) finSupp (0g𝐺))
1965, 76, 181, 98, 10, 195, 20gsumf1o 19118 . . . . 5 ((𝜑𝑗𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)) = (𝐺 Σg ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)))))
19769oveq2d 7172 . . . . 5 ((𝜑𝑗𝑆) → (𝐺 Σg ((𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑗) ∘f𝑚)))) = (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))
198196, 197eqtrd 2793 . . . 4 ((𝜑𝑗𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)) = (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))
199198mpteq2dva 5131 . . 3 (𝜑 → (𝑗𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋))) = (𝑗𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋))))
200199oveq2d 7172 . 2 (𝜑 → (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)))) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ ((𝐹f𝑚) ∘f𝑗) / 𝑘𝑋)))))
201107, 180, 2003eqtr4d 2803 1 (𝜑 → (𝐺 Σg (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥r𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥r ≤ (𝐹f𝑗)} ↦ 𝑋)))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {crab 3074  Vcvv 3409  ⦋csb 3807   ⊆ wss 3860   class class class wbr 5036   ↦ cmpt 5116   I cid 5433   × cxp 5526  ◡ccnv 5527  dom cdm 5528   ↾ cres 5530   “ cima 5531   ∘ ccom 5532  Fun wfun 6334  ⟶wf 6336  –1-1-onto→wf1o 6339  ‘cfv 6340  (class class class)co 7156   ∈ cmpo 7158   ∘f cof 7409   ∘r cofr 7410   supp csupp 7841   ↑m cmap 8422  Fincfn 8540   finSupp cfsupp 8879  ℂcc 10586   ≤ cle 10727   − cmin 10921  ℕcn 11687  ℕ0cn0 11947  Basecbs 16555  0gc0g 16785   Σg cgsu 16786  CMndccmn 18987 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 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465  ax-cnex 10644  ax-resscn 10645  ax-1cn 10646  ax-icn 10647  ax-addcl 10648  ax-addrcl 10649  ax-mulcl 10650  ax-mulrcl 10651  ax-mulcom 10652  ax-addass 10653  ax-mulass 10654  ax-distr 10655  ax-i2m1 10656  ax-1ne0 10657  ax-1rid 10658  ax-rnegex 10659  ax-rrecex 10660  ax-cnre 10661  ax-pre-lttri 10662  ax-pre-lttrn 10663  ax-pre-ltadd 10664  ax-pre-mulgt0 10665 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-iin 4889  df-br 5037  df-opab 5099  df-mpt 5117  df-tr 5143  df-id 5434  df-eprel 5439  df-po 5447  df-so 5448  df-fr 5487  df-se 5488  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6131  df-ord 6177  df-on 6178  df-lim 6179  df-suc 6180  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-isom 6349  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-of 7411  df-ofr 7412  df-om 7586  df-1st 7699  df-2nd 7700  df-supp 7842  df-wrecs 7963  df-recs 8024  df-rdg 8062  df-1o 8118  df-er 8305  df-map 8424  df-pm 8425  df-ixp 8493  df-en 8541  df-dom 8542  df-sdom 8543  df-fin 8544  df-fsupp 8880  df-oi 9020  df-card 9414  df-pnf 10728  df-mnf 10729  df-xr 10730  df-ltxr 10731  df-le 10732  df-sub 10923  df-neg 10924  df-nn 11688  df-2 11750  df-n0 11948  df-z 12034  df-uz 12296  df-fz 12953  df-fzo 13096  df-seq 13432  df-hash 13754  df-ndx 16558  df-slot 16559  df-base 16561  df-sets 16562  df-ress 16563  df-plusg 16650  df-0g 16787  df-gsum 16788  df-mre 16929  df-mrc 16930  df-acs 16932  df-mgm 17932  df-sgrp 17981  df-mnd 17992  df-submnd 18037  df-mulg 18306  df-cntz 18528  df-cmn 18989 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator