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	$⊢ A \in V \to M \in TopMnd$

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	$⊢ A \in V \to M \in Mnd$
3		eqid	$⊢ {Base}_{M} = {Base}_{M}$
4	1 3	efmndtopn	$⊢ A \in V \to \prod_{𝑡} (A \times \{𝒫 A\}) ↾_{𝑡} {Base}_{M} = TopOpen (M)$
5		distopon	$⊢ A \in V \to 𝒫 A \in TopOn (A)$
6		eqid	$⊢ \prod_{𝑡} (A \times \{𝒫 A\}) = \prod_{𝑡} (A \times \{𝒫 A\})$
7	6	pttoponconst	$⊢ (A \in V \land 𝒫 A \in TopOn (A)) \to \prod_{𝑡} (A \times \{𝒫 A\}) \in TopOn (A^{A})$
8	5 7	mpdan	$⊢ A \in V \to \prod_{𝑡} (A \times \{𝒫 A\}) \in TopOn (A^{A})$
9	1 3	efmndbas	$⊢ {Base}_{M} = A^{A}$
10	9	eleq2i	$⊢ x \in {Base}_{M} \leftrightarrow x \in (A^{A})$
11	10	biimpi	$⊢ x \in {Base}_{M} \to x \in (A^{A})$
12	11	a1i	$⊢ A \in V \to (x \in {Base}_{M} \to x \in (A^{A}))$
13	12	ssrdv	$⊢ A \in V \to {Base}_{M} \subseteq A^{A}$
14		resttopon	$⊢ (\prod_{𝑡} (A \times \{𝒫 A\}) \in TopOn (A^{A}) \land {Base}_{M} \subseteq A^{A}) \to \prod_{𝑡} (A \times \{𝒫 A\}) ↾_{𝑡} {Base}_{M} \in TopOn ({Base}_{M})$
15	8 13 14	syl2anc	$⊢ A \in V \to \prod_{𝑡} (A \times \{𝒫 A\}) ↾_{𝑡} {Base}_{M} \in TopOn ({Base}_{M})$
16	4 15	eqeltrrd	$⊢ A \in V \to TopOpen (M) \in TopOn ({Base}_{M})$
17		eqid	$⊢ TopOpen (M) = TopOpen (M)$
18	3 17	istps	$⊢ M \in TopSp \leftrightarrow TopOpen (M) \in TopOn ({Base}_{M})$
19	16 18	sylibr	$⊢ A \in V \to M \in TopSp$
20		eqid	$⊢ +_{M} = +_{M}$
21	1 3 20	efmndplusg	$⊢ +_{M} = (x \in {Base}_{M}, y \in {Base}_{M} ⟼ x \circ y)$
22		eqid	$⊢ (𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{M} = (𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{M}$
23		distop	$⊢ A \in V \to 𝒫 A \in Top$
24		eqid	$⊢ 𝒫 A^_{ko} 𝒫 A = 𝒫 A^_{ko} 𝒫 A$
25	24	xkotopon	$⊢ (𝒫 A \in Top \land 𝒫 A \in Top) \to 𝒫 A^_{ko} 𝒫 A \in TopOn (𝒫 A Cn 𝒫 A)$
26	23 23 25	syl2anc	$⊢ A \in V \to 𝒫 A^_{ko} 𝒫 A \in TopOn (𝒫 A Cn 𝒫 A)$
27		cndis	$⊢ (A \in V \land 𝒫 A \in TopOn (A)) \to 𝒫 A Cn 𝒫 A = A^{A}$
28	5 27	mpdan	$⊢ A \in V \to 𝒫 A Cn 𝒫 A = A^{A}$
29	13 28	sseqtrrd	$⊢ A \in V \to {Base}_{M} \subseteq 𝒫 A Cn 𝒫 A$
30		disllycmp	$⊢ A \in V \to 𝒫 A \in LocallyComp$
31		llynlly	$⊢ 𝒫 A \in LocallyComp\to𝒫 A \in N-LocallyComp$
32	30 31	syl	$⊢ A \in V \to 𝒫 A \in N-LocallyComp$
33		eqid	$⊢ (x \in (𝒫 A Cn 𝒫 A), y \in (𝒫 A Cn 𝒫 A) ⟼ x \circ y) = (x \in (𝒫 A Cn 𝒫 A), y \in (𝒫 A Cn 𝒫 A) ⟼ x \circ y)$
34	33	xkococn	$⊢ (𝒫 A \in Top \land 𝒫 A \in N-LocallyComp\land𝒫 A \in Top\to(x \in (𝒫 A Cn 𝒫 A), y \in (𝒫 A Cn 𝒫 A) ⟼ x \circ y) \in (((𝒫 A^_{ko} 𝒫 A) \times_{t} (𝒫 A^_{ko} 𝒫 A)) Cn (𝒫 A^_{ko} 𝒫 A)))$
35	23 32 23 34	syl3anc	$⊢ A \in V \to (x \in (𝒫 A Cn 𝒫 A), y \in (𝒫 A Cn 𝒫 A) ⟼ x \circ y) \in (((𝒫 A^_{ko} 𝒫 A) \times_{t} (𝒫 A^_{ko} 𝒫 A)) Cn (𝒫 A^_{ko} 𝒫 A))$
36	22 26 29 22 26 29 35	cnmpt2res	$⊢ A \in V \to (x \in {Base}_{M}, y \in {Base}_{M} ⟼ x \circ y) \in ((((𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{M}) \times_{t} ((𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{M})) Cn (𝒫 A^_{ko} 𝒫 A))$
37	21 36	eqeltrid	$⊢ A \in V \to +_{M} \in ((((𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{M}) \times_{t} ((𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{M})) Cn (𝒫 A^_{ko} 𝒫 A))$
38		xkopt	$⊢ (𝒫 A \in Top \land A \in V) \to 𝒫 A^_{ko} 𝒫 A = \prod_{𝑡} (A \times \{𝒫 A\})$
39	23 38	mpancom	$⊢ A \in V \to 𝒫 A^_{ko} 𝒫 A = \prod_{𝑡} (A \times \{𝒫 A\})$
40	39	oveq1d	$⊢ A \in V \to (𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{M} = \prod_{𝑡} (A \times \{𝒫 A\}) ↾_{𝑡} {Base}_{M}$
41	40 4	eqtrd	$⊢ A \in V \to (𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{M} = TopOpen (M)$
42	41 41	oveq12d	$⊢ A \in V \to ((𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{M}) \times_{t} ((𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{M}) = TopOpen (M) \times_{t} TopOpen (M)$
43	42	oveq1d	$⊢ A \in V \to (((𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{M}) \times_{t} ((𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{M})) Cn (𝒫 A^_{ko} 𝒫 A) = (TopOpen (M) \times_{t} TopOpen (M)) Cn (𝒫 A^_{ko} 𝒫 A)$
44	37 43	eleqtrd	$⊢ A \in V \to +_{M} \in ((TopOpen (M) \times_{t} TopOpen (M)) Cn (𝒫 A^_{ko} 𝒫 A))$
45		vex	$⊢ x \in V$
46		vex	$⊢ y \in V$
47	45 46	coex	$⊢ x \circ y \in V$
48	21 47	fnmpoi	$⊢ +_{M} Fn ({Base}_{M} \times {Base}_{M})$
49		eqid	$⊢ +_{𝑓} (M) = +_{𝑓} (M)$
50	3 20 49	plusfeq	$⊢ +_{M} Fn ({Base}_{M} \times {Base}_{M}) \to +_{𝑓} (M) = +_{M}$
51	48 50	ax-mp	$⊢ +_{𝑓} (M) = +_{M}$
52	51	eqcomi	$⊢ +_{M} = +_{𝑓} (M)$
53	3 52	mndplusf	$⊢ M \in Mnd \to +_{M} : {Base}_{M} \times {Base}_{M} ⟶ {Base}_{M}$
54		frn	$⊢ +_{M} : {Base}_{M} \times {Base}_{M} ⟶ {Base}_{M} \to ran +_{M} \subseteq {Base}_{M}$
55	2 53 54	3syl	$⊢ A \in V \to ran +_{M} \subseteq {Base}_{M}$
56		cnrest2	$⊢ (𝒫 A^_{ko} 𝒫 A \in TopOn (𝒫 A Cn 𝒫 A) \land ran +_{M} \subseteq {Base}_{M} \land {Base}_{M} \subseteq 𝒫 A Cn 𝒫 A) \to (+_{M} \in ((TopOpen (M) \times_{t} TopOpen (M)) Cn (𝒫 A^_{ko} 𝒫 A)) \leftrightarrow +_{M} \in ((TopOpen (M) \times_{t} TopOpen (M)) Cn ((𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{M})))$
57	26 55 29 56	syl3anc	$⊢ A \in V \to (+_{M} \in ((TopOpen (M) \times_{t} TopOpen (M)) Cn (𝒫 A^_{ko} 𝒫 A)) \leftrightarrow +_{M} \in ((TopOpen (M) \times_{t} TopOpen (M)) Cn ((𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{M})))$
58	44 57	mpbid	$⊢ A \in V \to +_{M} \in ((TopOpen (M) \times_{t} TopOpen (M)) Cn ((𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{M}))$
59	41	oveq2d	$⊢ A \in V \to (TopOpen (M) \times_{t} TopOpen (M)) Cn ((𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{M}) = (TopOpen (M) \times_{t} TopOpen (M)) Cn TopOpen (M)$
60	58 59	eleqtrd	$⊢ A \in V \to +_{M} \in ((TopOpen (M) \times_{t} TopOpen (M)) Cn TopOpen (M))$
61	52 17	istmd	$⊢ M \in TopMnd \leftrightarrow (M \in Mnd \land M \in TopSp \land +_{M} \in ((TopOpen (M) \times_{t} TopOpen (M)) Cn TopOpen (M)))$
62	2 19 60 61	syl3anbrc	$⊢ A \in V \to M \in TopMnd$

Metamath Proof Explorer

Theorem efmndtmd

Proof