Metamath Proof Explorer

Theorem iistmd

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

Ref Expression
Hypothesis df-iis ⊢ 𝐼 = ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) )
Assertion iistmd 𝐼 ∈ TopMnd

Proof

Step Hyp Ref Expression
1 df-iis ⊢ 𝐼 = ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) )
2 cnnrg ⊢ ℂfld ∈ NrmRing
3 nrgtrg ⊢ ( ℂfld ∈ NrmRing → ℂfld ∈ TopRing )
4 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
5 4 trgtmd ⊢ ( ℂfld ∈ TopRing → ( mulGrp ‘ ℂfld ) ∈ TopMnd )
6 2 3 5 mp2b ⊢ ( mulGrp ‘ ℂfld ) ∈ TopMnd
7 unitsscn ⊢ ( 0 [,] 1 ) ⊆ ℂ
8 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
9 iimulcl ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) → ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 ) )
10 9 rgen2 ⊢ ∀ 𝑥 ∈ ( 0 [,] 1 ) ∀ 𝑦 ∈ ( 0 [,] 1 ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 )
11 nrgring ⊢ ( ℂfld ∈ NrmRing → ℂfld ∈ Ring )
12 4 ringmgp ⊢ ( ℂfld ∈ Ring → ( mulGrp ‘ ℂfld ) ∈ Mnd )
13 2 11 12 mp2b ⊢ ( mulGrp ‘ ℂfld ) ∈ Mnd
14 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
15 4 14 mgpbas ⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
16 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
17 4 16 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
18 cnfldmul ⊢ · = ( .r ‘ ℂfld )
19 4 18 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
20 15 17 19 issubm ⊢ ( ( mulGrp ‘ ℂfld ) ∈ Mnd → ( ( 0 [,] 1 ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ↔ ( ( 0 [,] 1 ) ⊆ ℂ ∧ 1 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑥 ∈ ( 0 [,] 1 ) ∀ 𝑦 ∈ ( 0 [,] 1 ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 ) ) ) )
21 13 20 ax-mp ⊢ ( ( 0 [,] 1 ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ↔ ( ( 0 [,] 1 ) ⊆ ℂ ∧ 1 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑥 ∈ ( 0 [,] 1 ) ∀ 𝑦 ∈ ( 0 [,] 1 ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 ) ) )
22 7 8 10 21 mpbir3an ⊢ ( 0 [,] 1 ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) )
23 1 submtmd ⊢ ( ( ( mulGrp ‘ ℂfld ) ∈ TopMnd ∧ ( 0 [,] 1 ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ) → 𝐼 ∈ TopMnd )
24 6 22 23 mp2an ⊢ 𝐼 ∈ TopMnd