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

Metamath Proof Explorer

Theorem srabase

Description: Base set of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 4-Oct-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by AV, 29-Oct-2024)

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

Proof

Step Hyp Ref Expression
1 srapart.a ⊢ φ → A = subringAlg ⁡ W ⁡ S
2 srapart.s ⊢ φ → S ⊆ Base W
3 baseid ⊢ Base = Slot Base ndx
4 scandxnbasendx ⊢ Scalar ⁡ ndx ≠ Base ndx
5 vscandxnbasendx ⊢ ⋅ ndx ≠ Base ndx
6 ipndxnbasendx ⊢ ⋅ 𝑖 ⁡ ndx ≠ Base ndx
7 1 2 3 4 5 6 sralem ⊢ φ → Base W = Base A