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
|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )
srapart.s
|- ( ph -> S C_ ( Base ` W ) )
Assertion sratopn
|- ( ph -> ( TopOpen ` W ) = ( TopOpen ` A ) )

Proof

Step Hyp Ref Expression
1 srapart.a
 |-  ( ph -> A = ( ( subringAlg ` W ) ` S ) )
2 srapart.s
 |-  ( ph -> S C_ ( Base ` W ) )
3 1 2 srabase
 |-  ( ph -> ( Base ` W ) = ( Base ` A ) )
4 1 2 sratset
 |-  ( ph -> ( TopSet ` W ) = ( TopSet ` A ) )
5 3 4 topnpropd
 |-  ( ph -> ( TopOpen ` W ) = ( TopOpen ` A ) )