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 
|- M = ( EndoFMnd ` A )
Assertion efmndtmd 
|- ( A e. V -> M e. TopMnd )

Proof

Step Hyp Ref Expression
1 efmndtmd.g 
 |-  M = ( EndoFMnd ` A )
2 1 efmndmnd 
 |-  ( A e. V -> M e. Mnd )
3 eqid 
 |-  ( Base ` M ) = ( Base ` M )
4 1 3 efmndtopn 
 |-  ( A e. V -> ( ( Xt_ ` ( A X. { ~P A } ) ) |`t ( Base ` M ) ) = ( TopOpen ` M ) )
5 distopon 
 |-  ( A e. V -> ~P A e. ( TopOn ` A ) )
6 eqid 
 |-  ( Xt_ ` ( A X. { ~P A } ) ) = ( Xt_ ` ( A X. { ~P A } ) )
7 6 pttoponconst 
 |-  ( ( A e. V /\ ~P A e. ( TopOn ` A ) ) -> ( Xt_ ` ( A X. { ~P A } ) ) e. ( TopOn ` ( A ^m A ) ) )
8 5 7 mpdan 
 |-  ( A e. V -> ( Xt_ ` ( A X. { ~P A } ) ) e. ( TopOn ` ( A ^m A ) ) )
9 1 3 efmndbas 
 |-  ( Base ` M ) = ( A ^m A )
10 9 eleq2i 
 |-  ( x e. ( Base ` M ) <-> x e. ( A ^m A ) )
11 10 biimpi 
 |-  ( x e. ( Base ` M ) -> x e. ( A ^m A ) )
12 11 a1i 
 |-  ( A e. V -> ( x e. ( Base ` M ) -> x e. ( A ^m A ) ) )
13 12 ssrdv 
 |-  ( A e. V -> ( Base ` M ) C_ ( A ^m A ) )
14 resttopon 
 |-  ( ( ( Xt_ ` ( A X. { ~P A } ) ) e. ( TopOn ` ( A ^m A ) ) /\ ( Base ` M ) C_ ( A ^m A ) ) -> ( ( Xt_ ` ( A X. { ~P A } ) ) |`t ( Base ` M ) ) e. ( TopOn ` ( Base ` M ) ) )
15 8 13 14 syl2anc 
 |-  ( A e. V -> ( ( Xt_ ` ( A X. { ~P A } ) ) |`t ( Base ` M ) ) e. ( TopOn ` ( Base ` M ) ) )
16 4 15 eqeltrrd 
 |-  ( A e. V -> ( TopOpen ` M ) e. ( TopOn ` ( Base ` M ) ) )
17 eqid 
 |-  ( TopOpen ` M ) = ( TopOpen ` M )
18 3 17 istps 
 |-  ( M e. TopSp <-> ( TopOpen ` M ) e. ( TopOn ` ( Base ` M ) ) )
19 16 18 sylibr 
 |-  ( A e. V -> M e. TopSp )
20 eqid 
 |-  ( +g ` M ) = ( +g ` M )
21 1 3 20 efmndplusg 
 |-  ( +g ` M ) = ( x e. ( Base ` M ) , y e. ( Base ` M ) |-> ( x o. y ) )
22 eqid 
 |-  ( ( ~P A ^ko ~P A ) |`t ( Base ` M ) ) = ( ( ~P A ^ko ~P A ) |`t ( Base ` M ) )
23 distop 
 |-  ( A e. V -> ~P A e. Top )
24 eqid 
 |-  ( ~P A ^ko ~P A ) = ( ~P A ^ko ~P A )
25 24 xkotopon 
 |-  ( ( ~P A e. Top /\ ~P A e. Top ) -> ( ~P A ^ko ~P A ) e. ( TopOn ` ( ~P A Cn ~P A ) ) )
26 23 23 25 syl2anc 
 |-  ( A e. V -> ( ~P A ^ko ~P A ) e. ( TopOn ` ( ~P A Cn ~P A ) ) )
27 cndis 
 |-  ( ( A e. V /\ ~P A e. ( TopOn ` A ) ) -> ( ~P A Cn ~P A ) = ( A ^m A ) )
