Theorem assalem

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	assalem	$$⊢\left(W\in \mathrm{AssAlg}\wedge \left(A\in B\wedge X\in V\wedge Y\in V\right)\right)\to \left(\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\wedge X\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}Y\right)=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\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	1 2 3 4 5	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)$$
7	6	simprbi	$$⊢W\in \mathrm{AssAlg}\to \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)$$
8		oveq1	$$⊢r=A\to r\underset{\dot{}}{·}x=A\underset{\dot{}}{·}x$$
9	8	oveq1d	$$⊢r=A\to \left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=\left(A\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y$$
10		oveq1	$$⊢r=A\to r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)=A\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)$$
11	9 10	eqeq12d	$$⊢r=A\to \left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\leftrightarrow \left(A\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=A\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)$$
12		oveq1	$$⊢r=A\to r\underset{\dot{}}{·}y=A\underset{\dot{}}{·}y$$
13	12	oveq2d	$$⊢r=A\to x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=x\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}y\right)$$
14	13 10	eqeq12d	$$⊢r=A\to \left(x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\leftrightarrow x\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}y\right)=A\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)$$
15	11 14	anbi12d	$$⊢r=A\to \left(\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)\leftrightarrow \left(\left(A\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=A\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}y\right)=A\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\right)$$
16		oveq2	$$⊢x=X\to A\underset{\dot{}}{·}x=A\underset{\dot{}}{·}X$$
17	16	oveq1d	$$⊢x=X\to \left(A\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }y$$
18		oveq1	$$⊢x=X\to x\underset{\dot{}}{\times }y=X\underset{\dot{}}{\times }y$$
19	18	oveq2d	$$⊢x=X\to A\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }y\right)$$
20	17 19	eqeq12d	$$⊢x=X\to \left(\left(A\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=A\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\leftrightarrow \left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }y=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }y\right)\right)$$
21		oveq1	$$⊢x=X\to x\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}y\right)=X\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}y\right)$$
22	21 19	eqeq12d	$$⊢x=X\to \left(x\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}y\right)=A\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\leftrightarrow X\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}y\right)=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }y\right)\right)$$
23	20 22	anbi12d	$$⊢x=X\to \left(\left(\left(A\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=A\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}y\right)=A\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\leftrightarrow \left(\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }y=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }y\right)\wedge X\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}y\right)=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }y\right)\right)\right)$$
24		oveq2	$$⊢y=Y\to \left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }y=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y$$
25		oveq2	$$⊢y=Y\to X\underset{\dot{}}{\times }y=X\underset{\dot{}}{\times }Y$$
26	25	oveq2d	$$⊢y=Y\to A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }y\right)=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)$$
27	24 26	eqeq12d	$$⊢y=Y\to \left(\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }y=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }y\right)\leftrightarrow \left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)$$
28		oveq2	$$⊢y=Y\to A\underset{\dot{}}{·}y=A\underset{\dot{}}{·}Y$$
29	28	oveq2d	$$⊢y=Y\to X\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}y\right)=X\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}Y\right)$$
30	29 26	eqeq12d	$$⊢y=Y\to \left(X\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}y\right)=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }y\right)\leftrightarrow X\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}Y\right)=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)$$
31	27 30	anbi12d	$$⊢y=Y\to \left(\left(\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }y=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }y\right)\wedge X\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}y\right)=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }y\right)\right)\leftrightarrow \left(\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\wedge X\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}Y\right)=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)\right)$$
32	15 23 31	rspc3v	$$⊢\left(A\in B\wedge X\in V\wedge Y\in V\right)\to \left(\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)\to \left(\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\wedge X\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}Y\right)=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)\right)$$
33	7 32	mpan9	$$⊢\left(W\in \mathrm{AssAlg}\wedge \left(A\in B\wedge X\in V\wedge Y\in V\right)\right)\to \left(\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{\times }Y=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\wedge X\underset{\dot{}}{\times }\left(A\underset{\dot{}}{·}Y\right)=A\underset{\dot{}}{·}\left(X\underset{\dot{}}{\times }Y\right)\right)$$