Metamath Proof Explorer


Theorem efmndtmd

Description: The monoid of endofunctions on a set A is a topological monoid. Formerly part of proof for symgtgp . (Contributed by AV, 23-Feb-2024)

Ref Expression
Hypothesis efmndtmd.g No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |-
Assertion efmndtmd AVMTopMnd

Proof

Step Hyp Ref Expression
1 efmndtmd.g Could not format M = ( EndoFMnd ` A ) : No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |-
2 1 efmndmnd AVMMnd
3 eqid BaseM=BaseM
4 1 3 efmndtopn AV𝑡A×𝒫A𝑡BaseM=TopOpenM
5 distopon AV𝒫ATopOnA
6 eqid 𝑡A×𝒫A=𝑡A×𝒫A
7 6 pttoponconst AV𝒫ATopOnA𝑡A×𝒫ATopOnAA
8 5 7 mpdan AV𝑡A×𝒫ATopOnAA
9 1 3 efmndbas BaseM=AA
10 9 eleq2i xBaseMxAA
11 10 biimpi xBaseMxAA
12 11 a1i AVxBaseMxAA
13 12 ssrdv AVBaseMAA
14 resttopon 𝑡A×𝒫ATopOnAABaseMAA𝑡A×𝒫A𝑡BaseMTopOnBaseM
15 8 13 14 syl2anc AV𝑡A×𝒫A𝑡BaseMTopOnBaseM
16 4 15 eqeltrrd AVTopOpenMTopOnBaseM
17 eqid TopOpenM=TopOpenM
18 3 17 istps MTopSpTopOpenMTopOnBaseM
19 16 18 sylibr AVMTopSp
20 eqid +M=+M
21 1 3 20 efmndplusg +M=xBaseM,yBaseMxy
22 eqid 𝒫A^ko𝒫A𝑡BaseM=𝒫A^ko𝒫A𝑡BaseM
23 distop AV𝒫ATop
24 eqid 𝒫A^ko𝒫A=𝒫A^ko𝒫A
25 24 xkotopon 𝒫ATop𝒫ATop𝒫A^ko𝒫ATopOn𝒫ACn𝒫A
26 23 23 25 syl2anc AV𝒫A^ko𝒫ATopOn𝒫ACn𝒫A
27 cndis AV𝒫ATopOnA𝒫ACn𝒫A=AA
28 5 27 mpdan AV𝒫ACn𝒫A=AA
29 13 28 sseqtrrd AVBaseM𝒫ACn𝒫A
30 disllycmp AV𝒫ALocally Comp
31 llynlly 𝒫ALocally Comp 𝒫AN-Locally Comp
32 30 31 syl AV𝒫AN-Locally Comp
33 eqid x𝒫ACn𝒫A,y𝒫ACn𝒫Axy=x𝒫ACn𝒫A,y𝒫ACn𝒫Axy
34 33 xkococn 𝒫ATop𝒫AN-Locally Comp 𝒫ATop x𝒫ACn𝒫A,y𝒫ACn𝒫Axy𝒫A^ko𝒫A×t𝒫A^ko𝒫ACn𝒫A^ko𝒫A
35 23 32 23 34 syl3anc AVx𝒫ACn𝒫A,y𝒫ACn𝒫Axy𝒫A^ko𝒫A×t𝒫A^ko𝒫ACn𝒫A^ko𝒫A
36 22 26 29 22 26 29 35 cnmpt2res AVxBaseM,yBaseMxy𝒫A^ko𝒫A𝑡BaseM×t𝒫A^ko𝒫A𝑡BaseMCn𝒫A^ko𝒫A
37 21 36 eqeltrid AV+M𝒫A^ko𝒫A𝑡BaseM×t𝒫A^ko𝒫A𝑡BaseMCn𝒫A^ko𝒫A
38 xkopt 𝒫ATopAV𝒫A^ko𝒫A=𝑡A×𝒫A
39 23 38 mpancom AV𝒫A^ko𝒫A=𝑡A×𝒫A
40 39 oveq1d AV𝒫A^ko𝒫A𝑡BaseM=𝑡A×𝒫A𝑡BaseM
41 40 4 eqtrd AV𝒫A^ko𝒫A𝑡BaseM=TopOpenM
42 41 41 oveq12d AV𝒫A^ko𝒫A𝑡BaseM×t𝒫A^ko𝒫A𝑡BaseM=TopOpenM×tTopOpenM
43 42 oveq1d AV𝒫A^ko𝒫A𝑡BaseM×t𝒫A^ko𝒫A𝑡BaseMCn𝒫A^ko𝒫A=TopOpenM×tTopOpenMCn𝒫A^ko𝒫A
44 37 43 eleqtrd AV+MTopOpenM×tTopOpenMCn𝒫A^ko𝒫A
45 vex xV
46 vex yV
47 45 46 coex xyV
48 21 47 fnmpoi +MFnBaseM×BaseM
49 eqid +𝑓M=+𝑓M
50 3 20 49 plusfeq +MFnBaseM×BaseM+𝑓M=+M
51 48 50 ax-mp +𝑓M=+M
52 51 eqcomi +M=+𝑓M
53 3 52 mndplusf MMnd+M:BaseM×BaseMBaseM
54 frn +M:BaseM×BaseMBaseMran+MBaseM
55 2 53 54 3syl AVran+MBaseM
56 cnrest2 𝒫A^ko𝒫ATopOn𝒫ACn𝒫Aran+MBaseMBaseM𝒫ACn𝒫A+MTopOpenM×tTopOpenMCn𝒫A^ko𝒫A+MTopOpenM×tTopOpenMCn𝒫A^ko𝒫A𝑡BaseM
57 26 55 29 56 syl3anc AV+MTopOpenM×tTopOpenMCn𝒫A^ko𝒫A+MTopOpenM×tTopOpenMCn𝒫A^ko𝒫A𝑡BaseM
58 44 57 mpbid AV+MTopOpenM×tTopOpenMCn𝒫A^ko𝒫A𝑡BaseM
59 41 oveq2d AVTopOpenM×tTopOpenMCn𝒫A^ko𝒫A𝑡BaseM=TopOpenM×tTopOpenMCnTopOpenM
60 58 59 eleqtrd AV+MTopOpenM×tTopOpenMCnTopOpenM
61 52 17 istmd MTopMndMMndMTopSp+MTopOpenM×tTopOpenMCnTopOpenM
62 2 19 60 61 syl3anbrc AVMTopMnd