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

Theorem psrass1lem 19140
Description: A group sum commutation used by psrass1 19168. (Contributed by Mario Carneiro, 5-Jan-2015.)
Hypotheses
Ref Expression
psrbag.d 𝐷 = {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
psrbagconf1o.1 𝑆 = {𝑦𝐷𝑦𝑟𝐹}
gsumbagdiag.i (𝜑𝐼𝑉)
gsumbagdiag.f (𝜑𝐹𝐷)
gsumbagdiag.b 𝐵 = (Base‘𝐺)
gsumbagdiag.g (𝜑𝐺 ∈ CMnd)
gsumbagdiag.x ((𝜑 ∧ (𝑗𝑆𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})) → 𝑋𝐵)
psrass1lem.y (𝑘 = (𝑛𝑓𝑗) → 𝑋 = 𝑌)
Assertion
Ref Expression
psrass1lem (𝜑 → (𝐺 Σg (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋)))))
Distinct variable groups:   𝑓,𝑗,𝑘,𝑛,𝑥,𝑦,𝐹   𝑓,𝐺,𝑗,𝑘,𝑛,𝑥,𝑦   𝑛,𝑉,𝑥,𝑦   𝑓,𝐼,𝑛,𝑥,𝑦   𝜑,𝑗,𝑘   𝑆,𝑗,𝑘,𝑛,𝑥   𝐵,𝑗,𝑘   𝐷,𝑗,𝑘,𝑛,𝑥,𝑦   𝑓,𝑋,𝑛,𝑥,𝑦   𝑓,𝑌,𝑘,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑓,𝑛)   𝐵(𝑥,𝑦,𝑓,𝑛)   𝐷(𝑓)   𝑆(𝑦,𝑓)   𝐼(𝑗,𝑘)   𝑉(𝑓,𝑗,𝑘)   𝑋(𝑗,𝑘)   𝑌(𝑗,𝑛)

