Metamath Proof Explorer

Theorem nrgtdrg

Description: A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Assertion nrgtdrg ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) → 𝑅 ∈ TopDRing )

Proof

Step Hyp Ref Expression
1 nrgtrg ⊢ ( 𝑅 ∈ NrmRing → 𝑅 ∈ TopRing )
2 1 adantr ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) → 𝑅 ∈ TopRing )
3 simpr ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) → 𝑅 ∈ DivRing )
4 nrgring ⊢ ( 𝑅 ∈ NrmRing → 𝑅 ∈ Ring )
5 4 adantr ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) → 𝑅 ∈ Ring )
6 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
7 eqid ⊢ ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) )
8 6 7 unitgrp ⊢ ( 𝑅 ∈ Ring → ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) ∈ Grp )
9 5 8 syl ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) → ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) ∈ Grp )
10 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
11 10 trgtmd ⊢ ( 𝑅 ∈ TopRing → ( mulGrp ‘ 𝑅 ) ∈ TopMnd )
12 2 11 syl ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) → ( mulGrp ‘ 𝑅 ) ∈ TopMnd )
13 6 10 unitsubm ⊢ ( 𝑅 ∈ Ring → ( Unit ‘ 𝑅 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
14 5 13 syl ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) → ( Unit ‘ 𝑅 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
15 7 submtmd ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ TopMnd ∧ ( Unit ‘ 𝑅 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ) → ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) ∈ TopMnd )
16 12 14 15 syl2anc ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) → ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) ∈ TopMnd )
17 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
18 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
19 eqid ⊢ ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
20 17 6 18 19 nrginvrcn ⊢ ( 𝑅 ∈ NrmRing → ( invr ‘ 𝑅 ) ∈ ( ( ( TopOpen ‘ 𝑅 ) ↾t ( Unit ‘ 𝑅 ) ) Cn ( ( TopOpen ‘ 𝑅 ) ↾t ( Unit ‘ 𝑅 ) ) ) )
21 20 adantr ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) → ( invr ‘ 𝑅 ) ∈ ( ( ( TopOpen ‘ 𝑅 ) ↾t ( Unit ‘ 𝑅 ) ) Cn ( ( TopOpen ‘ 𝑅 ) ↾t ( Unit ‘ 𝑅 ) ) ) )
22 10 19 mgptopn ⊢ ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ ( mulGrp ‘ 𝑅 ) )
23 7 22 resstopn ⊢ ( ( TopOpen ‘ 𝑅 ) ↾t ( Unit ‘ 𝑅 ) ) = ( TopOpen ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) )
24 6 7 18 invrfval ⊢ ( invr ‘ 𝑅 ) = ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) )
25 23 24 istgp ⊢ ( ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) ∈ TopGrp ↔ ( ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) ∈ Grp ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) ∈ TopMnd ∧ ( invr ‘ 𝑅 ) ∈ ( ( ( TopOpen ‘ 𝑅 ) ↾t ( Unit ‘ 𝑅 ) ) Cn ( ( TopOpen ‘ 𝑅 ) ↾t ( Unit ‘ 𝑅 ) ) ) ) )
26 9 16 21 25 syl3anbrc ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) → ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) ∈ TopGrp )
27 10 6 istdrg ⊢ ( 𝑅 ∈ TopDRing ↔ ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) ∈ TopGrp ) )
28 2 3 26 27 syl3anbrc ⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) → 𝑅 ∈ TopDRing )