Definition df-assa

Description: Definition of an associative algebra. An associative algebra is a set equipped with a left-module structure on a (commutative) ring, coupled with a multiplicative internal operation on the vectors of the module that is associative and distributive for the additive structure of the left-module (so giving the vectors a ring structure) and that is also bilinear under the scalar product. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Assertion	df-assa	$$⊢\mathrm{AssAlg}=\left\{w\in \left(\mathrm{LMod}\cap \mathrm{Ring}\right)|\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/f\underset{\dot{}}{]}\left(f\in \mathrm{CRing}\wedge \forall r\in {\mathrm{Base}}_f\forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_w\underset{\dot{}}{[}{\cdot }_w/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_w/t\underset{\dot{}}{]}\left(\left(rsx\right)ty=rs\left(xty\right)\wedge xt\left(rsy\right)=rs\left(xty\right)\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		casa	$$class\mathrm{AssAlg}$$
1		vw	$$setvarw$$
2		clmod	$$class\mathrm{LMod}$$
3		crg	$$class\mathrm{Ring}$$
4	2 3	cin	$$class\left(\mathrm{LMod}\cap \mathrm{Ring}\right)$$
5		csca	$$class\mathrm{Scalar}$$
6	1	cv	$$setvarw$$
7	6 5	cfv	$$class\mathrm{Scalar}\left(w\right)$$
8		vf	$$setvarf$$
9	8	cv	$$setvarf$$
10		ccrg	$$class\mathrm{CRing}$$
11	9 10	wcel	$$wfff\in \mathrm{CRing}$$
12		vr	$$setvarr$$
13		cbs	$$class\mathrm{Base}$$
14	9 13	cfv	$$class{\mathrm{Base}}_f$$
15		vx	$$setvarx$$
16	6 13	cfv	$$class{\mathrm{Base}}_w$$
17		vy	$$setvary$$
18		cvsca	$$class{\cdot }_{𝑠}$$
19	6 18	cfv	$$class{\cdot }_w$$
20		vs	$$setvars$$
21		cmulr	$$class{\cdot }_{𝑟}$$
22	6 21	cfv	$$class{\cdot }_w$$
23		vt	$$setvart$$
24	12	cv	$$setvarr$$
25	20	cv	$$setvars$$
26	15	cv	$$setvarx$$
27	24 26 25	co	$$class\left(rsx\right)$$
28	23	cv	$$setvart$$
29	17	cv	$$setvary$$
30	27 29 28	co	$$class\left(\left(rsx\right)ty\right)$$
31	26 29 28	co	$$class\left(xty\right)$$
32	24 31 25	co	$$class\left(rs\left(xty\right)\right)$$
33	30 32	wceq	$$wff\left(rsx\right)ty=rs\left(xty\right)$$
34	24 29 25	co	$$class\left(rsy\right)$$
35	26 34 28	co	$$class\left(xt\left(rsy\right)\right)$$
36	35 32	wceq	$$wffxt\left(rsy\right)=rs\left(xty\right)$$
37	33 36	wa	$$wff\left(\left(rsx\right)ty=rs\left(xty\right)\wedge xt\left(rsy\right)=rs\left(xty\right)\right)$$
38	37 23 22	wsbc	$$wff\underset{\dot{}}{[}{\cdot }_w/t\underset{\dot{}}{]}\left(\left(rsx\right)ty=rs\left(xty\right)\wedge xt\left(rsy\right)=rs\left(xty\right)\right)$$
39	38 20 19	wsbc	$$wff\underset{\dot{}}{[}{\cdot }_w/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_w/t\underset{\dot{}}{]}\left(\left(rsx\right)ty=rs\left(xty\right)\wedge xt\left(rsy\right)=rs\left(xty\right)\right)$$
40	39 17 16	wral	$$wff\forall y\in {\mathrm{Base}}_w\underset{\dot{}}{[}{\cdot }_w/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_w/t\underset{\dot{}}{]}\left(\left(rsx\right)ty=rs\left(xty\right)\wedge xt\left(rsy\right)=rs\left(xty\right)\right)$$
41	40 15 16	wral	$$wff\forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_w\underset{\dot{}}{[}{\cdot }_w/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_w/t\underset{\dot{}}{]}\left(\left(rsx\right)ty=rs\left(xty\right)\wedge xt\left(rsy\right)=rs\left(xty\right)\right)$$
42	41 12 14	wral	$$wff\forall r\in {\mathrm{Base}}_f\forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_w\underset{\dot{}}{[}{\cdot }_w/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_w/t\underset{\dot{}}{]}\left(\left(rsx\right)ty=rs\left(xty\right)\wedge xt\left(rsy\right)=rs\left(xty\right)\right)$$
43	11 42	wa	$$wff\left(f\in \mathrm{CRing}\wedge \forall r\in {\mathrm{Base}}_f\forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_w\underset{\dot{}}{[}{\cdot }_w/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_w/t\underset{\dot{}}{]}\left(\left(rsx\right)ty=rs\left(xty\right)\wedge xt\left(rsy\right)=rs\left(xty\right)\right)\right)$$
44	43 8 7	wsbc	$$wff\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/f\underset{\dot{}}{]}\left(f\in \mathrm{CRing}\wedge \forall r\in {\mathrm{Base}}_f\forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_w\underset{\dot{}}{[}{\cdot }_w/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_w/t\underset{\dot{}}{]}\left(\left(rsx\right)ty=rs\left(xty\right)\wedge xt\left(rsy\right)=rs\left(xty\right)\right)\right)$$
45	44 1 4	crab	$$class\left\{w\in \left(\mathrm{LMod}\cap \mathrm{Ring}\right)|\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/f\underset{\dot{}}{]}\left(f\in \mathrm{CRing}\wedge \forall r\in {\mathrm{Base}}_f\forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_w\underset{\dot{}}{[}{\cdot }_w/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_w/t\underset{\dot{}}{]}\left(\left(rsx\right)ty=rs\left(xty\right)\wedge xt\left(rsy\right)=rs\left(xty\right)\right)\right)\right\}$$
46	0 45	wceq	$$wff\mathrm{AssAlg}=\left\{w\in \left(\mathrm{LMod}\cap \mathrm{Ring}\right)|\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/f\underset{\dot{}}{]}\left(f\in \mathrm{CRing}\wedge \forall r\in {\mathrm{Base}}_f\forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_w\underset{\dot{}}{[}{\cdot }_w/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_w/t\underset{\dot{}}{]}\left(\left(rsx\right)ty=rs\left(xty\right)\wedge xt\left(rsy\right)=rs\left(xty\right)\right)\right)\right\}$$