nrgtrg

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

		Ref	Expression
	Assertion	nrgtrg	$⊢ R \in NrmRing \to R \in TopRing$

Proof

Step	Hyp	Ref	Expression
1		nrgtgp	$⊢ R \in NrmRing \to R \in TopGrp$
2		nrgring	$⊢ R \in NrmRing \to R \in Ring$
3		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
4	3	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
5	2 4	syl	$⊢ R \in NrmRing \to {mulGrp}_{R} \in Mnd$
6		tgptps	$⊢ R \in TopGrp \to R \in TopSp$
7	1 6	syl	$⊢ R \in NrmRing \to R \in TopSp$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9		eqid	$⊢ TopOpen (R) = TopOpen (R)$
10	8 9	istps	$⊢ R \in TopSp \leftrightarrow TopOpen (R) \in TopOn ({Base}_{R})$
11	7 10	sylib	$⊢ R \in NrmRing \to TopOpen (R) \in TopOn ({Base}_{R})$
12	3 8	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
13	3 9	mgptopn	$⊢ TopOpen (R) = TopOpen ({mulGrp}_{R})$
14	12 13	istps	$⊢ {mulGrp}_{R} \in TopSp \leftrightarrow TopOpen (R) \in TopOn ({Base}_{R})$
15	11 14	sylibr	$⊢ R \in NrmRing \to {mulGrp}_{R} \in TopSp$
16		rlmnlm	$⊢ R \in NrmRing \to ringLMod (R) \in NrmMod$
17		rlmsca2	$⊢ I (R) = Scalar (ringLMod (R))$
18		rlmscaf	$⊢ +_{𝑓} ({mulGrp}_{R}) = \cdot_{𝑠𝑓} (ringLMod (R))$
19		rlmtopn	$⊢ TopOpen (R) = TopOpen (ringLMod (R))$
20		baseid	$⊢ Base = Slot {Base}_{ndx}$
21	20 8	strfvi	$⊢ {Base}_{R} = {Base}_{I (R)}$
22	21	a1i	$⊢ ⊤ \to {Base}_{R} = {Base}_{I (R)}$
23		tsetid	$⊢ TopSet = Slot TopSet (ndx)$
24		eqid	$⊢ TopSet (R) = TopSet (R)$
25	23 24	strfvi	$⊢ TopSet (R) = TopSet (I (R))$
26	25	a1i	$⊢ ⊤ \to TopSet (R) = TopSet (I (R))$
27	22 26	topnpropd	$⊢ ⊤ \to TopOpen (R) = TopOpen (I (R))$
28	27	mptru	$⊢ TopOpen (R) = TopOpen (I (R))$
29	17 18 19 28	nlmvscn	$⊢ ringLMod (R) \in NrmMod \to +_{𝑓} ({mulGrp}_{R}) \in ((TopOpen (R) \times_{t} TopOpen (R)) Cn TopOpen (R))$
30	16 29	syl	$⊢ R \in NrmRing \to +_{𝑓} ({mulGrp}_{R}) \in ((TopOpen (R) \times_{t} TopOpen (R)) Cn TopOpen (R))$
31		eqid	$⊢ +_{𝑓} ({mulGrp}_{R}) = +_{𝑓} ({mulGrp}_{R})$
32	31 13	istmd	$⊢ {mulGrp}_{R} \in TopMnd \leftrightarrow ({mulGrp}_{R} \in Mnd \land {mulGrp}_{R} \in TopSp \land +_{𝑓} ({mulGrp}_{R}) \in ((TopOpen (R) \times_{t} TopOpen (R)) Cn TopOpen (R)))$
33	5 15 30 32	syl3anbrc	$⊢ R \in NrmRing \to {mulGrp}_{R} \in TopMnd$
34	3	istrg	$⊢ R \in TopRing \leftrightarrow (R \in TopGrp \land R \in Ring \land {mulGrp}_{R} \in TopMnd)$
35	1 2 33 34	syl3anbrc	$⊢ R \in NrmRing \to R \in TopRing$

Metamath Proof Explorer

Theorem nrgtrg

Proof