Theorem asclcom

Description: Scalars are commutative after being lifted.

However, the scalars themselves are not necessarily commutative if the algebra is not a faithful module. For example, Let F be the 2 by 2 upper triangular matrix algebra over a commutative ring W . It is provable that F is in general non-commutative. Define scalar multiplication C .x. X as multipying the top-left entry, which is a "vector" element of W , of the "scalar" C , which is now an upper triangular matrix, with the "vector" X e. ( BaseW ) .

Equivalently, the algebra scalar lifting function is not necessarily injective unless the algebra is faithful. Therefore, all "scalar injection" was renamed.

Alternate proof involves assa2ass , assa2ass2 , and asclval , by setting X and Y the multiplicative identity of the algebra.

(Contributed by Zhi Wang, 11-Sep-2025)

	Ref	Expression
Hypotheses	asclelbasALT.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	asclelbasALT.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	asclelbasALT.b	$$⊢B={\mathrm{Base}}_F$$
	asclelbasALT.w	$$⊢\phi \to W\in \mathrm{AssAlg}$$
	asclelbasALT.c	$$⊢\phi \to C\in B$$
	asclcom.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_F$$
	asclcom.d	$$⊢\phi \to D\in B$$
Assertion	asclcom	$$⊢\phi \to A\left(C\underset{\dot{}}{\ast }D\right)=A\left(D\underset{\dot{}}{\ast }C\right)$$

Proof

Step	Hyp	Ref	Expression
1		asclelbasALT.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
2		asclelbasALT.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		asclelbasALT.b	$$⊢B={\mathrm{Base}}_F$$
4		asclelbasALT.w	$$⊢\phi \to W\in \mathrm{AssAlg}$$
5		asclelbasALT.c	$$⊢\phi \to C\in B$$
6		asclcom.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_F$$
7		asclcom.d	$$⊢\phi \to D\in B$$
8	1 2 3 4 7	asclelbas	$$⊢\phi \to A\left(D\right)\in {\mathrm{Base}}_W$$
9		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
10		eqid	$$⊢{\cdot }_W={\cdot }_W$$
11		eqid	$$⊢{\cdot }_W={\cdot }_W$$
12	1 2 3 9 10 11	asclmul1	$$⊢\left(W\in \mathrm{AssAlg}\wedge C\in B\wedge A\left(D\right)\in {\mathrm{Base}}_W\right)\to A\left(C\right){\cdot }_{W}A\left(D\right)=C{\cdot }_{W}A\left(D\right)$$
13	1 2 3 9 10 11	asclmul2	$$⊢\left(W\in \mathrm{AssAlg}\wedge C\in B\wedge A\left(D\right)\in {\mathrm{Base}}_W\right)\to A\left(D\right){\cdot }_{W}A\left(C\right)=C{\cdot }_{W}A\left(D\right)$$
14	12 13	eqtr4d	$$⊢\left(W\in \mathrm{AssAlg}\wedge C\in B\wedge A\left(D\right)\in {\mathrm{Base}}_W\right)\to A\left(C\right){\cdot }_{W}A\left(D\right)=A\left(D\right){\cdot }_{W}A\left(C\right)$$
15	4 5 8 14	syl3anc	$$⊢\phi \to A\left(C\right){\cdot }_{W}A\left(D\right)=A\left(D\right){\cdot }_{W}A\left(C\right)$$
16	1 2 3 10 6	ascldimul	$$⊢\left(W\in \mathrm{AssAlg}\wedge C\in B\wedge D\in B\right)\to A\left(C\underset{\dot{}}{\ast }D\right)=A\left(C\right){\cdot }_{W}A\left(D\right)$$
17	4 5 7 16	syl3anc	$$⊢\phi \to A\left(C\underset{\dot{}}{\ast }D\right)=A\left(C\right){\cdot }_{W}A\left(D\right)$$
18	1 2 3 10 6	ascldimul	$$⊢\left(W\in \mathrm{AssAlg}\wedge D\in B\wedge C\in B\right)\to A\left(D\underset{\dot{}}{\ast }C\right)=A\left(D\right){\cdot }_{W}A\left(C\right)$$
19	4 7 5 18	syl3anc	$$⊢\phi \to A\left(D\underset{\dot{}}{\ast }C\right)=A\left(D\right){\cdot }_{W}A\left(C\right)$$
20	15 17 19	3eqtr4d	$$⊢\phi \to A\left(C\underset{\dot{}}{\ast }D\right)=A\left(D\underset{\dot{}}{\ast }C\right)$$