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 ⊢ I = mulGrp ℂ fld ↾ 𝑠 0 1
Assertion iistmd ⊢ I ∈ TopMnd

Proof

Step Hyp Ref Expression
1 df-iis ⊢ I = mulGrp ℂ fld ↾ 𝑠 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 ⊢ x ∈ 0 1 ∧ y ∈ 0 1 → x ⁢ y ∈ 0 1
10 9 rgen2 ⊢ ∀ x ∈ 0 1 ∀ y ∈ 0 1 x ⁢ y ∈ 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 = 1 ℂ fld
17 4 16 ringidval ⊢ 1 = 0 mulGrp ℂ fld
18 cnfldmul ⊢ × = ⋅ ℂ fld
19 4 18 mgpplusg ⊢ × = + mulGrp ℂ fld
20 15 17 19 issubm ⊢ mulGrp ℂ fld ∈ Mnd → 0 1 ∈ SubMnd ⁡ mulGrp ℂ fld ↔ 0 1 ⊆ ℂ ∧ 1 ∈ 0 1 ∧ ∀ x ∈ 0 1 ∀ y ∈ 0 1 x ⁢ y ∈ 0 1
21 13 20 ax-mp ⊢ 0 1 ∈ SubMnd ⁡ mulGrp ℂ fld ↔ 0 1 ⊆ ℂ ∧ 1 ∈ 0 1 ∧ ∀ x ∈ 0 1 ∀ y ∈ 0 1 x ⁢ y ∈ 0 1
22 7 8 10 21 mpbir3an ⊢ 0 1 ∈ SubMnd ⁡ mulGrp ℂ fld
23 1 submtmd ⊢ mulGrp ℂ fld ∈ TopMnd ∧ 0 1 ∈ SubMnd ⁡ mulGrp ℂ fld → I ∈ TopMnd
24 6 22 23 mp2an ⊢ I ∈ TopMnd