Theorem assamulgscm

Description: Exponentiation of a scalar multiplication in an associative algebra: ( a .x. X ) ^ N = ( a ^ N ) .X. ( X ^ N ) . (Contributed by AV, 26-Aug-2019)

	Ref	Expression
Hypotheses	assamulgscm.v	$$⊢V={\mathrm{Base}}_W$$
	assamulgscm.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	assamulgscm.b	$$⊢B={\mathrm{Base}}_F$$
	assamulgscm.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	assamulgscm.g	$$⊢G={\mathrm{mulGrp}}_F$$
	assamulgscm.p	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
	assamulgscm.h	$$⊢H={\mathrm{mulGrp}}_W$$
	assamulgscm.e	$$⊢E={\cdot }_H$$
Assertion	assamulgscm	$$⊢\left(W\in \mathrm{AssAlg}\wedge \left(N\in {\mathbb{N}}_0\wedge A\in B\wedge X\in V\right)\right)\to NE\left(A\underset{\dot{}}{·}X\right)=\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(NEX\right)$$

Proof

Step	Hyp	Ref	Expression
1		assamulgscm.v	$$⊢V={\mathrm{Base}}_W$$
2		assamulgscm.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		assamulgscm.b	$$⊢B={\mathrm{Base}}_F$$
4		assamulgscm.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
5		assamulgscm.g	$$⊢G={\mathrm{mulGrp}}_F$$
6		assamulgscm.p	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
7		assamulgscm.h	$$⊢H={\mathrm{mulGrp}}_W$$
8		assamulgscm.e	$$⊢E={\cdot }_H$$
9		oveq1	$$⊢x=0\to xE\left(A\underset{\dot{}}{·}X\right)=0E\left(A\underset{\dot{}}{·}X\right)$$
10		oveq1	$$⊢x=0\to x\underset{\dot{}}{\times }A=0\underset{\dot{}}{\times }A$$
11		oveq1	$$⊢x=0\to xEX=0EX$$
12	10 11	oveq12d	$$⊢x=0\to \left(x\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(xEX\right)=\left(0\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(0EX\right)$$
13	9 12	eqeq12d	$$⊢x=0\to \left(xE\left(A\underset{\dot{}}{·}X\right)=\left(x\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(xEX\right)\leftrightarrow 0E\left(A\underset{\dot{}}{·}X\right)=\left(0\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(0EX\right)\right)$$
14	13	imbi2d	$$⊢x=0\to \left(\left(\left(\left(A\in B\wedge X\in V\right)\wedge W\in \mathrm{AssAlg}\right)\to xE\left(A\underset{\dot{}}{·}X\right)=\left(x\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(xEX\right)\right)\leftrightarrow \left(\left(\left(A\in B\wedge X\in V\right)\wedge W\in \mathrm{AssAlg}\right)\to 0E\left(A\underset{\dot{}}{·}X\right)=\left(0\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(0EX\right)\right)\right)$$
15		oveq1	$$⊢x=y\to xE\left(A\underset{\dot{}}{·}X\right)=yE\left(A\underset{\dot{}}{·}X\right)$$
16		oveq1	$$⊢x=y\to x\underset{\dot{}}{\times }A=y\underset{\dot{}}{\times }A$$
17		oveq1	$$⊢x=y\to xEX=yEX$$
18	16 17	oveq12d	$$⊢x=y\to \left(x\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(xEX\right)=\left(y\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(yEX\right)$$
19	15 18	eqeq12d	$$⊢x=y\to \left(xE\left(A\underset{\dot{}}{·}X\right)=\left(x\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(xEX\right)\leftrightarrow yE\left(A\underset{\dot{}}{·}X\right)=\left(y\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(yEX\right)\right)$$
20	19	imbi2d	$$⊢x=y\to \left(\left(\left(\left(A\in B\wedge X\in V\right)\wedge W\in \mathrm{AssAlg}\right)\to xE\left(A\underset{\dot{}}{·}X\right)=\left(x\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(xEX\right)\right)\leftrightarrow \left(\left(\left(A\in B\wedge X\in V\right)\wedge W\in \mathrm{AssAlg}\right)\to yE\left(A\underset{\dot{}}{·}X\right)=\left(y\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(yEX\right)\right)\right)$$
21		oveq1	$$⊢x=y+1\to xE\left(A\underset{\dot{}}{·}X\right)=\left(y+1\right)E\left(A\underset{\dot{}}{·}X\right)$$
22		oveq1	$$⊢x=y+1\to x\underset{\dot{}}{\times }A=\left(y+1\right)\underset{\dot{}}{\times }A$$
23		oveq1	$$⊢x=y+1\to xEX=\left(y+1\right)EX$$
24	22 23	oveq12d	$$⊢x=y+1\to \left(x\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(xEX\right)=\left(\left(y+1\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(\left(y+1\right)EX\right)$$
25	21 24	eqeq12d	$$⊢x=y+1\to \left(xE\left(A\underset{\dot{}}{·}X\right)=\left(x\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(xEX\right)\leftrightarrow \left(y+1\right)E\left(A\underset{\dot{}}{·}X\right)=\left(\left(y+1\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(\left(y+1\right)EX\right)\right)$$
26	25	imbi2d	$$⊢x=y+1\to \left(\left(\left(\left(A\in B\wedge X\in V\right)\wedge W\in \mathrm{AssAlg}\right)\to xE\left(A\underset{\dot{}}{·}X\right)=\left(x\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(xEX\right)\right)\leftrightarrow \left(\left(\left(A\in B\wedge X\in V\right)\wedge W\in \mathrm{AssAlg}\right)\to \left(y+1\right)E\left(A\underset{\dot{}}{·}X\right)=\left(\left(y+1\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(\left(y+1\right)EX\right)\right)\right)$$
27		oveq1	$$⊢x=N\to xE\left(A\underset{\dot{}}{·}X\right)=NE\left(A\underset{\dot{}}{·}X\right)$$
28		oveq1	$$⊢x=N\to x\underset{\dot{}}{\times }A=N\underset{\dot{}}{\times }A$$
29		oveq1	$$⊢x=N\to xEX=NEX$$
30	28 29	oveq12d	$$⊢x=N\to \left(x\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(xEX\right)=\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(NEX\right)$$
31	27 30	eqeq12d	$$⊢x=N\to \left(xE\left(A\underset{\dot{}}{·}X\right)=\left(x\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(xEX\right)\leftrightarrow NE\left(A\underset{\dot{}}{·}X\right)=\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(NEX\right)\right)$$
32	31	imbi2d	$$⊢x=N\to \left(\left(\left(\left(A\in B\wedge X\in V\right)\wedge W\in \mathrm{AssAlg}\right)\to xE\left(A\underset{\dot{}}{·}X\right)=\left(x\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(xEX\right)\right)\leftrightarrow \left(\left(\left(A\in B\wedge X\in V\right)\wedge W\in \mathrm{AssAlg}\right)\to NE\left(A\underset{\dot{}}{·}X\right)=\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(NEX\right)\right)\right)$$
33	1 2 3 4 5 6 7 8	assamulgscmlem1	$$⊢\left(\left(A\in B\wedge X\in V\right)\wedge W\in \mathrm{AssAlg}\right)\to 0E\left(A\underset{\dot{}}{·}X\right)=\left(0\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(0EX\right)$$
34	1 2 3 4 5 6 7 8	assamulgscmlem2	$$⊢y\in {\mathbb{N}}_0\to \left(\left(\left(A\in B\wedge X\in V\right)\wedge W\in \mathrm{AssAlg}\right)\to \left(yE\left(A\underset{\dot{}}{·}X\right)=\left(y\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(yEX\right)\to \left(y+1\right)E\left(A\underset{\dot{}}{·}X\right)=\left(\left(y+1\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(\left(y+1\right)EX\right)\right)\right)$$
35	34	a2d	$$⊢y\in {\mathbb{N}}_0\to \left(\left(\left(\left(A\in B\wedge X\in V\right)\wedge W\in \mathrm{AssAlg}\right)\to yE\left(A\underset{\dot{}}{·}X\right)=\left(y\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(yEX\right)\right)\to \left(\left(\left(A\in B\wedge X\in V\right)\wedge W\in \mathrm{AssAlg}\right)\to \left(y+1\right)E\left(A\underset{\dot{}}{·}X\right)=\left(\left(y+1\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(\left(y+1\right)EX\right)\right)\right)$$
36	14 20 26 32 33 35	nn0ind	$$⊢N\in {\mathbb{N}}_0\to \left(\left(\left(A\in B\wedge X\in V\right)\wedge W\in \mathrm{AssAlg}\right)\to NE\left(A\underset{\dot{}}{·}X\right)=\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(NEX\right)\right)$$
37	36	exp4c	$$⊢N\in {\mathbb{N}}_0\to \left(A\in B\to \left(X\in V\to \left(W\in \mathrm{AssAlg}\to NE\left(A\underset{\dot{}}{·}X\right)=\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(NEX\right)\right)\right)\right)$$
38	37	3imp	$$⊢\left(N\in {\mathbb{N}}_0\wedge A\in B\wedge X\in V\right)\to \left(W\in \mathrm{AssAlg}\to NE\left(A\underset{\dot{}}{·}X\right)=\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(NEX\right)\right)$$
39	38	impcom	$$⊢\left(W\in \mathrm{AssAlg}\wedge \left(N\in {\mathbb{N}}_0\wedge A\in B\wedge X\in V\right)\right)\to NE\left(A\underset{\dot{}}{·}X\right)=\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{·}\left(NEX\right)$$