28 5 27 mpdan 
 |-  ( A e. V -> ( ~P A Cn ~P A ) = ( A ^m A ) )
29 13 28 sseqtrrd 
 |-  ( A e. V -> ( Base ` M ) C_ ( ~P A Cn ~P A ) )
30 disllycmp 
 |-  ( A e. V -> ~P A e. Locally Comp )
31 llynlly 
 |-  ( ~P A e. Locally Comp -> ~P A e. N-Locally Comp )
32 30 31 syl 
 |-  ( A e. V -> ~P A e. N-Locally Comp )
33 eqid 
 |-  ( x e. ( ~P A Cn ~P A ) , y e. ( ~P A Cn ~P A ) |-> ( x o. y ) ) = ( x e. ( ~P A Cn ~P A ) , y e. ( ~P A Cn ~P A ) |-> ( x o. y ) )
34 33 xkococn 
 |-  ( ( ~P A e. Top /\ ~P A e. N-Locally Comp /\ ~P A e. Top ) -> ( x e. ( ~P A Cn ~P A ) , y e. ( ~P A Cn ~P A ) |-> ( x o. y ) ) e. ( ( ( ~P A ^ko ~P A ) tX ( ~P A ^ko ~P A ) ) Cn ( ~P A ^ko ~P A ) ) )
35 23 32 23 34 syl3anc 
 |-  ( A e. V -> ( x e. ( ~P A Cn ~P A ) , y e. ( ~P A Cn ~P A ) |-> ( x o. y ) ) e. ( ( ( ~P A ^ko ~P A ) tX ( ~P A ^ko ~P A ) ) Cn ( ~P A ^ko ~P A ) ) )
36 22 26 29 22 26 29 35 cnmpt2res 
 |-  ( A e. V -> ( x e. ( Base ` M ) , y e. ( Base ` M ) |-> ( x o. y ) ) e. ( ( ( ( ~P A ^ko ~P A ) |`t ( Base ` M ) ) tX ( ( ~P A ^ko ~P A ) |`t ( Base ` M ) ) ) Cn ( ~P A ^ko ~P A ) ) )
37 21 36 eqeltrid 
 |-  ( A e. V -> ( +g ` M ) e. ( ( ( ( ~P A ^ko ~P A ) |`t ( Base ` M ) ) tX ( ( ~P A ^ko ~P A ) |`t ( Base ` M ) ) ) Cn ( ~P A ^ko ~P A ) ) )
38 xkopt 
 |-  ( ( ~P A e. Top /\ A e. V ) -> ( ~P A ^ko ~P A ) = ( Xt_ ` ( A X. { ~P A } ) ) )
39 23 38 mpancom 
 |-  ( A e. V -> ( ~P A ^ko ~P A ) = ( Xt_ ` ( A X. { ~P A } ) ) )
40 39 oveq1d 
 |-  ( A e. V -> ( ( ~P A ^ko ~P A ) |`t ( Base ` M ) ) = ( ( Xt_ ` ( A X. { ~P A } ) ) |`t ( Base ` M ) ) )
41 40 4 eqtrd 
 |-  ( A e. V -> ( ( ~P A ^ko ~P A ) |`t ( Base ` M ) ) = ( TopOpen ` M ) )
42 41 41 oveq12d 
 |-  ( A e. V -> ( ( ( ~P A ^ko ~P A ) |`t ( Base ` M ) ) tX ( ( ~P A ^ko ~P A ) |`t ( Base ` M ) ) ) = ( ( TopOpen ` M ) tX ( TopOpen ` M ) ) )
43 42 oveq1d 
 |-  ( A e. V -> ( ( ( ( ~P A ^ko ~P A ) |`t ( Base ` M ) ) tX ( ( ~P A ^ko ~P A ) |`t ( Base ` M ) ) ) Cn ( ~P A ^ko ~P A ) ) = ( ( ( TopOpen ` M ) tX ( TopOpen ` M ) ) Cn ( ~P A ^ko ~P A ) ) )
