Metamath Proof Explorer


Theorem tsmscls

Description: One half of tgptsmscls , true in any commutative monoid topological space. (Contributed by Mario Carneiro, 21-Sep-2015)

Ref Expression
Hypotheses tsmscls.b B=BaseG
tsmscls.j J=TopOpenG
tsmscls.1 φGCMnd
tsmscls.2 φGTopSp
tsmscls.a φAV
tsmscls.f φF:AB
tsmscls.x φXGtsumsF
Assertion tsmscls φclsJXGtsumsF

Proof

Step Hyp Ref Expression
1 tsmscls.b B=BaseG
2 tsmscls.j J=TopOpenG
3 tsmscls.1 φGCMnd
4 tsmscls.2 φGTopSp
5 tsmscls.a φAV
6 tsmscls.f φF:AB
7 tsmscls.x φXGtsumsF
8 eqid 𝒫AFin=𝒫AFin
9 eqid ranx𝒫AFiny𝒫AFin|xy=ranx𝒫AFiny𝒫AFin|xy
10 1 2 8 9 4 5 6 tsmsval φGtsumsF=JfLimf𝒫AFinfilGenranx𝒫AFiny𝒫AFin|xyy𝒫AFinGFy
11 1 2 istps GTopSpJTopOnB
12 4 11 sylib φJTopOnB
13 eqid x𝒫AFiny𝒫AFin|xy=x𝒫AFiny𝒫AFin|xy
14 8 13 9 5 tsmsfbas φranx𝒫AFiny𝒫AFin|xyfBas𝒫AFin
15 fgcl ranx𝒫AFiny𝒫AFin|xyfBas𝒫AFin𝒫AFinfilGenranx𝒫AFiny𝒫AFin|xyFil𝒫AFin
16 14 15 syl φ𝒫AFinfilGenranx𝒫AFiny𝒫AFin|xyFil𝒫AFin
17 1 8 3 5 6 tsmslem1 φy𝒫AFinGFyB
18 17 fmpttd φy𝒫AFinGFy:𝒫AFinB
19 flfval JTopOnB𝒫AFinfilGenranx𝒫AFiny𝒫AFin|xyFil𝒫AFiny𝒫AFinGFy:𝒫AFinBJfLimf𝒫AFinfilGenranx𝒫AFiny𝒫AFin|xyy𝒫AFinGFy=JfLimBFilMapy𝒫AFinGFy𝒫AFinfilGenranx𝒫AFiny𝒫AFin|xy
20 12 16 18 19 syl3anc φJfLimf𝒫AFinfilGenranx𝒫AFiny𝒫AFin|xyy𝒫AFinGFy=JfLimBFilMapy𝒫AFinGFy𝒫AFinfilGenranx𝒫AFiny𝒫AFin|xy
21 10 20 eqtrd φGtsumsF=JfLimBFilMapy𝒫AFinGFy𝒫AFinfilGenranx𝒫AFiny𝒫AFin|xy
22 7 21 eleqtrd φXJfLimBFilMapy𝒫AFinGFy𝒫AFinfilGenranx𝒫AFiny𝒫AFin|xy
23 flimsncls XJfLimBFilMapy𝒫AFinGFy𝒫AFinfilGenranx𝒫AFiny𝒫AFin|xyclsJXJfLimBFilMapy𝒫AFinGFy𝒫AFinfilGenranx𝒫AFiny𝒫AFin|xy
24 22 23 syl φclsJXJfLimBFilMapy𝒫AFinGFy𝒫AFinfilGenranx𝒫AFiny𝒫AFin|xy
25 24 21 sseqtrrd φclsJXGtsumsF