assaring

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

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

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{W} = {Base}_{W}$
2		eqid	$⊢ Scalar (W) = Scalar (W)$
3		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
4		eqid	$⊢ \cdot_{W} = \cdot_{W}$
5		eqid	$⊢ \cdot_{W} = \cdot_{W}$
6	1 2 3 4 5	isassa	$⊢ W \in AssAlg \leftrightarrow ((W \in LMod \land W \in Ring) \land \forall z \in {Base}_{Scalar (W)} \forall x \in {Base}_{W} \forall y \in {Base}_{W} ((z \cdot_{W} x) \cdot_{W} y = z \cdot_{W} (x \cdot_{W} y) \land x \cdot_{W} (z \cdot_{W} y) = z \cdot_{W} (x \cdot_{W} y)))$
7	6	simplbi	$⊢ W \in AssAlg \to (W \in LMod \land W \in Ring)$
8	7	simprd	$⊢ W \in AssAlg \to W \in Ring$

Metamath Proof Explorer