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)

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 df-base
 |-  Base = Slot 1
4 1nn
 |-  1 e. NN
5 1lt5
 |-  1 < 5
6 5 orci
 |-  ( 1 < 5 \/ 8 < 1 )
7 1 2 3 4 6 sralem
 |-  ( ph -> ( Base ` W ) = ( Base ` A ) )