![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nrgtdrg | Structured version Visualization version GIF version |
Description: A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
Ref | Expression |
---|---|
nrgtdrg | ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → 𝑅 ∈ TopDRing) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nrgtrg 22715 | . . 3 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopRing) | |
2 | 1 | adantr 466 | . 2 ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → 𝑅 ∈ TopRing) |
3 | simpr 471 | . 2 ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → 𝑅 ∈ DivRing) | |
4 | nrgring 22688 | . . . . 5 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring) | |
5 | 4 | adantr 466 | . . . 4 ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → 𝑅 ∈ Ring) |
6 | eqid 2771 | . . . . 5 ⊢ (Unit‘𝑅) = (Unit‘𝑅) | |
7 | eqid 2771 | . . . . 5 ⊢ ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) = ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) | |
8 | 6, 7 | unitgrp 18876 | . . . 4 ⊢ (𝑅 ∈ Ring → ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) ∈ Grp) |
9 | 5, 8 | syl 17 | . . 3 ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) ∈ Grp) |
10 | eqid 2771 | . . . . . 6 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅) | |
11 | 10 | trgtmd 22189 | . . . . 5 ⊢ (𝑅 ∈ TopRing → (mulGrp‘𝑅) ∈ TopMnd) |
12 | 2, 11 | syl 17 | . . . 4 ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → (mulGrp‘𝑅) ∈ TopMnd) |
13 | 6, 10 | unitsubm 18879 | . . . . 5 ⊢ (𝑅 ∈ Ring → (Unit‘𝑅) ∈ (SubMnd‘(mulGrp‘𝑅))) |
14 | 5, 13 | syl 17 | . . . 4 ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → (Unit‘𝑅) ∈ (SubMnd‘(mulGrp‘𝑅))) |
15 | 7 | submtmd 22129 | . . . 4 ⊢ (((mulGrp‘𝑅) ∈ TopMnd ∧ (Unit‘𝑅) ∈ (SubMnd‘(mulGrp‘𝑅))) → ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) ∈ TopMnd) |
16 | 12, 14, 15 | syl2anc 567 | . . 3 ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) ∈ TopMnd) |
17 | eqid 2771 | . . . . 5 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
18 | eqid 2771 | . . . . 5 ⊢ (invr‘𝑅) = (invr‘𝑅) | |
19 | eqid 2771 | . . . . 5 ⊢ (TopOpen‘𝑅) = (TopOpen‘𝑅) | |
20 | 17, 6, 18, 19 | nrginvrcn 22717 | . . . 4 ⊢ (𝑅 ∈ NrmRing → (invr‘𝑅) ∈ (((TopOpen‘𝑅) ↾t (Unit‘𝑅)) Cn ((TopOpen‘𝑅) ↾t (Unit‘𝑅)))) |
21 | 20 | adantr 466 | . . 3 ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → (invr‘𝑅) ∈ (((TopOpen‘𝑅) ↾t (Unit‘𝑅)) Cn ((TopOpen‘𝑅) ↾t (Unit‘𝑅)))) |
22 | 10, 19 | mgptopn 18707 | . . . . 5 ⊢ (TopOpen‘𝑅) = (TopOpen‘(mulGrp‘𝑅)) |
23 | 7, 22 | resstopn 21212 | . . . 4 ⊢ ((TopOpen‘𝑅) ↾t (Unit‘𝑅)) = (TopOpen‘((mulGrp‘𝑅) ↾s (Unit‘𝑅))) |
24 | 6, 7, 18 | invrfval 18882 | . . . 4 ⊢ (invr‘𝑅) = (invg‘((mulGrp‘𝑅) ↾s (Unit‘𝑅))) |
25 | 23, 24 | istgp 22102 | . . 3 ⊢ (((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 1428 | . 2 ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) ∈ TopGrp) |
27 | 10, 6 | istdrg 22190 | . 2 ⊢ (𝑅 ∈ TopDRing ↔ (𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) ∈ TopGrp)) |
28 | 2, 3, 26, 27 | syl3anbrc 1428 | 1 ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) → 𝑅 ∈ TopDRing) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 ∈ wcel 2145 ‘cfv 6032 (class class class)co 6794 Basecbs 16065 ↾s cress 16066 ↾t crest 16290 TopOpenctopn 16291 SubMndcsubmnd 17543 Grpcgrp 17631 mulGrpcmgp 18698 Ringcrg 18756 Unitcui 18848 invrcinvr 18880 DivRingcdr 18958 Cn ccn 21250 TopMndctmd 22095 TopGrpctgp 22096 TopRingctrg 22180 TopDRingctdrg 22181 NrmRingcnrg 22605 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-rep 4905 ax-sep 4916 ax-nul 4924 ax-pow 4975 ax-pr 5035 ax-un 7097 ax-inf2 8703 ax-cnex 10195 ax-resscn 10196 ax-1cn 10197 ax-icn 10198 ax-addcl 10199 ax-addrcl 10200 ax-mulcl 10201 ax-mulrcl 10202 ax-mulcom 10203 ax-addass 10204 ax-mulass 10205 ax-distr 10206 ax-i2m1 10207 ax-1ne0 10208 ax-1rid 10209 ax-rnegex 10210 ax-rrecex 10211 ax-cnre 10212 ax-pre-lttri 10213 ax-pre-lttrn 10214 ax-pre-ltadd 10215 ax-pre-mulgt0 10216 ax-pre-sup 10217 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 829 df-3or 1072 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3353 df-sbc 3589 df-csb 3684 df-dif 3727 df-un 3729 df-in 3731 df-ss 3738 df-pss 3740 df-nul 4065 df-if 4227 df-pw 4300 df-sn 4318 df-pr 4320 df-tp 4322 df-op 4324 df-uni 4576 df-int 4613 df-iun 4657 df-iin 4658 df-br 4788 df-opab 4848 df-mpt 4865 df-tr 4888 df-id 5158 df-eprel 5163 df-po 5171 df-so 5172 df-fr 5209 df-se 5210 df-we 5211 df-xp 5256 df-rel 5257 df-cnv 5258 df-co 5259 df-dm 5260 df-rn 5261 df-res 5262 df-ima 5263 df-pred 5824 df-ord 5870 df-on 5871 df-lim 5872 df-suc 5873 df-iota 5995 df-fun 6034 df-fn 6035 df-f 6036 df-f1 6037 df-fo 6038 df-f1o 6039 df-fv 6040 df-isom 6041 df-riota 6755 df-ov 6797 df-oprab 6798 df-mpt2 6799 df-of 7045 df-om 7214 df-1st 7316 df-2nd 7317 df-supp 7448 df-tpos 7505 df-wrecs 7560 df-recs 7622 df-rdg 7660 df-1o 7714 df-2o 7715 df-oadd 7718 df-er 7897 df-map 8012 df-ixp 8064 df-en 8111 df-dom 8112 df-sdom 8113 df-fin 8114 df-fsupp 8433 df-fi 8474 df-sup 8505 df-inf 8506 df-oi 8572 df-card 8966 df-cda 9193 df-pnf 10279 df-mnf 10280 df-xr 10281 df-ltxr 10282 df-le 10283 df-sub 10471 df-neg 10472 df-div 10888 df-nn 11224 df-2 11282 df-3 11283 df-4 11284 df-5 11285 df-6 11286 df-7 11287 df-8 11288 df-9 11289 df-n0 11496 df-z 11581 df-dec 11697 df-uz 11890 df-q 11993 df-rp 12037 df-xneg 12152 df-xadd 12153 df-xmul 12154 df-ico 12387 df-icc 12388 df-fz 12535 df-fzo 12675 df-seq 13010 df-exp 13069 df-hash 13323 df-cj 14048 df-re 14049 df-im 14050 df-sqrt 14184 df-abs 14185 df-struct 16067 df-ndx 16068 df-slot 16069 df-base 16071 df-sets 16072 df-ress 16073 df-plusg 16163 df-mulr 16164 df-sca 16166 df-vsca 16167 df-ip 16168 df-tset 16169 df-ple 16170 df-ds 16173 df-hom 16175 df-cco 16176 df-rest 16292 df-topn 16293 df-0g 16311 df-gsum 16312 df-topgen 16313 df-pt 16314 df-prds 16317 df-xrs 16371 df-qtop 16376 df-imas 16377 df-xps 16379 df-mre 16455 df-mrc 16456 df-acs 16458 df-plusf 17450 df-mgm 17451 df-sgrp 17493 df-mnd 17504 df-submnd 17545 df-grp 17634 df-minusg 17635 df-sbg 17636 df-mulg 17750 df-subg 17800 df-cntz 17958 df-cmn 18403 df-abl 18404 df-mgp 18699 df-ur 18711 df-ring 18758 df-oppr 18832 df-dvdsr 18850 df-unit 18851 df-invr 18881 df-subrg 18989 df-abv 19028 df-lmod 19076 df-scaf 19077 df-sra 19388 df-rgmod 19389 df-nzr 19474 df-psmet 19954 df-xmet 19955 df-met 19956 df-bl 19957 df-mopn 19958 df-top 20920 df-topon 20937 df-topsp 20959 df-bases 20972 df-cn 21253 df-cnp 21254 df-tx 21587 df-hmeo 21780 df-tmd 22097 df-tgp 22098 df-trg 22184 df-tdrg 22185 df-xms 22346 df-ms 22347 df-tms 22348 df-nm 22608 df-ngp 22609 df-nrg 22611 df-nlm 22612 |
This theorem is referenced by: nvctvc 22725 |
Copyright terms: Public domain | W3C validator |