# 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}=\mathrm{Scalar}\left({W}\right)$
Assertion assasca ${⊢}{W}\in \mathrm{AssAlg}\to {F}\in \mathrm{CRing}$

### Proof

Step Hyp Ref Expression
1 assasca.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
2 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
3 eqid ${⊢}{\mathrm{Base}}_{{F}}={\mathrm{Base}}_{{F}}$
4 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
5 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
6 2 1 3 4 5 isassa ${⊢}{W}\in \mathrm{AssAlg}↔\left(\left({W}\in \mathrm{LMod}\wedge {W}\in \mathrm{Ring}\wedge {F}\in \mathrm{CRing}\right)\wedge \forall {z}\in {\mathrm{Base}}_{{F}}\phantom{\rule{.4em}{0ex}}\forall {x}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\left(\left({z}{\cdot }_{{W}}{x}\right){\cdot }_{{W}}{y}={z}{\cdot }_{{W}}\left({x}{\cdot }_{{W}}{y}\right)\wedge {x}{\cdot }_{{W}}\left({z}{\cdot }_{{W}}{y}\right)={z}{\cdot }_{{W}}\left({x}{\cdot }_{{W}}{y}\right)\right)\right)$
7 6 simplbi ${⊢}{W}\in \mathrm{AssAlg}\to \left({W}\in \mathrm{LMod}\wedge {W}\in \mathrm{Ring}\wedge {F}\in \mathrm{CRing}\right)$
8 7 simp3d ${⊢}{W}\in \mathrm{AssAlg}\to {F}\in \mathrm{CRing}$