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 ⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 )
Assertion efmndtmd ( 𝐴 ∈ 𝑉 → 𝑀 ∈ TopMnd )

Proof

Step Hyp Ref Expression
1 efmndtmd.g ⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 )
2 1 efmndmnd ⊢ ( 𝐴 ∈ 𝑉 → 𝑀 ∈ Mnd )
3 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
4 1 3 efmndtopn ⊢ ( 𝐴 ∈ 𝑉 → ( ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ↾t ( Base ‘ 𝑀 ) ) = ( TopOpen ‘ 𝑀 ) )
5 distopon ⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ ( TopOn ‘ 𝐴 ) )
6 eqid ⊢ ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) )
7 6 pttoponconst ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝒫 𝐴 ∈ ( TopOn ‘ 𝐴 ) ) → ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ∈ ( TopOn ‘ ( 𝐴 ↑m 𝐴 ) ) )
8 5 7 mpdan ⊢ ( 𝐴 ∈ 𝑉 → ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ∈ ( TopOn ‘ ( 𝐴 ↑m 𝐴 ) ) )
9 1 3 efmndbas ⊢ ( Base ‘ 𝑀 ) = ( 𝐴 ↑m 𝐴 )
10 9 eleq2i ⊢ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ↔ 𝑥 ∈ ( 𝐴 ↑m 𝐴 ) )
11 10 biimpi ⊢ ( 𝑥 ∈ ( Base ‘ 𝑀 ) → 𝑥 ∈ ( 𝐴 ↑m 𝐴 ) )
12 11 a1i ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( Base ‘ 𝑀 ) → 𝑥 ∈ ( 𝐴 ↑m 𝐴 ) ) )
13 12 ssrdv ⊢ ( 𝐴 ∈ 𝑉 → ( Base ‘ 𝑀 ) ⊆ ( 𝐴 ↑m 𝐴 ) )
14 resttopon ⊢ ( ( ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ∈ ( TopOn ‘ ( 𝐴 ↑m 𝐴 ) ) ∧ ( Base ‘ 𝑀 ) ⊆ ( 𝐴 ↑m 𝐴 ) ) → ( ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ↾t ( Base ‘ 𝑀 ) ) ∈ ( TopOn ‘ ( Base ‘ 𝑀 ) ) )
15 8 13 14 syl2anc ⊢ ( 𝐴 ∈ 𝑉 → ( ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ↾t ( Base ‘ 𝑀 ) ) ∈ ( TopOn ‘ ( Base ‘ 𝑀 ) ) )
16 4 15 eqeltrrd ⊢ ( 𝐴 ∈ 𝑉 → ( TopOpen ‘ 𝑀 ) ∈ ( TopOn ‘ ( Base ‘ 𝑀 ) ) )
17 eqid ⊢ ( TopOpen ‘ 𝑀 ) = ( TopOpen ‘ 𝑀 )
18 3 17 istps ⊢ ( 𝑀 ∈ TopSp ↔ ( TopOpen ‘ 𝑀 ) ∈ ( TopOn ‘ ( Base ‘ 𝑀 ) ) )
19 16 18 sylibr ⊢ ( 𝐴 ∈ 𝑉 → 𝑀 ∈ TopSp )
20 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
21 1 3 20 efmndplusg ⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ ( Base ‘ 𝑀 ) , 𝑦 ∈ ( Base ‘ 𝑀 ) ↦ ( 𝑥 ∘ 𝑦 ) )
22 eqid ⊢ ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ↾t ( Base ‘ 𝑀 ) ) = ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ↾t ( Base ‘ 𝑀 ) )
23 distop ⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top )
24 eqid ⊢ ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) = ( 𝒫 𝐴 ↑ko 𝒫 𝐴 )
25 24 xkotopon ⊢ ( ( 𝒫 𝐴 ∈ Top ∧ 𝒫 𝐴 ∈ Top ) → ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ∈ ( TopOn ‘ ( 𝒫 𝐴 Cn 𝒫 𝐴 ) ) )
26 23 23 25 syl2anc ⊢ ( 𝐴 ∈ 𝑉 → ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ∈ ( TopOn ‘ ( 𝒫 𝐴 Cn 𝒫 𝐴 ) ) )
27 cndis ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝒫 𝐴 ∈ ( TopOn ‘ 𝐴 ) ) → ( 𝒫 𝐴 Cn 𝒫 𝐴 ) = ( 𝐴 ↑m 𝐴 ) )
28 5 27 mpdan ⊢ ( 𝐴 ∈ 𝑉 → ( 𝒫 𝐴 Cn 𝒫 𝐴 ) = ( 𝐴 ↑m 𝐴 ) )
29 13 28 sseqtrrd ⊢ ( 𝐴 ∈ 𝑉 → ( Base ‘ 𝑀 ) ⊆ ( 𝒫 𝐴 Cn 𝒫 𝐴 ) )
30 disllycmp ⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Locally Comp )
31 llynlly ⊢ ( 𝒫 𝐴 ∈ Locally Comp → 𝒫 𝐴 ∈ 𝑛-Locally Comp )
32 30 31 syl ⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ 𝑛-Locally Comp )
33 eqid ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 Cn 𝒫 𝐴 ) , 𝑦 ∈ ( 𝒫 𝐴 Cn 𝒫 𝐴 ) ↦ ( 𝑥 ∘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝒫 𝐴 Cn 𝒫 𝐴 ) , 𝑦 ∈ ( 𝒫 𝐴 Cn 𝒫 𝐴 ) ↦ ( 𝑥 ∘ 𝑦 ) )
34 33 xkococn ⊢ ( ( 𝒫 𝐴 ∈ Top ∧ 𝒫 𝐴 ∈ 𝑛-Locally Comp ∧ 𝒫 𝐴 ∈ Top ) → ( 𝑥 ∈ ( 𝒫 𝐴 Cn 𝒫 𝐴 ) , 𝑦 ∈ ( 𝒫 𝐴 Cn 𝒫 𝐴 ) ↦ ( 𝑥 ∘ 𝑦 ) ) ∈ ( ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ×t ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ) Cn ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ) )
35 23 32 23 34 syl3anc ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( 𝒫 𝐴 Cn 𝒫 𝐴 ) , 𝑦 ∈ ( 𝒫 𝐴 Cn 𝒫 𝐴 ) ↦ ( 𝑥 ∘ 𝑦 ) ) ∈ ( ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ×t ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ) Cn ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ) )
36 22 26 29 22 26 29 35 cnmpt2res ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( Base ‘ 𝑀 ) , 𝑦 ∈ ( Base ‘ 𝑀 ) ↦ ( 𝑥 ∘ 𝑦 ) ) ∈ ( ( ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ↾t ( Base ‘ 𝑀 ) ) ×t ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ↾t ( Base ‘ 𝑀 ) ) ) Cn ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ) )
37 21 36 eqeltrid ⊢ ( 𝐴 ∈ 𝑉 → ( +g ‘ 𝑀 ) ∈ ( ( ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ↾t ( Base ‘ 𝑀 ) ) ×t ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ↾t ( Base ‘ 𝑀 ) ) ) Cn ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ) )
38 xkopt ⊢ ( ( 𝒫 𝐴 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) = ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) )
39 23 38 mpancom ⊢ ( 𝐴 ∈ 𝑉 → ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) = ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) )
40 39 oveq1d ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ↾t ( Base ‘ 𝑀 ) ) = ( ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ↾t ( Base ‘ 𝑀 ) ) )
41 40 4 eqtrd ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ↾t ( Base ‘ 𝑀 ) ) = ( TopOpen ‘ 𝑀 ) )
42 41 41 oveq12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ↾t ( Base ‘ 𝑀 ) ) ×t ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ↾t ( Base ‘ 𝑀 ) ) ) = ( ( TopOpen ‘ 𝑀 ) ×t ( TopOpen ‘ 𝑀 ) ) )
43 42 oveq1d ⊢ ( 𝐴 ∈ 𝑉 → ( ( ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ↾t ( Base ‘ 𝑀 ) ) ×t ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ↾t ( Base ‘ 𝑀 ) ) ) Cn ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ) = ( ( ( TopOpen ‘ 𝑀 ) ×t ( TopOpen ‘ 𝑀 ) ) Cn ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ) )
44 37 43 eleqtrd ⊢ ( 𝐴 ∈ 𝑉 → ( +g ‘ 𝑀 ) ∈ ( ( ( TopOpen ‘ 𝑀 ) ×t ( TopOpen ‘ 𝑀 ) ) Cn ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ) )
45 vex ⊢ 𝑥 ∈ V
46 vex ⊢ 𝑦 ∈ V
47 45 46 coex ⊢ ( 𝑥 ∘ 𝑦 ) ∈ V
48 21 47 fnmpoi ⊢ ( +g ‘ 𝑀 ) Fn ( ( Base ‘ 𝑀 ) × ( Base ‘ 𝑀 ) )
49 eqid ⊢ ( +𝑓 ‘ 𝑀 ) = ( +𝑓 ‘ 𝑀 )
50 3 20 49 plusfeq ⊢ ( ( +g ‘ 𝑀 ) Fn ( ( Base ‘ 𝑀 ) × ( Base ‘ 𝑀 ) ) → ( +𝑓 ‘ 𝑀 ) = ( +g ‘ 𝑀 ) )
51 48 50 ax-mp ⊢ ( +𝑓 ‘ 𝑀 ) = ( +g ‘ 𝑀 )
52 51 eqcomi ⊢ ( +g ‘ 𝑀 ) = ( +𝑓 ‘ 𝑀 )
53 3 52 mndplusf ⊢ ( 𝑀 ∈ Mnd → ( +g ‘ 𝑀 ) : ( ( Base ‘ 𝑀 ) × ( Base ‘ 𝑀 ) ) ⟶ ( Base ‘ 𝑀 ) )
54 frn ⊢ ( ( +g ‘ 𝑀 ) : ( ( Base ‘ 𝑀 ) × ( Base ‘ 𝑀 ) ) ⟶ ( Base ‘ 𝑀 ) → ran ( +g ‘ 𝑀 ) ⊆ ( Base ‘ 𝑀 ) )
55 2 53 54 3syl ⊢ ( 𝐴 ∈ 𝑉 → ran ( +g ‘ 𝑀 ) ⊆ ( Base ‘ 𝑀 ) )
56 cnrest2 ⊢ ( ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ∈ ( TopOn ‘ ( 𝒫 𝐴 Cn 𝒫 𝐴 ) ) ∧ ran ( +g ‘ 𝑀 ) ⊆ ( Base ‘ 𝑀 ) ∧ ( Base ‘ 𝑀 ) ⊆ ( 𝒫 𝐴 Cn 𝒫 𝐴 ) ) → ( ( +g ‘ 𝑀 ) ∈ ( ( ( TopOpen ‘ 𝑀 ) ×t ( TopOpen ‘ 𝑀 ) ) Cn ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ) ↔ ( +g ‘ 𝑀 ) ∈ ( ( ( TopOpen ‘ 𝑀 ) ×t ( TopOpen ‘ 𝑀 ) ) Cn ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ↾t ( Base ‘ 𝑀 ) ) ) ) )
57 26 55 29 56 syl3anc ⊢ ( 𝐴 ∈ 𝑉 → ( ( +g ‘ 𝑀 ) ∈ ( ( ( TopOpen ‘ 𝑀 ) ×t ( TopOpen ‘ 𝑀 ) ) Cn ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ) ↔ ( +g ‘ 𝑀 ) ∈ ( ( ( TopOpen ‘ 𝑀 ) ×t ( TopOpen ‘ 𝑀 ) ) Cn ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ↾t ( Base ‘ 𝑀 ) ) ) ) )
58 44 57 mpbid ⊢ ( 𝐴 ∈ 𝑉 → ( +g ‘ 𝑀 ) ∈ ( ( ( TopOpen ‘ 𝑀 ) ×t ( TopOpen ‘ 𝑀 ) ) Cn ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ↾t ( Base ‘ 𝑀 ) ) ) )
59 41 oveq2d ⊢ ( 𝐴 ∈ 𝑉 → ( ( ( TopOpen ‘ 𝑀 ) ×t ( TopOpen ‘ 𝑀 ) ) Cn ( ( 𝒫 𝐴 ↑ko 𝒫 𝐴 ) ↾t ( Base ‘ 𝑀 ) ) ) = ( ( ( TopOpen ‘ 𝑀 ) ×t ( TopOpen ‘ 𝑀 ) ) Cn ( TopOpen ‘ 𝑀 ) ) )
60 58 59 eleqtrd ⊢ ( 𝐴 ∈ 𝑉 → ( +g ‘ 𝑀 ) ∈ ( ( ( TopOpen ‘ 𝑀 ) ×t ( TopOpen ‘ 𝑀 ) ) Cn ( TopOpen ‘ 𝑀 ) ) )
61 52 17 istmd ⊢ ( 𝑀 ∈ TopMnd ↔ ( 𝑀 ∈ Mnd ∧ 𝑀 ∈ TopSp ∧ ( +g ‘ 𝑀 ) ∈ ( ( ( TopOpen ‘ 𝑀 ) ×t ( TopOpen ‘ 𝑀 ) ) Cn ( TopOpen ‘ 𝑀 ) ) ) )
62 2 19 60 61 syl3anbrc ⊢ ( 𝐴 ∈ 𝑉 → 𝑀 ∈ TopMnd )