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=subringAlgWS
srapart.s φSBaseW
Assertion srabase φBaseW=BaseA

Proof

Step Hyp Ref Expression
1 srapart.a φA=subringAlgWS
2 srapart.s φSBaseW
3 baseid Base=SlotBasendx
4 scandxnbasendx ScalarndxBasendx
5 vscandxnbasendx ndxBasendx
6 ipndxnbasendx 𝑖ndxBasendx
7 1 2 3 4 5 6 sralem φBaseW=BaseA