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}\leftrightarrow \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)}\forall x\in {\mathrm{Base}}_W\forall y\in {\mathrm{Base}}_W\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}$$