# Metamath Proof Explorer

Description: Sufficient condition for being an associative algebra. (Contributed by Mario Carneiro, 5-Dec-2014)

Ref Expression
Hypotheses isassad.v ${⊢}{\phi }\to {V}={\mathrm{Base}}_{{W}}$
isassad.f ${⊢}{\phi }\to {F}=\mathrm{Scalar}\left({W}\right)$
isassad.b ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{F}}$
isassad.1 ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
isassad.2 ${⊢}{\phi }\to {W}\in \mathrm{Ring}$
isassad.3 ${⊢}{\phi }\to {F}\in \mathrm{CRing}$
Assertion isassad ${⊢}{\phi }\to {W}\in \mathrm{AssAlg}$

### Proof

Step Hyp Ref Expression
1 isassad.v ${⊢}{\phi }\to {V}={\mathrm{Base}}_{{W}}$
2 isassad.f ${⊢}{\phi }\to {F}=\mathrm{Scalar}\left({W}\right)$
3 isassad.b ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{F}}$
6 isassad.1 ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
7 isassad.2 ${⊢}{\phi }\to {W}\in \mathrm{Ring}$
8 isassad.3 ${⊢}{\phi }\to {F}\in \mathrm{CRing}$
11 2 8 eqeltrrd ${⊢}{\phi }\to \mathrm{Scalar}\left({W}\right)\in \mathrm{CRing}$
12 6 7 11 3jca ${⊢}{\phi }\to \left({W}\in \mathrm{LMod}\wedge {W}\in \mathrm{Ring}\wedge \mathrm{Scalar}\left({W}\right)\in \mathrm{CRing}\right)$
13 9 10 jca
14 13 ralrimivvva
15 2 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{F}}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
16 3 15 eqtrd ${⊢}{\phi }\to {B}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
17 4 oveqd
18 eqidd ${⊢}{\phi }\to {y}={y}$
19 5 17 18 oveq123d
20 eqidd ${⊢}{\phi }\to {r}={r}$
21 5 oveqd
22 4 20 21 oveq123d
23 19 22 eqeq12d
24 eqidd ${⊢}{\phi }\to {x}={x}$
25 4 oveqd
26 5 24 25 oveq123d
27 26 22 eqeq12d
28 23 27 anbi12d
29 1 28 raleqbidv
30 1 29 raleqbidv
31 16 30 raleqbidv
32 14 31 mpbid ${⊢}{\phi }\to \forall {r}\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({r}{\cdot }_{{W}}{x}\right){\cdot }_{{W}}{y}={r}{\cdot }_{{W}}\left({x}{\cdot }_{{W}}{y}\right)\wedge {x}{\cdot }_{{W}}\left({r}{\cdot }_{{W}}{y}\right)={r}{\cdot }_{{W}}\left({x}{\cdot }_{{W}}{y}\right)\right)$
33 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
34 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
35 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
36 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
37 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
38 33 34 35 36 37 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 {r}\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({r}{\cdot }_{{W}}{x}\right){\cdot }_{{W}}{y}={r}{\cdot }_{{W}}\left({x}{\cdot }_{{W}}{y}\right)\wedge {x}{\cdot }_{{W}}\left({r}{\cdot }_{{W}}{y}\right)={r}{\cdot }_{{W}}\left({x}{\cdot }_{{W}}{y}\right)\right)\right)$
39 12 32 38 sylanbrc ${⊢}{\phi }\to {W}\in \mathrm{AssAlg}$