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

Proof

Step Hyp Ref Expression
1 srapart.a
 |-  ( ph -> A = ( ( subringAlg ` W ) ` S ) )
2 srapart.s
 |-  ( ph -> S C_ ( Base ` W ) )
3 baseid
 |-  Base = Slot ( Base ` ndx )
4 scandxnbasendx
 |-  ( Scalar ` ndx ) =/= ( Base ` ndx )
5 vscandxnbasendx
 |-  ( .s ` ndx ) =/= ( Base ` ndx )
6 ipndxnbasendx
 |-  ( .i ` ndx ) =/= ( Base ` ndx )
7 1 2 3 4 5 6 sralem
 |-  ( ph -> ( Base ` W ) = ( Base ` A ) )