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 ` CCfld ) |`s ( 0 [,] 1 ) )
Assertion iistmd 
|- I e. TopMnd

Proof

Step Hyp Ref Expression
1 df-iis 
 |-  I = ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) )
2 cnnrg 
 |-  CCfld e. NrmRing
3 nrgtrg 
 |-  ( CCfld e. NrmRing -> CCfld e. TopRing )
4 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
5 4 trgtmd 
 |-  ( CCfld e. TopRing -> ( mulGrp ` CCfld ) e. TopMnd )
6 2 3 5 mp2b 
 |-  ( mulGrp ` CCfld ) e. TopMnd
7 unitsscn 
 |-  ( 0 [,] 1 ) C_ CC
8 1elunit 
 |-  1 e. ( 0 [,] 1 )
9 iimulcl 
 |-  ( ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) -> ( x x. y ) e. ( 0 [,] 1 ) )
10 9 rgen2 
 |-  A. x e. ( 0 [,] 1 ) A. y e. ( 0 [,] 1 ) ( x x. y ) e. ( 0 [,] 1 )
11 nrgring 
 |-  ( CCfld e. NrmRing -> CCfld e. Ring )
12 4 ringmgp 
 |-  ( CCfld e. Ring -> ( mulGrp ` CCfld ) e. Mnd )
13 2 11 12 mp2b 
 |-  ( mulGrp ` CCfld ) e. Mnd
14 cnfldbas 
 |-  CC = ( Base ` CCfld )
15 4 14 mgpbas 
 |-  CC = ( Base ` ( mulGrp ` CCfld ) )
16 cnfld1 
 |-  1 = ( 1r ` CCfld )
17 4 16 ringidval 
 |-  1 = ( 0g ` ( mulGrp ` CCfld ) )
18 cnfldmul 
 |-  x. = ( .r ` CCfld )
19 4 18 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
20 15 17 19 issubm 
 |-  ( ( mulGrp ` CCfld ) e. Mnd -> ( ( 0 [,] 1 ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) <-> ( ( 0 [,] 1 ) C_ CC /\ 1 e. ( 0 [,] 1 ) /\ A. x e. ( 0 [,] 1 ) A. y e. ( 0 [,] 1 ) ( x x. y ) e. ( 0 [,] 1 ) ) ) )
21 13 20 ax-mp 
 |-  ( ( 0 [,] 1 ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) <-> ( ( 0 [,] 1 ) C_ CC /\ 1 e. ( 0 [,] 1 ) /\ A. x e. ( 0 [,] 1 ) A. y e. ( 0 [,] 1 ) ( x x. y ) e. ( 0 [,] 1 ) ) )
22 7 8 10 21 mpbir3an 
 |-  ( 0 [,] 1 ) e. ( SubMnd ` ( mulGrp ` CCfld ) )
23 1 submtmd 
 |-  ( ( ( mulGrp ` CCfld ) e. TopMnd /\ ( 0 [,] 1 ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) ) -> I e. TopMnd )
24 6 22 23 mp2an 
 |-  I e. TopMnd