44 37 43 eleqtrd 
 |-  ( A e. V -> ( +g ` M ) e. ( ( ( TopOpen ` M ) tX ( TopOpen ` M ) ) Cn ( ~P A ^ko ~P A ) ) )
45 vex 
 |-  x e. _V
46 vex 
 |-  y e. _V
47 45 46 coex 
 |-  ( x o. y ) e. _V
48 21 47 fnmpoi 
 |-  ( +g ` M ) Fn ( ( Base ` M ) X. ( Base ` M ) )
49 eqid 
 |-  ( +f ` M ) = ( +f ` M )
50 3 20 49 plusfeq 
 |-  ( ( +g ` M ) Fn ( ( Base ` M ) X. ( Base ` M ) ) -> ( +f ` M ) = ( +g ` M ) )
51 48 50 ax-mp 
 |-  ( +f ` M ) = ( +g ` M )
52 51 eqcomi 
 |-  ( +g ` M ) = ( +f ` M )
53 3 52 mndplusf 
 |-  ( M e. Mnd -> ( +g ` M ) : ( ( Base ` M ) X. ( Base ` M ) ) --> ( Base ` M ) )
54 frn 
 |-  ( ( +g ` M ) : ( ( Base ` M ) X. ( Base ` M ) ) --> ( Base ` M ) -> ran ( +g ` M ) C_ ( Base ` M ) )
55 2 53 54 3syl 
 |-  ( A e. V -> ran ( +g ` M ) C_ ( Base ` M ) )
56 cnrest2 
 |-  ( ( ( ~P A ^ko ~P A ) e. ( TopOn ` ( ~P A Cn ~P A ) ) /\ ran ( +g ` M ) C_ ( Base ` M ) /\ ( Base ` M ) C_ ( ~P A Cn ~P A ) ) -> ( ( +g ` M ) e. ( ( ( TopOpen ` M ) tX ( TopOpen ` M ) ) Cn ( ~P A ^ko ~P A ) ) <-> ( +g ` M ) e. ( ( ( TopOpen ` M ) tX ( TopOpen ` M ) ) Cn ( ( ~P A ^ko ~P A ) |`t ( Base ` M ) ) ) ) )
57 26 55 29 56 syl3anc 
 |-  ( A e. V -> ( ( +g ` M ) e. ( ( ( TopOpen ` M ) tX ( TopOpen ` M ) ) Cn ( ~P A ^ko ~P A ) ) <-> ( +g ` M ) e. ( ( ( TopOpen ` M ) tX ( TopOpen ` M ) ) Cn ( ( ~P A ^ko ~P A ) |`t ( Base ` M ) ) ) ) )
58 44 57 mpbid 
 |-  ( A e. V -> ( +g ` M ) e. ( ( ( TopOpen ` M ) tX ( TopOpen ` M ) ) Cn ( ( ~P A ^ko ~P A ) |`t ( Base ` M ) ) ) )
59 41 oveq2d 
 |-  ( A e. V -> ( ( ( TopOpen ` M ) tX ( TopOpen ` M ) ) Cn ( ( ~P A ^ko ~P A ) |`t ( Base ` M ) ) ) = ( ( ( TopOpen ` M ) tX ( TopOpen ` M ) ) Cn ( TopOpen ` M ) ) )
60 58 59 eleqtrd 
 |-  ( A e. V -> ( +g ` M ) e. ( ( ( TopOpen ` M ) tX ( TopOpen ` M ) ) Cn ( TopOpen ` M ) ) )
61 52 17 istmd 
 |-  ( M e. TopMnd <-> ( M e. Mnd /\ M e. TopSp /\ ( +g ` M ) e. ( ( ( TopOpen ` M ) tX ( TopOpen ` M ) ) Cn ( TopOpen ` M ) ) ) )
62 2 19 60 61 syl3anbrc 
 |-  ( A e. V -> M e. TopMnd )