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

Theorem tsmsadd 22743
Description: The sum of two infinite group sums. (Contributed by Mario Carneiro, 19-Sep-2015.) (Proof shortened by AV, 24-Jul-2019.)
Hypotheses
Ref Expression
tsmsadd.b 𝐵 = (Base‘𝐺)
tsmsadd.p + = (+g𝐺)
tsmsadd.1 (𝜑𝐺 ∈ CMnd)
tsmsadd.2 (𝜑𝐺 ∈ TopMnd)
tsmsadd.a (𝜑𝐴𝑉)
tsmsadd.f (𝜑𝐹:𝐴𝐵)
tsmsadd.h (𝜑𝐻:𝐴𝐵)
tsmsadd.x (𝜑𝑋 ∈ (𝐺 tsums 𝐹))
tsmsadd.y (𝜑𝑌 ∈ (𝐺 tsums 𝐻))
Assertion
Ref Expression
tsmsadd (𝜑 → (𝑋 + 𝑌) ∈ (𝐺 tsums (𝐹f + 𝐻)))

Proof of Theorem tsmsadd
Dummy variables 𝑦 𝑧 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tsmsadd.b . . . . . 6 𝐵 = (Base‘𝐺)
2 tsmsadd.1 . . . . . 6 (𝜑𝐺 ∈ CMnd)
3 tsmsadd.2 . . . . . . 7 (𝜑𝐺 ∈ TopMnd)
4 tmdtps 22672 . . . . . . 7 (𝐺 ∈ TopMnd → 𝐺 ∈ TopSp)
53, 4syl 17 . . . . . 6 (𝜑𝐺 ∈ TopSp)
6 tsmsadd.a . . . . . 6 (𝜑𝐴𝑉)
7 tsmsadd.f . . . . . 6 (𝜑𝐹:𝐴𝐵)
81, 2, 5, 6, 7tsmscl 22731 . . . . 5 (𝜑 → (𝐺 tsums 𝐹) ⊆ 𝐵)
9 tsmsadd.x . . . . 5 (𝜑𝑋 ∈ (𝐺 tsums 𝐹))
108, 9sseldd 3952 . . . 4 (𝜑𝑋𝐵)
11 tsmsadd.h . . . . . 6 (𝜑𝐻:𝐴𝐵)
121, 2, 5, 6, 11tsmscl 22731 . . . . 5 (𝜑 → (𝐺 tsums 𝐻) ⊆ 𝐵)
13 tsmsadd.y . . . . 5 (𝜑𝑌 ∈ (𝐺 tsums 𝐻))
1412, 13sseldd 3952 . . . 4 (𝜑𝑌𝐵)
15 tsmsadd.p . . . . 5 + = (+g𝐺)
16 eqid 2824 . . . . 5 (+𝑓𝐺) = (+𝑓𝐺)
171, 15, 16plusfval 17850 . . . 4 ((𝑋𝐵𝑌𝐵) → (𝑋(+𝑓𝐺)𝑌) = (𝑋 + 𝑌))
1810, 14, 17syl2anc 587 . . 3 (𝜑 → (𝑋(+𝑓𝐺)𝑌) = (𝑋 + 𝑌))
19 eqid 2824 . . . . . 6 (TopOpen‘𝐺) = (TopOpen‘𝐺)
201, 19istps 21530 . . . . 5 (𝐺 ∈ TopSp ↔ (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
215, 20sylib 221 . . . 4 (𝜑 → (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
22 eqid 2824 . . . . . 6 (𝒫 𝐴 ∩ Fin) = (𝒫 𝐴 ∩ Fin)
23 eqid 2824 . . . . . 6 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧}) = (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})
24 eqid 2824 . . . . . 6 ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧}) = ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})
2522, 23, 24, 6tsmsfbas 22724 . . . . 5 (𝜑 → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧}) ∈ (fBas‘(𝒫 𝐴 ∩ Fin)))
26 fgcl 22474 . . . . 5 (ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧}) ∈ (fBas‘(𝒫 𝐴 ∩ Fin)) → ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})) ∈ (Fil‘(𝒫 𝐴 ∩ Fin)))
2725, 26syl 17 . . . 4 (𝜑 → ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})) ∈ (Fil‘(𝒫 𝐴 ∩ Fin)))
281, 22, 2, 6, 7tsmslem1 22725 . . . 4 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹𝑧)) ∈ 𝐵)
291, 22, 2, 6, 11tsmslem1 22725 . . . 4 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐻𝑧)) ∈ 𝐵)
301, 19, 22, 24, 2, 6, 7tsmsval 22727 . . . . 5 (𝜑 → (𝐺 tsums 𝐹) = (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑧)))))
319, 30eleqtrd 2918 . . . 4 (𝜑𝑋 ∈ (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑧)))))
321, 19, 22, 24, 2, 6, 11tsmsval 22727 . . . . 5 (𝜑 → (𝐺 tsums 𝐻) = (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐻𝑧)))))
3313, 32eleqtrd 2918 . . . 4 (𝜑𝑌 ∈ (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐻𝑧)))))
3419, 16tmdcn 22679 . . . . . 6 (𝐺 ∈ TopMnd → (+𝑓𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺)))
353, 34syl 17 . . . . 5 (𝜑 → (+𝑓𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺)))
3610, 14opelxpd 5576 . . . . . 6 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
37 txtopon 22187 . . . . . . . 8 (((TopOpen‘𝐺) ∈ (TopOn‘𝐵) ∧ (TopOpen‘𝐺) ∈ (TopOn‘𝐵)) → ((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) ∈ (TopOn‘(𝐵 × 𝐵)))
3821, 21, 37syl2anc 587 . . . . . . 7 (𝜑 → ((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) ∈ (TopOn‘(𝐵 × 𝐵)))
39 toponuni 21510 . . . . . . 7 (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) ∈ (TopOn‘(𝐵 × 𝐵)) → (𝐵 × 𝐵) = ((TopOpen‘𝐺) ×t (TopOpen‘𝐺)))
4038, 39syl 17 . . . . . 6 (𝜑 → (𝐵 × 𝐵) = ((TopOpen‘𝐺) ×t (TopOpen‘𝐺)))
4136, 40eleqtrd 2918 . . . . 5 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ((TopOpen‘𝐺) ×t (TopOpen‘𝐺)))
42 eqid 2824 . . . . . 6 ((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) = ((TopOpen‘𝐺) ×t (TopOpen‘𝐺))
4342cncnpi 21874 . . . . 5 (((+𝑓𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺)) ∧ ⟨𝑋, 𝑌⟩ ∈ ((TopOpen‘𝐺) ×t (TopOpen‘𝐺))) → (+𝑓𝐺) ∈ ((((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) CnP (TopOpen‘𝐺))‘⟨𝑋, 𝑌⟩))
4435, 41, 43syl2anc 587 . . . 4 (𝜑 → (+𝑓𝐺) ∈ ((((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) CnP (TopOpen‘𝐺))‘⟨𝑋, 𝑌⟩))
4521, 21, 27, 28, 29, 31, 33, 44flfcnp2 22603 . . 3 (𝜑 → (𝑋(+𝑓𝐺)𝑌) ∈ (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((𝐺 Σg (𝐹𝑧))(+𝑓𝐺)(𝐺 Σg (𝐻𝑧))))))
4618, 45eqeltrrd 2917 . 2 (𝜑 → (𝑋 + 𝑌) ∈ (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((𝐺 Σg (𝐹𝑧))(+𝑓𝐺)(𝐺 Σg (𝐻𝑧))))))
47 cmnmnd 18913 . . . . . . 7 (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
482, 47syl 17 . . . . . 6 (𝜑𝐺 ∈ Mnd)
491, 15mndcl 17910 . . . . . . 7 ((𝐺 ∈ Mnd ∧ 𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
50493expb 1117 . . . . . 6 ((𝐺 ∈ Mnd ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
5148, 50sylan 583 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
52 inidm 4178 . . . . 5 (𝐴𝐴) = 𝐴
5351, 7, 11, 6, 6, 52off 7409 . . . 4 (𝜑 → (𝐹f + 𝐻):𝐴𝐵)
541, 19, 22, 24, 2, 6, 53tsmsval 22727 . . 3 (𝜑 → (𝐺 tsums (𝐹f + 𝐻)) = (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg ((𝐹f + 𝐻) ↾ 𝑧)))))
55 eqid 2824 . . . . . . 7 (0g𝐺) = (0g𝐺)
562adantr 484 . . . . . . 7 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd)
57 elinel2 4156 . . . . . . . 8 (𝑧 ∈ (𝒫 𝐴 ∩ Fin) → 𝑧 ∈ Fin)
5857adantl 485 . . . . . . 7 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑧 ∈ Fin)
59 elfpw 8812 . . . . . . . . 9 (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑧𝐴𝑧 ∈ Fin))
6059simplbi 501 . . . . . . . 8 (𝑧 ∈ (𝒫 𝐴 ∩ Fin) → 𝑧𝐴)
61 fssres 6527 . . . . . . . 8 ((𝐹:𝐴𝐵𝑧𝐴) → (𝐹𝑧):𝑧𝐵)
627, 60, 61syl2an 598 . . . . . . 7 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹𝑧):𝑧𝐵)
63 fssres 6527 . . . . . . . 8 ((𝐻:𝐴𝐵𝑧𝐴) → (𝐻𝑧):𝑧𝐵)
6411, 60, 63syl2an 598 . . . . . . 7 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐻𝑧):𝑧𝐵)
65 fvexd 6668 . . . . . . . 8 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (0g𝐺) ∈ V)
6662, 58, 65fdmfifsupp 8829 . . . . . . 7 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹𝑧) finSupp (0g𝐺))
6764, 58, 65fdmfifsupp 8829 . . . . . . 7 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐻𝑧) finSupp (0g𝐺))
681, 55, 15, 56, 58, 62, 64, 66, 67gsumadd 19034 . . . . . 6 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg ((𝐹𝑧) ∘f + (𝐻𝑧))) = ((𝐺 Σg (𝐹𝑧)) + (𝐺 Σg (𝐻𝑧))))
691fvexi 6667 . . . . . . . . . . 11 𝐵 ∈ V
7069a1i 11 . . . . . . . . . 10 (𝜑𝐵 ∈ V)
71 fex2 7623 . . . . . . . . . 10 ((𝐹:𝐴𝐵𝐴𝑉𝐵 ∈ V) → 𝐹 ∈ V)
727, 6, 70, 71syl3anc 1368 . . . . . . . . 9 (𝜑𝐹 ∈ V)
73 fex2 7623 . . . . . . . . . 10 ((𝐻:𝐴𝐵𝐴𝑉𝐵 ∈ V) → 𝐻 ∈ V)
7411, 6, 70, 73syl3anc 1368 . . . . . . . . 9 (𝜑𝐻 ∈ V)
75 offres 7669 . . . . . . . . 9 ((𝐹 ∈ V ∧ 𝐻 ∈ V) → ((𝐹f + 𝐻) ↾ 𝑧) = ((𝐹𝑧) ∘f + (𝐻𝑧)))
7672, 74, 75syl2anc 587 . . . . . . . 8 (𝜑 → ((𝐹f + 𝐻) ↾ 𝑧) = ((𝐹𝑧) ∘f + (𝐻𝑧)))
7776adantr 484 . . . . . . 7 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹f + 𝐻) ↾ 𝑧) = ((𝐹𝑧) ∘f + (𝐻𝑧)))
7877oveq2d 7156 . . . . . 6 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg ((𝐹f + 𝐻) ↾ 𝑧)) = (𝐺 Σg ((𝐹𝑧) ∘f + (𝐻𝑧))))
791, 15, 16plusfval 17850 . . . . . . 7 (((𝐺 Σg (𝐹𝑧)) ∈ 𝐵 ∧ (𝐺 Σg (𝐻𝑧)) ∈ 𝐵) → ((𝐺 Σg (𝐹𝑧))(+𝑓𝐺)(𝐺 Σg (𝐻𝑧))) = ((𝐺 Σg (𝐹𝑧)) + (𝐺 Σg (𝐻𝑧))))
8028, 29, 79syl2anc 587 . . . . . 6 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐺 Σg (𝐹𝑧))(+𝑓𝐺)(𝐺 Σg (𝐻𝑧))) = ((𝐺 Σg (𝐹𝑧)) + (𝐺 Σg (𝐻𝑧))))
8168, 78, 803eqtr4d 2869 . . . . 5 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg ((𝐹f + 𝐻) ↾ 𝑧)) = ((𝐺 Σg (𝐹𝑧))(+𝑓𝐺)(𝐺 Σg (𝐻𝑧))))
8281mpteq2dva 5144 . . . 4 (𝜑 → (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg ((𝐹f + 𝐻) ↾ 𝑧))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((𝐺 Σg (𝐹𝑧))(+𝑓𝐺)(𝐺 Σg (𝐻𝑧)))))
8382fveq2d 6657 . . 3 (𝜑 → (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg ((𝐹f + 𝐻) ↾ 𝑧)))) = (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((𝐺 Σg (𝐹𝑧))(+𝑓𝐺)(𝐺 Σg (𝐻𝑧))))))
8454, 83eqtrd 2859 . 2 (𝜑 → (𝐺 tsums (𝐹f + 𝐻)) = (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((𝐺 Σg (𝐹𝑧))(+𝑓𝐺)(𝐺 Σg (𝐻𝑧))))))
8546, 84eleqtrrd 2919 1 (𝜑 → (𝑋 + 𝑌) ∈ (𝐺 tsums (𝐹f + 𝐻)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2115  {crab 3136  Vcvv 3479  cin 3917  wss 3918  𝒫 cpw 4520  cop 4554   cuni 4821  cmpt 5129   × cxp 5536  ran crn 5539  cres 5540  wf 6334  cfv 6338  (class class class)co 7140  f cof 7392  Fincfn 8494  Basecbs 16474  +gcplusg 16556  TopOpenctopn 16686  0gc0g 16704   Σg cgsu 16705  +𝑓cplusf 17840  Mndcmnd 17902  CMndccmn 18897  fBascfbas 20521  filGencfg 20522  TopOnctopon 21506  TopSpctps 21528   Cn ccn 21820   CnP ccnp 21821   ×t ctx 22156  Filcfil 22441   fLimf cflf 22531  TopMndctmd 22666   tsums ctsu 22722
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5173  ax-sep 5186  ax-nul 5193  ax-pow 5249  ax-pr 5313  ax-un 7446  ax-cnex 10580  ax-resscn 10581  ax-1cn 10582  ax-icn 10583  ax-addcl 10584  ax-addrcl 10585  ax-mulcl 10586  ax-mulrcl 10587  ax-mulcom 10588  ax-addass 10589  ax-mulass 10590  ax-distr 10591  ax-i2m1 10592  ax-1ne0 10593  ax-1rid 10594  ax-rnegex 10595  ax-rrecex 10596  ax-cnre 10597  ax-pre-lttri 10598  ax-pre-lttrn 10599  ax-pre-ltadd 10600  ax-pre-mulgt0 10601
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-nel 3118  df-ral 3137  df-rex 3138  df-reu 3139  df-rmo 3140  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-pss 3937  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-tp 4553  df-op 4555  df-uni 4822  df-int 4860  df-iun 4904  df-br 5050  df-opab 5112  df-mpt 5130  df-tr 5156  df-id 5443  df-eprel 5448  df-po 5457  df-so 5458  df-fr 5497  df-se 5498  df-we 5499  df-xp 5544  df-rel 5545  df-cnv 5546  df-co 5547  df-dm 5548  df-rn 5549  df-res 5550  df-ima 5551  df-pred 6131  df-ord 6177  df-on 6178  df-lim 6179  df-suc 6180  df-iota 6297  df-fun 6340  df-fn 6341  df-f 6342  df-f1 6343  df-fo 6344  df-f1o 6345  df-fv 6346  df-isom 6347  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-of 7394  df-om 7566  df-1st 7674  df-2nd 7675  df-supp 7816  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-1o 8087  df-oadd 8091  df-er 8274  df-map 8393  df-en 8495  df-dom 8496  df-sdom 8497  df-fin 8498  df-fsupp 8820  df-oi 8960  df-card 9354  df-pnf 10664  df-mnf 10665  df-xr 10666  df-ltxr 10667  df-le 10668  df-sub 10859  df-neg 10860  df-nn 11626  df-2 11688  df-n0 11886  df-z 11970  df-uz 12232  df-fz 12886  df-fzo 13029  df-seq 13365  df-hash 13687  df-ndx 16477  df-slot 16478  df-base 16480  df-sets 16481  df-ress 16482  df-plusg 16569  df-0g 16706  df-gsum 16707  df-topgen 16708  df-plusf 17842  df-mgm 17843  df-sgrp 17892  df-mnd 17903  df-submnd 17948  df-cntz 18438  df-cmn 18899  df-fbas 20530  df-fg 20531  df-top 21490  df-topon 21507  df-topsp 21529  df-bases 21542  df-ntr 21616  df-nei 21694  df-cn 21823  df-cnp 21824  df-tx 22158  df-fil 22442  df-fm 22534  df-flim 22535  df-flf 22536  df-tmd 22668  df-tsms 22723
This theorem is referenced by:  tsmssub  22745  tsmssplit  22748  esumadd  31336  esumaddf  31340
  Copyright terms: Public domain W3C validator