Definition df-assa

Description: Definition of an associative algebra. An associative algebra is a set equipped with a left-module structure on a 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) (Revised by SN, 2-Mar-2025)

	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{}}{]}\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\}$$

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		vr	$$setvarr$$
10		cbs	$$class\mathrm{Base}$$
11	8	cv	$$setvarf$$
12	11 10	cfv	$$class{\mathrm{Base}}_f$$
13		vx	$$setvarx$$
14	6 10	cfv	$$class{\mathrm{Base}}_w$$
15		vy	$$setvary$$
16		cvsca	$$class{\cdot }_{𝑠}$$
17	6 16	cfv	$$class{\cdot }_w$$
18		vs	$$setvars$$
19		cmulr	$$class{\cdot }_{𝑟}$$
20	6 19	cfv	$$class{\cdot }_w$$
21		vt	$$setvart$$
22	9	cv	$$setvarr$$
23	18	cv	$$setvars$$
24	13	cv	$$setvarx$$
25	22 24 23	co	$$class\left(rsx\right)$$
26	21	cv	$$setvart$$
27	15	cv	$$setvary$$
28	25 27 26	co	$$class\left(\left(rsx\right)ty\right)$$
29	24 27 26	co	$$class\left(xty\right)$$
30	22 29 23	co	$$class\left(rs\left(xty\right)\right)$$
31	28 30	wceq	$$wff\left(rsx\right)ty=rs\left(xty\right)$$
32	22 27 23	co	$$class\left(rsy\right)$$
33	24 32 26	co	$$class\left(xt\left(rsy\right)\right)$$
34	33 30	wceq	$$wffxt\left(rsy\right)=rs\left(xty\right)$$
35	31 34	wa	$$wff\left(\left(rsx\right)ty=rs\left(xty\right)\wedge xt\left(rsy\right)=rs\left(xty\right)\right)$$
36	35 21 20	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)$$
37	36 18 17	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)$$
38	37 15 14	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)$$
39	38 13 14	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)$$
40	39 9 12	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)$$
41	40 8 7	wsbc	$$wff\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/f\underset{\dot{}}{]}\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)$$
42	41 1 4	crab	$$class\left\{w\in \left(\mathrm{LMod}\cap \mathrm{Ring}\right)|\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/f\underset{\dot{}}{]}\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\}$$
43	0 42	wceq	$$wff\mathrm{AssAlg}=\left\{w\in \left(\mathrm{LMod}\cap \mathrm{Ring}\right)|\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/f\underset{\dot{}}{]}\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\}$$