Metamath Proof Explorer

Theorem assasca

Description: The scalars of an associative algebra form a ring. (Contributed by Mario Carneiro, 7-Jan-2015) (Revised by SN, 2-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 assasca.f 
 |-  F = ( Scalar ` W )
2 assalmod 
 |-  ( W e. AssAlg -> W e. LMod )
3 1 lmodring 
 |-  ( W e. LMod -> F e. Ring )
4 2 3 syl 
 |-  ( W e. AssAlg -> F e. Ring )