This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sratopn

Description: Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015) (Revised by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Hypotheses srapart.a ⊢ φ → A = subringAlg ⁡ W ⁡ S
srapart.s ⊢ φ → S ⊆ Base W
Assertion sratopn ⊢ φ → TopOpen ⁡ W = TopOpen ⁡ A

Proof

Step Hyp Ref Expression
1 srapart.a ⊢ φ → A = subringAlg ⁡ W ⁡ S
2 srapart.s ⊢ φ → S ⊆ Base W
3 1 2 srabase ⊢ φ → Base W = Base A
4 1 2 sratset ⊢ φ → TopSet ⁡ W = TopSet ⁡ A
5 3 4 topnpropd ⊢ φ → TopOpen ⁡ W = TopOpen ⁡ A