Metamath Proof Explorer

Theorem 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 ( 𝑅 ∈ NrmRing → 𝑅 ∈ TopRing )

Proof

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