Metamath Proof Explorer

Theorem assasca

Description: An associative algebra's scalar field is a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Hypothesis assasca.f 
|- F = ( Scalar ` W )
Assertion assasca 
|- ( W e. AssAlg -> F e. CRing )

Proof

Step Hyp Ref Expression
1 assasca.f 
 |-  F = ( Scalar ` W )
2 eqid 
 |-  ( Base ` W ) = ( Base ` W )
3 eqid 
 |-  ( Base ` F ) = ( Base ` F )
4 eqid 
 |-  ( .s ` W ) = ( .s ` W )
5 eqid 
 |-  ( .r ` W ) = ( .r ` W )
6 2 1 3 4 5 isassa 
 |-  ( W e. AssAlg <-> ( ( W e. LMod /\ W e. Ring /\ F e. CRing ) /\ A. z e. ( Base ` F ) A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( ( z ( .s ` W ) x ) ( .r ` W ) y ) = ( z ( .s ` W ) ( x ( .r ` W ) y ) ) /\ ( x ( .r ` W ) ( z ( .s ` W ) y ) ) = ( z ( .s ` W ) ( x ( .r ` W ) y ) ) ) ) )
7 6 simplbi 
 |-  ( W e. AssAlg -> ( W e. LMod /\ W e. Ring /\ F e. CRing ) )
8 7 simp3d 
 |-  ( W e. AssAlg -> F e. CRing )