Proof of Theorem psrass1lem
Dummy variables 𝑚 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 psrbag.d . . . 4 𝐷 = {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
2 psrbagconf1o.1 . . . 4 𝑆 = {𝑦𝐷𝑦𝑟𝐹}
3 gsumbagdiag.i . . . 4 (𝜑𝐼𝑉)
4 gsumbagdiag.f . . . 4 (𝜑𝐹𝐷)
5 gsumbagdiag.b . . . 4 𝐵 = (Base‘𝐺)
6 gsumbagdiag.g . . . 4 (𝜑𝐺 ∈ CMnd)
71, 2, 3, 4gsumbagdiaglem 19138 . . . . 5 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)})) → (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}))
8 gsumbagdiag.x . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗𝑆𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})) → 𝑋𝐵)
98anassrs 677 . . . . . . . . . . 11 (((𝜑𝑗𝑆) ∧ 𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → 𝑋𝐵)
10 eqid 2605 . . . . . . . . . . 11 (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) = (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋)
119, 10fmptd 6273 . . . . . . . . . 10 ((𝜑𝑗𝑆) → (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋):{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}⟶𝐵)
123adantr 479 . . . . . . . . . . . 12 ((𝜑𝑗𝑆) → 𝐼𝑉)
13 ssrab2 3645 . . . . . . . . . . . . . 14 {𝑦𝐷𝑦𝑟𝐹} ⊆ 𝐷
142, 13eqsstri 3593 . . . . . . . . . . . . 13 𝑆𝐷
154adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑗𝑆) → 𝐹𝐷)
16 simpr 475 . . . . . . . . . . . . . 14 ((𝜑𝑗𝑆) → 𝑗𝑆)
171, 2psrbagconcl 19136 . . . . . . . . . . . . . 14 ((𝐼𝑉𝐹𝐷𝑗𝑆) → (𝐹𝑓𝑗) ∈ 𝑆)
1812, 15, 16, 17syl3anc 1317 . . . . . . . . . . . . 13 ((𝜑𝑗𝑆) → (𝐹𝑓𝑗) ∈ 𝑆)
1914, 18sseldi 3561 . . . . . . . . . . . 12 ((𝜑𝑗𝑆) → (𝐹𝑓𝑗) ∈ 𝐷)
20 eqid 2605 . . . . . . . . . . . . 13 {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} = {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}
211, 20psrbagconf1o 19137 . . . . . . . . . . . 12 ((𝐼𝑉 ∧ (𝐹𝑓𝑗) ∈ 𝐷) → (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑗) ∘𝑓𝑚)):{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}–1-1-onto→{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})
2212, 19, 21syl2anc 690 . . . . . . . . . . 11 ((𝜑𝑗𝑆) → (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑗) ∘𝑓𝑚)):{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}–1-1-onto→{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})
23 f1of 6031 . . . . . . . . . . 11 ((𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑗) ∘𝑓𝑚)):{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}–1-1-onto→{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} → (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑗) ∘𝑓𝑚)):{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}⟶{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})
2422, 23syl 17 . . . . . . . . . 10 ((𝜑𝑗𝑆) → (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑗) ∘𝑓𝑚)):{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}⟶{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})
25 fco 5953 . . . . . . . . . 10 (((𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋):{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}⟶𝐵 ∧ (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑗) ∘𝑓𝑚)):{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}⟶{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → ((𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑗) ∘𝑓𝑚))):{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}⟶𝐵)
2611, 24, 25syl2anc 690 . . . . . . . . 9 ((𝜑𝑗𝑆) → ((𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑗) ∘𝑓𝑚))):{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}⟶𝐵)
2712adantr 479 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → 𝐼𝑉)
2815adantr 479 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → 𝐹𝐷)
291psrbagf 19128 . . . . . . . . . . . . . . . . 17 ((𝐼𝑉𝐹𝐷) → 𝐹:𝐼⟶ℕ0)
3027, 28, 29syl2anc 690 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → 𝐹:𝐼⟶ℕ0)
3130ffvelrnda 6248 . . . . . . . . . . . . . . 15 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) ∧ 𝑧𝐼) → (𝐹𝑧) ∈ ℕ0)
3216adantr 479 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → 𝑗𝑆)
3314, 32sseldi 3561 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → 𝑗𝐷)
341psrbagf 19128 . . . . . . . . . . . . . . . . 17 ((𝐼𝑉𝑗𝐷) → 𝑗:𝐼⟶ℕ0)
3527, 33, 34syl2anc 690 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → 𝑗:𝐼⟶ℕ0)
3635ffvelrnda 6248 . . . . . . . . . . . . . . 15 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) ∧ 𝑧𝐼) → (𝑗𝑧) ∈ ℕ0)
37 ssrab2 3645 . . . . . . . . . . . . . . . . . 18 {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ⊆ 𝐷
38 simpr 475 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})
3937, 38sseldi 3561 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → 𝑚𝐷)
401psrbagf 19128 . . . . . . . . . . . . . . . . 17 ((𝐼𝑉𝑚𝐷) → 𝑚:𝐼⟶ℕ0)
4127, 39, 40syl2anc 690 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → 𝑚:𝐼⟶ℕ0)
4241ffvelrnda 6248 . . . . . . . . . . . . . . 15 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) ∧ 𝑧𝐼) → (𝑚𝑧) ∈ ℕ0)
43 nn0cn 11145 . . . . . . . . . . . . . . . 16 ((𝐹𝑧) ∈ ℕ0 → (𝐹𝑧) ∈ ℂ)
44 nn0cn 11145 . . . . . . . . . . . . . . . 16 ((𝑗𝑧) ∈ ℕ0 → (𝑗𝑧) ∈ ℂ)
45 nn0cn 11145 . . . . . . . . . . . . . . . 16 ((𝑚𝑧) ∈ ℕ0 → (𝑚𝑧) ∈ ℂ)
46 sub32 10162 . . . . . . . . . . . . . . . 16 (((𝐹𝑧) ∈ ℂ ∧ (𝑗𝑧) ∈ ℂ ∧ (𝑚𝑧) ∈ ℂ) → (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧)) = (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧)))
4743, 44, 45, 46syl3an 1359 . . . . . . . . . . . . . . 15 (((𝐹𝑧) ∈ ℕ0 ∧ (𝑗𝑧) ∈ ℕ0 ∧ (𝑚𝑧) ∈ ℕ0) → (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧)) = (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧)))
4831, 36, 42, 47syl3anc 1317 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) ∧ 𝑧𝐼) → (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧)) = (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧)))
4948mpteq2dva 4662 . . . . . . . . . . . . 13 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → (𝑧𝐼 ↦ (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧))) = (𝑧𝐼 ↦ (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧))))
50 ovex 6551 . . . . . . . . . . . . . . 15 ((𝐹𝑧) − (𝑗𝑧)) ∈ V
5150a1i 11 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) ∧ 𝑧𝐼) → ((𝐹𝑧) − (𝑗𝑧)) ∈ V)
5230feqmptd 6140 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → 𝐹 = (𝑧𝐼 ↦ (𝐹𝑧)))
5335feqmptd 6140 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → 𝑗 = (𝑧𝐼 ↦ (𝑗𝑧)))
5427, 31, 36, 52, 53offval2 6785 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → (𝐹𝑓𝑗) = (𝑧𝐼 ↦ ((𝐹𝑧) − (𝑗𝑧))))
5541feqmptd 6140 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → 𝑚 = (𝑧𝐼 ↦ (𝑚𝑧)))
5627, 51, 42, 54, 55offval2 6785 . . . . . . . . . . . . 13 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → ((𝐹𝑓𝑗) ∘𝑓𝑚) = (𝑧𝐼 ↦ (((𝐹𝑧) − (𝑗𝑧)) − (𝑚𝑧))))
57 ovex 6551 . . . . . . . . . . . . . . 15 ((𝐹𝑧) − (𝑚𝑧)) ∈ V
5857a1i 11 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) ∧ 𝑧𝐼) → ((𝐹𝑧) − (𝑚𝑧)) ∈ V)
5927, 31, 42, 52, 55offval2 6785 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → (𝐹𝑓𝑚) = (𝑧𝐼 ↦ ((𝐹𝑧) − (𝑚𝑧))))
6027, 58, 36, 59, 53offval2 6785 . . . . . . . . . . . . 13 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → ((𝐹𝑓𝑚) ∘𝑓𝑗) = (𝑧𝐼 ↦ (((𝐹𝑧) − (𝑚𝑧)) − (𝑗𝑧))))
6149, 56, 603eqtr4d 2649 . . . . . . . . . . . 12 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → ((𝐹𝑓𝑗) ∘𝑓𝑚) = ((𝐹𝑓𝑚) ∘𝑓𝑗))
6219adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → (𝐹𝑓𝑗) ∈ 𝐷)
631, 20psrbagconcl 19136 . . . . . . . . . . . . 13 ((𝐼𝑉 ∧ (𝐹𝑓𝑗) ∈ 𝐷𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → ((𝐹𝑓𝑗) ∘𝑓𝑚) ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})
6427, 62, 38, 63syl3anc 1317 . . . . . . . . . . . 12 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → ((𝐹𝑓𝑗) ∘𝑓𝑚) ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})
6561, 64eqeltrrd 2684 . . . . . . . . . . 11 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → ((𝐹𝑓𝑚) ∘𝑓𝑗) ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})
6661mpteq2dva 4662 . . . . . . . . . . 11 ((𝜑𝑗𝑆) → (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑗) ∘𝑓𝑚)) = (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗)))
67 nfcv 2746 . . . . . . . . . . . . 13 𝑛𝑋
68 nfcsb1v 3510 . . . . . . . . . . . . 13 𝑘𝑛 / 𝑘𝑋
69 csbeq1a 3503 . . . . . . . . . . . . 13 (𝑘 = 𝑛𝑋 = 𝑛 / 𝑘𝑋)
7067, 68, 69cbvmpt 4667 . . . . . . . . . . . 12 (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑛 / 𝑘𝑋)
7170a1i 11 . . . . . . . . . . 11 ((𝜑𝑗𝑆) → (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑛 / 𝑘𝑋))
72 csbeq1 3497 . . . . . . . . . . 11 (𝑛 = ((𝐹𝑓𝑚) ∘𝑓𝑗) → 𝑛 / 𝑘𝑋 = ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)
7365, 66, 71, 72fmptco 6284 . . . . . . . . . 10 ((𝜑𝑗𝑆) → ((𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑗) ∘𝑓𝑚))) = (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋))
7473feq1d 5925 . . . . . . . . 9 ((𝜑𝑗𝑆) → (((𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑗) ∘𝑓𝑚))):{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}⟶𝐵 ↔ (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋):{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}⟶𝐵))
7526, 74mpbid 220 . . . . . . . 8 ((𝜑𝑗𝑆) → (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋):{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}⟶𝐵)
76 eqid 2605 . . . . . . . . 9 (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋) = (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)
7776fmpt 6270 . . . . . . . 8 (∀𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋𝐵 ↔ (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋):{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}⟶𝐵)
7875, 77sylibr 222 . . . . . . 7 ((𝜑𝑗𝑆) → ∀𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋𝐵)
7978r19.21bi 2911 . . . . . 6 (((𝜑𝑗𝑆) ∧ 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) → ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋𝐵)
8079anasss 676 . . . . 5 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})) → ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋𝐵)
817, 80syldan 485 . . . 4 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)})) → ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋𝐵)
821, 2, 3, 4, 5, 6, 81gsumbagdiag 19139 . . 3 (𝜑 → (𝐺 Σg (𝑚𝑆, 𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)) = (𝐺 Σg (𝑗𝑆, 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)))
83 eqid 2605 . . . 4 (0g𝐺) = (0g𝐺)
841psrbaglefi 19135 . . . . . 6 ((𝐼𝑉𝐹𝐷) → {𝑦𝐷𝑦𝑟𝐹} ∈ Fin)
853, 4, 84syl2anc 690 . . . . 5 (𝜑 → {𝑦𝐷𝑦𝑟𝐹} ∈ Fin)
862, 85syl5eqel 2687 . . . 4 (𝜑𝑆 ∈ Fin)
873adantr 479 . . . . 5 ((𝜑𝑚𝑆) → 𝐼𝑉)
884adantr 479 . . . . . . 7 ((𝜑𝑚𝑆) → 𝐹𝐷)
89 simpr 475 . . . . . . 7 ((𝜑𝑚𝑆) → 𝑚𝑆)
901, 2psrbagconcl 19136 . . . . . . 7 ((𝐼𝑉𝐹𝐷𝑚𝑆) → (𝐹𝑓𝑚) ∈ 𝑆)
9187, 88, 89, 90syl3anc 1317 . . . . . 6 ((𝜑𝑚𝑆) → (𝐹𝑓𝑚) ∈ 𝑆)
9214, 91sseldi 3561 . . . . 5 ((𝜑𝑚𝑆) → (𝐹𝑓𝑚) ∈ 𝐷)
931psrbaglefi 19135 . . . . 5 ((𝐼𝑉 ∧ (𝐹𝑓𝑚) ∈ 𝐷) → {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ∈ Fin)
9487, 92, 93syl2anc 690 . . . 4 ((𝜑𝑚𝑆) → {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ∈ Fin)
95 xpfi 8089 . . . . 5 ((𝑆 ∈ Fin ∧ 𝑆 ∈ Fin) → (𝑆 × 𝑆) ∈ Fin)
9686, 86, 95syl2anc 690 . . . 4 (𝜑 → (𝑆 × 𝑆) ∈ Fin)
97 simprl 789 . . . . . . 7 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)})) → 𝑚𝑆)
987simpld 473 . . . . . . 7 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)})) → 𝑗𝑆)
99 brxp 5057 . . . . . . 7 (𝑚(𝑆 × 𝑆)𝑗 ↔ (𝑚𝑆𝑗𝑆))
10097, 98, 99sylanbrc 694 . . . . . 6 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)})) → 𝑚(𝑆 × 𝑆)𝑗)
101100pm2.24d 145 . . . . 5 ((𝜑 ∧ (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)})) → (¬ 𝑚(𝑆 × 𝑆)𝑗((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋 = (0g𝐺)))
102101impr 646 . . . 4 ((𝜑 ∧ ((𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)}) ∧ ¬ 𝑚(𝑆 × 𝑆)𝑗)) → ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋 = (0g𝐺))
1035, 83, 6, 86, 94, 81, 96, 102gsum2d2 18138 . . 3 (𝜑 → (𝐺 Σg (𝑚𝑆, 𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)) = (𝐺 Σg (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)))))
1041psrbaglefi 19135 . . . . 5 ((𝐼𝑉 ∧ (𝐹𝑓𝑗) ∈ 𝐷) → {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ∈ Fin)
10512, 19, 104syl2anc 690 . . . 4 ((𝜑𝑗𝑆) → {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ∈ Fin)
106 simprl 789 . . . . . . 7 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})) → 𝑗𝑆)
1071, 2, 3, 4gsumbagdiaglem 19138 . . . . . . . 8 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})) → (𝑚𝑆𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)}))
108107simpld 473 . . . . . . 7 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})) → 𝑚𝑆)
109 brxp 5057 . . . . . . 7 (𝑗(𝑆 × 𝑆)𝑚 ↔ (𝑗𝑆𝑚𝑆))
110106, 108, 109sylanbrc 694 . . . . . 6 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})) → 𝑗(𝑆 × 𝑆)𝑚)
111110pm2.24d 145 . . . . 5 ((𝜑 ∧ (𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})) → (¬ 𝑗(𝑆 × 𝑆)𝑚((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋 = (0g𝐺)))
112111impr 646 . . . 4 ((𝜑 ∧ ((𝑗𝑆𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}) ∧ ¬ 𝑗(𝑆 × 𝑆)𝑚)) → ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋 = (0g𝐺))
1135, 83, 6, 86, 105, 80, 96, 112gsum2d2 18138 . . 3 (𝜑 → (𝐺 Σg (𝑗𝑆, 𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)))))
11482, 103, 1133eqtr3d 2647 . 2 (𝜑 → (𝐺 Σg (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)))) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)))))
1156adantr 479 . . . . . . . 8 ((𝜑𝑚𝑆) → 𝐺 ∈ CMnd)
11681anassrs 677 . . . . . . . . 9 (((𝜑𝑚𝑆) ∧ 𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)}) → ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋𝐵)
117 eqid 2605 . . . . . . . . 9 (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋) = (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)
118116, 117fmptd 6273 . . . . . . . 8 ((𝜑𝑚𝑆) → (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋):{𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)}⟶𝐵)
119 ovex 6551 . . . . . . . . . . . 12 (ℕ0𝑚 𝐼) ∈ V
1201, 119rabex2 4733 . . . . . . . . . . 11 𝐷 ∈ V
121120a1i 11 . . . . . . . . . 10 ((𝜑𝑚𝑆) → 𝐷 ∈ V)
122 rabexg 4730 . . . . . . . . . 10 (𝐷 ∈ V → {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ∈ V)
123 mptexg 6363 . . . . . . . . . 10 ({𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ∈ V → (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋) ∈ V)
124121, 122, 1233syl 18 . . . . . . . . 9 ((𝜑𝑚𝑆) → (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋) ∈ V)
125 funmpt 5822 . . . . . . . . . 10 Fun (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)
126125a1i 11 . . . . . . . . 9 ((𝜑𝑚𝑆) → Fun (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋))
127 fvex 6094 . . . . . . . . . 10 (0g𝐺) ∈ V
128127a1i 11 . . . . . . . . 9 ((𝜑𝑚𝑆) → (0g𝐺) ∈ V)
129 suppssdm 7168 . . . . . . . . . . 11 ((𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋) supp (0g𝐺)) ⊆ dom (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)
130117dmmptss 5530 . . . . . . . . . . 11 dom (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋) ⊆ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)}
131129, 130sstri 3572 . . . . . . . . . 10 ((𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)}
132131a1i 11 . . . . . . . . 9 ((𝜑𝑚𝑆) → ((𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)})
133 suppssfifsupp 8146 . . . . . . . . 9 ((((𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋) ∈ V ∧ Fun (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋) ∧ (0g𝐺) ∈ V) ∧ ({𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ∈ Fin ∧ ((𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)})) → (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋) finSupp (0g𝐺))
134124, 126, 128, 94, 132, 133syl32anc 1325 . . . . . . . 8 ((𝜑𝑚𝑆) → (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋) finSupp (0g𝐺))
1355, 83, 115, 94, 118, 134gsumcl 18081 . . . . . . 7 ((𝜑𝑚𝑆) → (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)) ∈ 𝐵)
136 eqid 2605 . . . . . . 7 (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋))) = (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)))
137135, 136fmptd 6273 . . . . . 6 (𝜑 → (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋))):𝑆𝐵)
1381, 2psrbagconf1o 19137 . . . . . . . 8 ((𝐼𝑉𝐹𝐷) → (𝑚𝑆 ↦ (𝐹𝑓𝑚)):𝑆1-1-onto𝑆)
1393, 4, 138syl2anc 690 . . . . . . 7 (𝜑 → (𝑚𝑆 ↦ (𝐹𝑓𝑚)):𝑆1-1-onto𝑆)
140 f1ocnv 6043 . . . . . . 7 ((𝑚𝑆 ↦ (𝐹𝑓𝑚)):𝑆1-1-onto𝑆(𝑚𝑆 ↦ (𝐹𝑓𝑚)):𝑆1-1-onto𝑆)
141 f1of 6031 . . . . . . 7 ((𝑚𝑆 ↦ (𝐹𝑓𝑚)):𝑆1-1-onto𝑆(𝑚𝑆 ↦ (𝐹𝑓𝑚)):𝑆𝑆)
142139, 140, 1413syl 18 . . . . . 6 (𝜑(𝑚𝑆 ↦ (𝐹𝑓𝑚)):𝑆𝑆)
143 fco 5953 . . . . . 6 (((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋))):𝑆𝐵(𝑚𝑆 ↦ (𝐹𝑓𝑚)):𝑆𝑆) → ((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚))):𝑆𝐵)
144137, 142, 143syl2anc 690 . . . . 5 (𝜑 → ((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚))):𝑆𝐵)
145 coass 5553 . . . . . . . 8 (((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚))) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚))) = ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ∘ ((𝑚𝑆 ↦ (𝐹𝑓𝑚)) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚))))
146 f1ococnv2 6057 . . . . . . . . . 10 ((𝑚𝑆 ↦ (𝐹𝑓𝑚)):𝑆1-1-onto𝑆 → ((𝑚𝑆 ↦ (𝐹𝑓𝑚)) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚))) = ( I ↾ 𝑆))
147139, 146syl 17 . . . . . . . . 9 (𝜑 → ((𝑚𝑆 ↦ (𝐹𝑓𝑚)) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚))) = ( I ↾ 𝑆))
148147coeq2d 5190 . . . . . . . 8 (𝜑 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ∘ ((𝑚𝑆 ↦ (𝐹𝑓𝑚)) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚)))) = ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)))
149145, 148syl5eq 2651 . . . . . . 7 (𝜑 → (((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚))) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚))) = ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)))
150 eqidd 2606 . . . . . . . . 9 (𝜑 → (𝑚𝑆 ↦ (𝐹𝑓𝑚)) = (𝑚𝑆 ↦ (𝐹𝑓𝑚)))
151 eqidd 2606 . . . . . . . . 9 (𝜑 → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))))
152 breq2 4577 . . . . . . . . . . . 12 (𝑛 = (𝐹𝑓𝑚) → (𝑥𝑟𝑛𝑥𝑟 ≤ (𝐹𝑓𝑚)))
153152rabbidv 3159 . . . . . . . . . . 11 (𝑛 = (𝐹𝑓𝑚) → {𝑥𝐷𝑥𝑟𝑛} = {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)})
154 ovex 6551 . . . . . . . . . . . . 13 (𝑛𝑓𝑗) ∈ V
155 psrass1lem.y . . . . . . . . . . . . 13 (𝑘 = (𝑛𝑓𝑗) → 𝑋 = 𝑌)
156154, 155csbie 3520 . . . . . . . . . . . 12 (𝑛𝑓𝑗) / 𝑘𝑋 = 𝑌
157 oveq1 6530 . . . . . . . . . . . . 13 (𝑛 = (𝐹𝑓𝑚) → (𝑛𝑓𝑗) = ((𝐹𝑓𝑚) ∘𝑓𝑗))
158157csbeq1d 3501 . . . . . . . . . . . 12 (𝑛 = (𝐹𝑓𝑚) → (𝑛𝑓𝑗) / 𝑘𝑋 = ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)
159156, 158syl5eqr 2653 . . . . . . . . . . 11 (𝑛 = (𝐹𝑓𝑚) → 𝑌 = ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)
160153, 159mpteq12dv 4653 . . . . . . . . . 10 (𝑛 = (𝐹𝑓𝑚) → (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌) = (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋))
161160oveq2d 6539 . . . . . . . . 9 (𝑛 = (𝐹𝑓𝑚) → (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌)) = (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)))
16291, 150, 151, 161fmptco 6284 . . . . . . . 8 (𝜑 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚))) = (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋))))
163162coeq1d 5189 . . . . . . 7 (𝜑 → (((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚))) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚))) = ((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚))))
164 coires1 5552 . . . . . . . . 9 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ↾ 𝑆)
165 ssid 3582 . . . . . . . . . 10 𝑆𝑆
166 resmpt 5352 . . . . . . . . . 10 (𝑆𝑆 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))))
167165, 166ax-mp 5 . . . . . . . . 9 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌)))
168164, 167eqtri 2627 . . . . . . . 8 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌)))
169168a1i 11 . . . . . . 7 (𝜑 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))))
170149, 163, 1693eqtr3d 2647 . . . . . 6 (𝜑 → ((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚))) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))))
171170feq1d 5925 . . . . 5 (𝜑 → (((𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋))) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚))):𝑆𝐵 ↔ (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))):𝑆𝐵))
172144, 171mpbid 220 . . . 4 (𝜑 → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))):𝑆𝐵)
173 rabexg 4730 . . . . . . . 8 (𝐷 ∈ V → {𝑦𝐷𝑦𝑟𝐹} ∈ V)
174120, 173mp1i 13 . . . . . . 7 (𝜑 → {𝑦𝐷𝑦𝑟𝐹} ∈ V)
1752, 174syl5eqel 2687 . . . . . 6 (𝜑𝑆 ∈ V)
176 mptexg 6363 . . . . . 6 (𝑆 ∈ V → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ∈ V)
177175, 176syl 17 . . . . 5 (𝜑 → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ∈ V)
178 funmpt 5822 . . . . . 6 Fun (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌)))
179178a1i 11 . . . . 5 (𝜑 → Fun (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))))
180127a1i 11 . . . . 5 (𝜑 → (0g𝐺) ∈ V)
181 suppssdm 7168 . . . . . . 7 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) supp (0g𝐺)) ⊆ dom (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌)))
182 eqid 2605 . . . . . . . 8 (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) = (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌)))
183182dmmptss 5530 . . . . . . 7 dom (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ⊆ 𝑆
184181, 183sstri 3572 . . . . . 6 ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) supp (0g𝐺)) ⊆ 𝑆
185184a1i 11 . . . . 5 (𝜑 → ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) supp (0g𝐺)) ⊆ 𝑆)
186 suppssfifsupp 8146 . . . . 5 ((((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ∈ V ∧ Fun (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ∧ (0g𝐺) ∈ V) ∧ (𝑆 ∈ Fin ∧ ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) supp (0g𝐺)) ⊆ 𝑆)) → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) finSupp (0g𝐺))
187177, 179, 180, 86, 185, 186syl32anc 1325 . . . 4 (𝜑 → (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) finSupp (0g𝐺))
1885, 83, 6, 86, 172, 187, 139gsumf1o 18082 . . 3 (𝜑 → (𝐺 Σg (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌)))) = (𝐺 Σg ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚)))))
189162oveq2d 6539 . . 3 (𝜑 → (𝐺 Σg ((𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌))) ∘ (𝑚𝑆 ↦ (𝐹𝑓𝑚)))) = (𝐺 Σg (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)))))
190188, 189eqtrd 2639 . 2 (𝜑 → (𝐺 Σg (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑚𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑚)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)))))
1916adantr 479 . . . . . 6 ((𝜑𝑗𝑆) → 𝐺 ∈ CMnd)
192120a1i 11 . . . . . . . 8 ((𝜑𝑗𝑆) → 𝐷 ∈ V)
193 rabexg 4730 . . . . . . . 8 (𝐷 ∈ V → {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ∈ V)
194 mptexg 6363 . . . . . . . 8 ({𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ∈ V → (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) ∈ V)
195192, 193, 1943syl 18 . . . . . . 7 ((𝜑𝑗𝑆) → (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) ∈ V)
196 funmpt 5822 . . . . . . . 8 Fun (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋)
197196a1i 11 . . . . . . 7 ((𝜑𝑗𝑆) → Fun (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋))
198127a1i 11 . . . . . . 7 ((𝜑𝑗𝑆) → (0g𝐺) ∈ V)
199 suppssdm 7168 . . . . . . . . 9 ((𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) supp (0g𝐺)) ⊆ dom (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋)
20010dmmptss 5530 . . . . . . . . 9 dom (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) ⊆ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}
201199, 200sstri 3572 . . . . . . . 8 ((𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)}
202201a1i 11 . . . . . . 7 ((𝜑𝑗𝑆) → ((𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})
203 suppssfifsupp 8146 . . . . . . 7 ((((𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) ∈ V ∧ Fun (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) ∧ (0g𝐺) ∈ V) ∧ ({𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ∈ Fin ∧ ((𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) supp (0g𝐺)) ⊆ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)})) → (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) finSupp (0g𝐺))
204195, 197, 198, 105, 202, 203syl32anc 1325 . . . . . 6 ((𝜑𝑗𝑆) → (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) finSupp (0g𝐺))
2055, 83, 191, 105, 11, 204, 22gsumf1o 18082 . . . . 5 ((𝜑𝑗𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋)) = (𝐺 Σg ((𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑗) ∘𝑓𝑚)))))
20673oveq2d 6539 . . . . 5 ((𝜑𝑗𝑆) → (𝐺 Σg ((𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑗) ∘𝑓𝑚)))) = (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)))
207205, 206eqtrd 2639 . . . 4 ((𝜑𝑗𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋)) = (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)))
208207mpteq2dva 4662 . . 3 (𝜑 → (𝑗𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋))) = (𝑗𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋))))
209208oveq2d 6539 . 2 (𝜑 → (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋)))) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ ((𝐹𝑓𝑚) ∘𝑓𝑗) / 𝑘𝑋)))))
210114, 190, 2093eqtr4d 2649 1 (𝜑 → (𝐺 Σg (𝑛𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥𝐷𝑥𝑟𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑗𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥𝐷𝑥𝑟 ≤ (𝐹𝑓𝑗)} ↦ 𝑋)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382   = wceq 1474  wcel 1975  wral 2891  {crab 2895  Vcvv 3168  csb 3494  wss 3535   class class class wbr 4573  cmpt 4633   I cid 4934   × cxp 5022  ccnv 5023  dom cdm 5024  cres 5026  cima 5027  ccom 5028  Fun wfun 5780  wf 5782  1-1-ontowf1o 5785  cfv 5786  (class class class)co 6523  cmpt2 6525  𝑓 cof 6766  𝑟 cofr 6767   supp csupp 7155  𝑚 cmap 7717  Fincfn 7814   finSupp cfsupp 8131  cc 9786  cle 9927  cmin 10113  cn 10863  0cn0 11135  Basecbs 15637  0gc0g 15865   Σg cgsu 15866  CMndccmn 17958
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-rep 4689  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-inf2 8394  ax-cnex 9844  ax-resscn 9845  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-addrcl 9849  ax-mulcl 9850  ax-mulrcl 9851  ax-mulcom 9852  ax-addass 9853  ax-mulass 9854  ax-distr 9855  ax-i2m1 9856  ax-1ne0 9857  ax-1rid 9858  ax-rnegex 9859  ax-rrecex 9860  ax-cnre 9861  ax-pre-lttri 9862  ax-pre-lttrn 9863  ax-pre-ltadd 9864  ax-pre-mulgt0 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-nel 2778  df-ral 2896  df-rex 2897  df-reu 2898  df-rmo 2899  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-int 4401  df-iun 4447  df-iin 4448  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-se 4984  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-isom 5795  df-riota 6485  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-of 6768  df-ofr 6769  df-om 6931  df-1st 7032  df-2nd 7033  df-supp 7156  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-1o 7420  df-2o 7421  df-oadd 7424  df-er 7602  df-map 7719  df-pm 7720  df-ixp 7768  df-en 7815  df-dom 7816  df-sdom 7817  df-fin 7818  df-fsupp 8132  df-oi 8271  df-card 8621  df-pnf 9928  df-mnf 9929  df-xr 9930  df-ltxr 9931  df-le 9932  df-sub 10115  df-neg 10116  df-nn 10864  df-2 10922  df-n0 11136  df-z 11207  df-uz 11516  df-fz 12149  df-fzo 12286  df-seq 12615  df-hash 12931  df-ndx 15640  df-slot 15641  df-base 15642  df-sets 15643  df-ress 15644  df-plusg 15723  df-0g 15867  df-gsum 15868  df-mre 16011  df-mrc 16012  df-acs 16014  df-mgm 17007  df-sgrp 17049  df-mnd 17060  df-submnd 17101  df-mulg 17306  df-cntz 17515  df-cmn 17960
This theorem is referenced by:  psrass1  19168
  Copyright terms: Public domain W3C validator