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

Metamath Proof Explorer

Theorem sratset

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

Ref Expression
Hypotheses srapart.a ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
srapart.s ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
Assertion sratset ( 𝜑 → ( TopSet ‘ 𝑊 ) = ( TopSet ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 srapart.a ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
2 srapart.s ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
3 tsetid ⊢ TopSet = Slot ( TopSet ‘ ndx )
4 slotstnscsi ⊢ ( ( TopSet ‘ ndx ) ≠ ( Scalar ‘ ndx ) ∧ ( TopSet ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( TopSet ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) )
5 4 simp1i ⊢ ( TopSet ‘ ndx ) ≠ ( Scalar ‘ ndx )
6 5 necomi ⊢ ( Scalar ‘ ndx ) ≠ ( TopSet ‘ ndx )
7 4 simp2i ⊢ ( TopSet ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
8 7 necomi ⊢ ( ·𝑠 ‘ ndx ) ≠ ( TopSet ‘ ndx )
9 4 simp3i ⊢ ( TopSet ‘ ndx ) ≠ ( ·𝑖 ‘ ndx )
10 9 necomi ⊢ ( ·𝑖 ‘ ndx ) ≠ ( TopSet ‘ ndx )
11 1 2 3 6 8 10 sralem ⊢ ( 𝜑 → ( TopSet ‘ 𝑊 ) = ( TopSet ‘ 𝐴 ) )