Theorem asclmulg

Description: Apply group multiplication to the algebra scalars. (Contributed by Thierry Arnoux, 24-Jul-2024)

	Ref	Expression
Hypotheses	asclmulg.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	asclmulg.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	asclmulg.k	$$⊢K={\mathrm{Base}}_F$$
	asclmulg.m	$$⊢\underset{\dot{}}{\times }={\cdot }_W$$
	asclmulg.t	$$⊢\underset{\dot{}}{\ast }={\cdot }_F$$
Assertion	asclmulg	$$⊢\left(W\in \mathrm{AssAlg}\wedge N\in {\mathbb{N}}_0\wedge X\in K\right)\to A\left(N\underset{\dot{}}{\ast }X\right)=N\underset{\dot{}}{\times }A\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		asclmulg.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
2		asclmulg.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		asclmulg.k	$$⊢K={\mathrm{Base}}_F$$
4		asclmulg.m	$$⊢\underset{\dot{}}{\times }={\cdot }_W$$
5		asclmulg.t	$$⊢\underset{\dot{}}{\ast }={\cdot }_F$$
6		assalmod	$$⊢W\in \mathrm{AssAlg}\to W\in \mathrm{LMod}$$
7	6	3ad2ant1	$$⊢\left(W\in \mathrm{AssAlg}\wedge N\in {\mathbb{N}}_0\wedge X\in K\right)\to W\in \mathrm{LMod}$$
8		simp3	$$⊢\left(W\in \mathrm{AssAlg}\wedge N\in {\mathbb{N}}_0\wedge X\in K\right)\to X\in K$$
9		simp2	$$⊢\left(W\in \mathrm{AssAlg}\wedge N\in {\mathbb{N}}_0\wedge X\in K\right)\to N\in {\mathbb{N}}_0$$
10		assaring	$$⊢W\in \mathrm{AssAlg}\to W\in \mathrm{Ring}$$
11		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
12		eqid	$$⊢1_W=1_W$$
13	11 12	ringidcl	$$⊢W\in \mathrm{Ring}\to 1_W\in {\mathrm{Base}}_W$$
14	10 13	syl	$$⊢W\in \mathrm{AssAlg}\to 1_W\in {\mathrm{Base}}_W$$
15	14	3ad2ant1	$$⊢\left(W\in \mathrm{AssAlg}\wedge N\in {\mathbb{N}}_0\wedge X\in K\right)\to 1_W\in {\mathrm{Base}}_W$$
16		eqid	$$⊢{\cdot }_W={\cdot }_W$$
17	11 2 16 3 4 5	lmodvsmmulgdi	$$⊢\left(W\in \mathrm{LMod}\wedge \left(X\in K\wedge N\in {\mathbb{N}}_0\wedge 1_W\in {\mathrm{Base}}_W\right)\right)\to N\underset{\dot{}}{\times }\left(X{\cdot }_W{1}_W\right)=\left(N\underset{\dot{}}{\ast }X\right){\cdot }_W{1}_W$$
18	7 8 9 15 17	syl13anc	$$⊢\left(W\in \mathrm{AssAlg}\wedge N\in {\mathbb{N}}_0\wedge X\in K\right)\to N\underset{\dot{}}{\times }\left(X{\cdot }_W{1}_W\right)=\left(N\underset{\dot{}}{\ast }X\right){\cdot }_W{1}_W$$
19	1 2 3 16 12	asclval	$$⊢X\in K\to A\left(X\right)=X{\cdot }_W{1}_W$$
20	8 19	syl	$$⊢\left(W\in \mathrm{AssAlg}\wedge N\in {\mathbb{N}}_0\wedge X\in K\right)\to A\left(X\right)=X{\cdot }_W{1}_W$$
21	20	oveq2d	$$⊢\left(W\in \mathrm{AssAlg}\wedge N\in {\mathbb{N}}_0\wedge X\in K\right)\to N\underset{\dot{}}{\times }A\left(X\right)=N\underset{\dot{}}{\times }\left(X{\cdot }_W{1}_W\right)$$
22	2	assasca	$$⊢W\in \mathrm{AssAlg}\to F\in \mathrm{CRing}$$
23	22	3ad2ant1	$$⊢\left(W\in \mathrm{AssAlg}\wedge N\in {\mathbb{N}}_0\wedge X\in K\right)\to F\in \mathrm{CRing}$$
24	23	crnggrpd	$$⊢\left(W\in \mathrm{AssAlg}\wedge N\in {\mathbb{N}}_0\wedge X\in K\right)\to F\in \mathrm{Grp}$$
25	9	nn0zd	$$⊢\left(W\in \mathrm{AssAlg}\wedge N\in {\mathbb{N}}_0\wedge X\in K\right)\to N\in \mathbb{Z}$$
26	3 5 24 25 8	mulgcld	$$⊢\left(W\in \mathrm{AssAlg}\wedge N\in {\mathbb{N}}_0\wedge X\in K\right)\to N\underset{\dot{}}{\ast }X\in K$$
27	1 2 3 16 12	asclval	$$⊢N\underset{\dot{}}{\ast }X\in K\to A\left(N\underset{\dot{}}{\ast }X\right)=\left(N\underset{\dot{}}{\ast }X\right){\cdot }_W{1}_W$$
28	26 27	syl	$$⊢\left(W\in \mathrm{AssAlg}\wedge N\in {\mathbb{N}}_0\wedge X\in K\right)\to A\left(N\underset{\dot{}}{\ast }X\right)=\left(N\underset{\dot{}}{\ast }X\right){\cdot }_W{1}_W$$
29	18 21 28	3eqtr4rd	$$⊢\left(W\in \mathrm{AssAlg}\wedge N\in {\mathbb{N}}_0\wedge X\in K\right)\to A\left(N\underset{\dot{}}{\ast }X\right)=N\underset{\dot{}}{\times }A\left(X\right)$$