nrgtrg - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > nrgtrg		Structured version Visualization version GIF version

Theorem nrgtrg 24945

Description: A normed ring is a topological ring. (Contributed by Mario Carneiro, 4-Oct-2015.) (Proof shortened by AV, 31-Oct-2024.)

**Assertion**
Ref	Expression
nrgtrg	⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopRing)

**Proof of Theorem nrgtrg**
Step	Hyp	Ref	Expression
1		nrgtgp 24927	. 2 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopGrp)
2		nrgring 24918	. 2 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring)
3		eqid 2760	. . . . 5 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
4	3	ringmgp 20401	. . . 4 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
5	2, 4	syl 18	. . 3 ⊢ (𝑅 ∈ NrmRing → (mulGrp‘𝑅) ∈ Mnd)
6		tgptps 24335	. . . . . 6 ⊢ (𝑅 ∈ TopGrp → 𝑅 ∈ TopSp)
7	1, 6	syl 18	. . . . 5 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopSp)
8		eqid 2760	. . . . . 6 ⊢ (Base‘𝑅) = (Base‘𝑅)
9		eqid 2760	. . . . . 6 ⊢ (TopOpen‘𝑅) = (TopOpen‘𝑅)
10	8, 9	istps 23188	. . . . 5 ⊢ (𝑅 ∈ TopSp ↔ (TopOpen‘𝑅) ∈ (TopOn‘(Base‘𝑅)))
11	7, 10	sylib 221	. . . 4 ⊢ (𝑅 ∈ NrmRing → (TopOpen‘𝑅) ∈ (TopOn‘(Base‘𝑅)))
12	3, 8	mgpbas 20301	. . . . 5 ⊢ (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
13	3, 9	mgptopn 20304	. . . . 5 ⊢ (TopOpen‘𝑅) = (TopOpen‘(mulGrp‘𝑅))
14	12, 13	istps 23188	. . . 4 ⊢ ((mulGrp‘𝑅) ∈ TopSp ↔ (TopOpen‘𝑅) ∈ (TopOn‘(Base‘𝑅)))
15	11, 14	sylibr 237	. . 3 ⊢ (𝑅 ∈ NrmRing → (mulGrp‘𝑅) ∈ TopSp)
16		rlmnlm 24943	. . . 4 ⊢ (𝑅 ∈ NrmRing → (ringLMod‘𝑅) ∈ NrmMod)
17		rlmsca2 21410	. . . . 5 ⊢ ( I ‘𝑅) = (Scalar‘(ringLMod‘𝑅))
18		rlmscaf 21418	. . . . 5 ⊢ (+_𝑓‘(mulGrp‘𝑅)) = ( ·_sf ‘(ringLMod‘𝑅))
19		rlmtopn 21412	. . . . 5 ⊢ (TopOpen‘𝑅) = (TopOpen‘(ringLMod‘𝑅))
20		baseid 17326	. . . . . . . . 9 ⊢ Base = Slot (Base‘ndx)
21	20, 8	strfvi 17304	. . . . . . . 8 ⊢ (Base‘𝑅) = (Base‘( I ‘𝑅))
22	21	a1i 11	. . . . . . 7 ⊢ (⊤ → (Base‘𝑅) = (Base‘( I ‘𝑅)))
23		tsetid 17460	. . . . . . . . 9 ⊢ TopSet = Slot (TopSet‘ndx)
24		eqid 2760	. . . . . . . . 9 ⊢ (TopSet‘𝑅) = (TopSet‘𝑅)
25	23, 24	strfvi 17304	. . . . . . . 8 ⊢ (TopSet‘𝑅) = (TopSet‘( I ‘𝑅))
26	25	a1i 11	. . . . . . 7 ⊢ (⊤ → (TopSet‘𝑅) = (TopSet‘( I ‘𝑅)))
27	22, 26	topnpropd 17543	. . . . . 6 ⊢ (⊤ → (TopOpen‘𝑅) = (TopOpen‘( I ‘𝑅)))
28	27	mptru 1577	. . . . 5 ⊢ (TopOpen‘𝑅) = (TopOpen‘( I ‘𝑅))
29	17, 18, 19, 28	nlmvscn 24942	. . . 4 ⊢ ((ringLMod‘𝑅) ∈ NrmMod → (+_𝑓‘(mulGrp‘𝑅)) ∈ (((TopOpen‘𝑅) ×_t (TopOpen‘𝑅)) Cn (TopOpen‘𝑅)))
30	16, 29	syl 18	. . 3 ⊢ (𝑅 ∈ NrmRing → (+_𝑓‘(mulGrp‘𝑅)) ∈ (((TopOpen‘𝑅) ×_t (TopOpen‘𝑅)) Cn (TopOpen‘𝑅)))
31		eqid 2760	. . . 4 ⊢ (+_𝑓‘(mulGrp‘𝑅)) = (+_𝑓‘(mulGrp‘𝑅))
32	31, 13	istmd 24329	. . 3 ⊢ ((mulGrp‘𝑅) ∈ TopMnd ↔ ((mulGrp‘𝑅) ∈ Mnd ∧ (mulGrp‘𝑅) ∈ TopSp ∧ (+_𝑓‘(mulGrp‘𝑅)) ∈ (((TopOpen‘𝑅) ×_t (TopOpen‘𝑅)) Cn (TopOpen‘𝑅))))
33	5, 15, 30, 32	syl3anbrc 1362	. 2 ⊢ (𝑅 ∈ NrmRing → (mulGrp‘𝑅) ∈ TopMnd)
34	3	istrg 24419	. 2 ⊢ (𝑅 ∈ TopRing ↔ (𝑅 ∈ TopGrp ∧ 𝑅 ∈ Ring ∧ (mulGrp‘𝑅) ∈ TopMnd))
35	1, 2, 33, 34	syl3anbrc 1362	1 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ TopRing)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1570 ⊤wtru 1571 ∈ wcel 2145 I cid 5549 ‘cfv 6534 (class class class)co 7415 ndxcnx 17307 Basecbs 17323 TopSetcts 17370 TopOpenctopn 17528 +_𝑓cplusf 18749 Mndcmnd 18859 mulGrpcmgp 20296 Ringcrg 20395 ringLModcrglmod 21383 TopOnctopon 23164 TopSpctps 23186 Cn ccn 23478 ×_t ctx 23815 TopMndctmd 24325 TopGrpctgp 24326 TopRingctrg 24411 NrmRingcnrg 24834 NrmModcnlm 24835

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7738 ax-cnex 11202 ax-resscn 11203 ax-1cn 11204 ax-icn 11205 ax-addcl 11206 ax-addrcl 11207 ax-mulcl 11208 ax-mulrcl 11209 ax-mulcom 11210 ax-addass 11211 ax-mulass 11212 ax-distr 11213 ax-i2m1 11214 ax-1ne0 11215 ax-1rid 11216 ax-rnegex 11217 ax-rrecex 11218 ax-cnre 11219 ax-pre-lttri 11220 ax-pre-lttrn 11221 ax-pre-ltadd 11222 ax-pre-mulgt0 11223 ax-pre-sup 11224

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6300 df-ord 6361 df-on 6362 df-lim 6363 df-suc 6364 df-iota 6490 df-fun 6536 df-fn 6537 df-f 6538 df-f1 6539 df-fo 6540 df-f1o 6541 df-fv 6542 df-isom 6543 df-riota 7372 df-ov 7418 df-oprab 7419 df-mpo 7420 df-of 7680 df-om 7865 df-1st 7988 df-2nd 7989 df-supp 8161 df-frecs 8282 df-wrecs 8313 df-recs 8362 df-rdg 8401 df-1o 8459 df-2o 8460 df-er 8700 df-map 8832 df-ixp 8909 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-fsupp 9336 df-fi 9385 df-sup 9416 df-inf 9417 df-oi 9486 df-card 9966 df-pnf 11291 df-mnf 11292 df-xr 11293 df-ltxr 11294 df-le 11295 df-sub 11489 df-neg 11490 df-div 11918 df-nn 12280 df-2 12349 df-3 12350 df-4 12351 df-5 12352 df-6 12353 df-7 12354 df-8 12355 df-9 12356 df-n0 12551 df-z 12638 df-dec 12759 df-uz 12910 df-q 13020 df-rp 13065 df-xneg 13185 df-xadd 13186 df-xmul 13187 df-ico 13426 df-icc 13427 df-fz 13584 df-fzo 13732 df-seq 14088 df-exp 14148 df-hash 14417 df-cj 15208 df-re 15209 df-im 15210 df-sqrt 15344 df-abs 15345 df-struct 17261 df-sets 17278 df-slot 17296 df-ndx 17308 df-base 17324 df-ress 17345 df-plusg 17377 df-mulr 17378 df-sca 17380 df-vsca 17381 df-ip 17382 df-tset 17383 df-ple 17384 df-ds 17386 df-hom 17388 df-cco 17389 df-rest 17529 df-topn 17530 df-0g 17548 df-gsum 17549 df-topgen 17550 df-pt 17551 df-prds 17554 df-xrs 17610 df-qtop 17615 df-imas 17616 df-xps 17618 df-mre 17692 df-mrc 17693 df-acs 17695 df-plusf 18751 df-mgm 18752 df-sgrp 18844 df-mnd 18860 df-submnd 18915 df-grp 19083 df-minusg 19084 df-sbg 19085 df-mulg 19214 df-subg 19269 df-cntz 19467 df-cmn 19932 df-abl 19933 df-mgp 20297 df-rng 20311 df-ur 20344 df-ring 20397 df-subrng 20734 df-subrg 20758 df-abv 21002 df-lmod 21073 df-scaf 21074 df-sra 21384 df-rgmod 21385 df-psmet 21606 df-xmet 21607 df-met 21608 df-bl 21609 df-mopn 21610 df-top 23148 df-topon 23165 df-topsp 23187 df-bases 23200 df-cn 23481 df-cnp 23482 df-tx 23817 df-hmeo 24010 df-tmd 24327 df-tgp 24328 df-trg 24415 df-xms 24575 df-ms 24576 df-tms 24577 df-nm 24837 df-ngp 24838 df-nrg 24840 df-nlm 24841

This theorem is used by: nrgtdrg 24948 nlmtlm 24949 iistmd 34442 qqhcn 34531

W3C validator