iistmd

Description: The closed unit interval forms a topological monoid under multiplication. (Contributed by Thierry Arnoux, 25-Mar-2017)

		Ref	Expression
	Hypothesis	df-iis	$⊢ I = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} [0, 1]$
	Assertion	iistmd	$⊢ I \in TopMnd$

Proof

Step	Hyp	Ref	Expression
1		df-iis	$⊢ I = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} [0, 1]$
2		cnnrg	$⊢ ℂ_{fld} \in NrmRing$
3		nrgtrg	$⊢ ℂ_{fld} \in NrmRing \to ℂ_{fld} \in TopRing$
4		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
5	4	trgtmd	$⊢ ℂ_{fld} \in TopRing \to {mulGrp}_{ℂ_{fld}} \in TopMnd$
6	2 3 5	mp2b	$⊢ {mulGrp}_{ℂ_{fld}} \in TopMnd$
7		unitsscn	$⊢ [0, 1] \subseteq ℂ$
8		1elunit	$⊢ 1 \in [0, 1]$
9		iimulcl	$⊢ (x \in [0, 1] \land y \in [0, 1]) \to x y \in [0, 1]$
10	9	rgen2	$⊢ \forall x \in [0, 1] \forall y \in [0, 1] x y \in [0, 1]$
11		nrgring	$⊢ ℂ_{fld} \in NrmRing \to ℂ_{fld} \in Ring$
12	4	ringmgp	$⊢ ℂ_{fld} \in Ring \to {mulGrp}_{ℂ_{fld}} \in Mnd$
13	2 11 12	mp2b	$⊢ {mulGrp}_{ℂ_{fld}} \in Mnd$
14		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
15	4 14	mgpbas	$⊢ ℂ = {Base}_{{mulGrp}_{ℂ_{fld}}}$
16		cnfld1	$⊢ 1 = 1_{ℂ_{fld}}$
17	4 16	ringidval	$⊢ 1 = 0_{{mulGrp}_{ℂ_{fld}}}$
18		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
19	4 18	mgpplusg	$⊢ \times = +_{{mulGrp}_{ℂ_{fld}}}$
20	15 17 19	issubm	$⊢ {mulGrp}_{ℂ_{fld}} \in Mnd \to ([0, 1] \in SubMnd ({mulGrp}_{ℂ_{fld}}) \leftrightarrow ([0, 1] \subseteq ℂ \land 1 \in [0, 1] \land \forall x \in [0, 1] \forall y \in [0, 1] x y \in [0, 1]))$
21	13 20	ax-mp	$⊢ [0, 1] \in SubMnd ({mulGrp}_{ℂ_{fld}}) \leftrightarrow ([0, 1] \subseteq ℂ \land 1 \in [0, 1] \land \forall x \in [0, 1] \forall y \in [0, 1] x y \in [0, 1])$
22	7 8 10 21	mpbir3an	$⊢ [0, 1] \in SubMnd ({mulGrp}_{ℂ_{fld}})$
23	1	submtmd	$⊢ ({mulGrp}_{ℂ_{fld}} \in TopMnd \land [0, 1] \in SubMnd ({mulGrp}_{ℂ_{fld}})) \to I \in TopMnd$
24	6 22 23	mp2an	$⊢ I \in TopMnd$

Metamath Proof Explorer

Theorem iistmd

Proof