# Metamath Proof Explorer

## Theorem assaring

Description: An associative algebra is a ring. (Contributed by Mario Carneiro, 5-Dec-2014)

Ref Expression
Assertion assaring ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{Ring}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
2 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
3 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
4 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
5 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
6 1 2 3 4 5 isassa ${⊢}{W}\in \mathrm{AssAlg}↔\left(\left({W}\in \mathrm{LMod}\wedge {W}\in \mathrm{Ring}\wedge \mathrm{Scalar}\left({W}\right)\in \mathrm{CRing}\right)\wedge \forall {z}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\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 \mathrm{Scalar}\left({W}\right)\in \mathrm{CRing}\right)$
8 7 simp2d ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{Ring}$