Theorem isassa

Description: The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	isassa.v	$$⊢V={\mathrm{Base}}_W$$
	isassa.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	isassa.b	$$⊢B={\mathrm{Base}}_F$$
	isassa.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	isassa.t	$$⊢\underset{\dot{}}{\times }={\cdot }_W$$
Assertion	isassa	$$⊢W\in \mathrm{AssAlg}\leftrightarrow \left(\left(W\in \mathrm{LMod}\wedge W\in \mathrm{Ring}\wedge F\in \mathrm{CRing}\right)\wedge \forall r\in B\forall x\in V\forall y\in V\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isassa.v	$$⊢V={\mathrm{Base}}_W$$
2		isassa.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		isassa.b	$$⊢B={\mathrm{Base}}_F$$
4		isassa.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
5		isassa.t	$$⊢\underset{\dot{}}{\times }={\cdot }_W$$
6		fvexd	$$⊢w=W\to \mathrm{Scalar}\left(w\right)\in \mathrm{V}$$
7		fveq2	$$⊢w=W\to \mathrm{Scalar}\left(w\right)=\mathrm{Scalar}\left(W\right)$$
8	7 2	eqtr4di	$$⊢w=W\to \mathrm{Scalar}\left(w\right)=F$$
9		simpr	$$⊢\left(w=W\wedge f=F\right)\to f=F$$
10	9	eleq1d	$$⊢\left(w=W\wedge f=F\right)\to \left(f\in \mathrm{CRing}\leftrightarrow F\in \mathrm{CRing}\right)$$
11	9	fveq2d	$$⊢\left(w=W\wedge f=F\right)\to {\mathrm{Base}}_f={\mathrm{Base}}_F$$
12	11 3	eqtr4di	$$⊢\left(w=W\wedge f=F\right)\to {\mathrm{Base}}_f=B$$
13		fveq2	$$⊢w=W\to {\mathrm{Base}}_w={\mathrm{Base}}_W$$
14	13 1	eqtr4di	$$⊢w=W\to {\mathrm{Base}}_w=V$$
15		fvexd	$$⊢w=W\to {\cdot }_w\in \mathrm{V}$$
16		fvexd	$$⊢\left(w=W\wedge s={\cdot }_w\right)\to {\cdot }_w\in \mathrm{V}$$
17		simpr	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to t={\cdot }_w$$
18		fveq2	$$⊢w=W\to {\cdot }_w={\cdot }_W$$
19	18	ad2antrr	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to {\cdot }_w={\cdot }_W$$
20	19 5	eqtr4di	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to {\cdot }_w=\underset{\dot{}}{\times }$$
21	17 20	eqtrd	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to t=\underset{\dot{}}{\times }$$
22		simplr	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to s={\cdot }_w$$
23		fveq2	$$⊢w=W\to {\cdot }_w={\cdot }_W$$
24	23	ad2antrr	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to {\cdot }_w={\cdot }_W$$
25	24 4	eqtr4di	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to {\cdot }_w=\underset{\dot{}}{·}$$
26	22 25	eqtrd	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to s=\underset{\dot{}}{·}$$
27	26	oveqd	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to rsx=r\underset{\dot{}}{·}x$$
28		eqidd	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to y=y$$
29	21 27 28	oveq123d	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to \left(rsx\right)ty=\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y$$
30		eqidd	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to r=r$$
31	21	oveqd	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to xty=x\underset{\dot{}}{\times }y$$
32	26 30 31	oveq123d	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to rs\left(xty\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)$$
33	29 32	eqeq12d	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to \left(\left(rsx\right)ty=rs\left(xty\right)\leftrightarrow \left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)$$
34		eqidd	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to x=x$$
35	26	oveqd	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to rsy=r\underset{\dot{}}{·}y$$
36	21 34 35	oveq123d	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to xt\left(rsy\right)=x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)$$
37	36 32	eqeq12d	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to \left(xt\left(rsy\right)=rs\left(xty\right)\leftrightarrow x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)$$
38	33 37	anbi12d	$$⊢\left(\left(w=W\wedge s={\cdot }_w\right)\wedge t={\cdot }_w\right)\to \left(\left(\left(rsx\right)ty=rs\left(xty\right)\wedge xt\left(rsy\right)=rs\left(xty\right)\right)\leftrightarrow \left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\right)$$
39	16 38	sbcied	$$⊢\left(w=W\wedge s={\cdot }_w\right)\to \left(\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)\leftrightarrow \left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\right)$$
40	15 39	sbcied	$$⊢w=W\to \left(\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)\leftrightarrow \left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\right)$$
41	14 40	raleqbidv	$$⊢w=W\to \left(\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)\leftrightarrow \forall y\in V\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\right)$$
42	14 41	raleqbidv	$$⊢w=W\to \left(\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)\leftrightarrow \forall x\in V\forall y\in V\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\right)$$
43	42	adantr	$$⊢\left(w=W\wedge f=F\right)\to \left(\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)\leftrightarrow \forall x\in V\forall y\in V\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\right)$$
44	12 43	raleqbidv	$$⊢\left(w=W\wedge f=F\right)\to \left(\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)\leftrightarrow \forall r\in B\forall x\in V\forall y\in V\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\right)$$
45	10 44	anbi12d	$$⊢\left(w=W\wedge f=F\right)\to \left(\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)\leftrightarrow \left(F\in \mathrm{CRing}\wedge \forall r\in B\forall x\in V\forall y\in V\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\right)\right)$$
46	6 8 45	sbcied2	$$⊢w=W\to \left(\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)\leftrightarrow \left(F\in \mathrm{CRing}\wedge \forall r\in B\forall x\in V\forall y\in V\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\right)\right)$$
47		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\}$$
48	46 47	elrab2	$$⊢W\in \mathrm{AssAlg}\leftrightarrow \left(W\in \left(\mathrm{LMod}\cap \mathrm{Ring}\right)\wedge \left(F\in \mathrm{CRing}\wedge \forall r\in B\forall x\in V\forall y\in V\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\right)\right)$$
49		anass	$$⊢\left(\left(W\in \left(\mathrm{LMod}\cap \mathrm{Ring}\right)\wedge F\in \mathrm{CRing}\right)\wedge \forall r\in B\forall x\in V\forall y\in V\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\right)\leftrightarrow \left(W\in \left(\mathrm{LMod}\cap \mathrm{Ring}\right)\wedge \left(F\in \mathrm{CRing}\wedge \forall r\in B\forall x\in V\forall y\in V\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\right)\right)$$
50		elin	$$⊢W\in \left(\mathrm{LMod}\cap \mathrm{Ring}\right)\leftrightarrow \left(W\in \mathrm{LMod}\wedge W\in \mathrm{Ring}\right)$$
51	50	anbi1i	$$⊢\left(W\in \left(\mathrm{LMod}\cap \mathrm{Ring}\right)\wedge F\in \mathrm{CRing}\right)\leftrightarrow \left(\left(W\in \mathrm{LMod}\wedge W\in \mathrm{Ring}\right)\wedge F\in \mathrm{CRing}\right)$$
52		df-3an	$$⊢\left(W\in \mathrm{LMod}\wedge W\in \mathrm{Ring}\wedge F\in \mathrm{CRing}\right)\leftrightarrow \left(\left(W\in \mathrm{LMod}\wedge W\in \mathrm{Ring}\right)\wedge F\in \mathrm{CRing}\right)$$
53	51 52	bitr4i	$$⊢\left(W\in \left(\mathrm{LMod}\cap \mathrm{Ring}\right)\wedge F\in \mathrm{CRing}\right)\leftrightarrow \left(W\in \mathrm{LMod}\wedge W\in \mathrm{Ring}\wedge F\in \mathrm{CRing}\right)$$
54	53	anbi1i	$$⊢\left(\left(W\in \left(\mathrm{LMod}\cap \mathrm{Ring}\right)\wedge F\in \mathrm{CRing}\right)\wedge \forall r\in B\forall x\in V\forall y\in V\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\right)\leftrightarrow \left(\left(W\in \mathrm{LMod}\wedge W\in \mathrm{Ring}\wedge F\in \mathrm{CRing}\right)\wedge \forall r\in B\forall x\in V\forall y\in V\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\right)$$
55	48 49 54	3bitr2i	$$⊢W\in \mathrm{AssAlg}\leftrightarrow \left(\left(W\in \mathrm{LMod}\wedge W\in \mathrm{Ring}\wedge F\in \mathrm{CRing}\right)\wedge \forall r\in B\forall x\in V\forall y\in V\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\right)$$