Theorem asclelbasALT

Description: Alternate proof of asclelbas . (Contributed by Zhi Wang, 11-Sep-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	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$$
Assertion	asclelbasALT	$$⊢\phi \to A\left(C\right)\in {\mathrm{Base}}_W$$

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		eqid	$$⊢{\cdot }_W={\cdot }_W$$
7		eqid	$$⊢1_W=1_W$$
8	1 2 3 6 7	asclval	$$⊢C\in B\to A\left(C\right)=C{\cdot }_W{1}_W$$
9	5 8	syl	$$⊢\phi \to A\left(C\right)=C{\cdot }_W{1}_W$$
10		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
11		assalmod	$$⊢W\in \mathrm{AssAlg}\to W\in \mathrm{LMod}$$
12	4 11	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
13		assaring	$$⊢W\in \mathrm{AssAlg}\to W\in \mathrm{Ring}$$
14	10 7	ringidcl	$$⊢W\in \mathrm{Ring}\to 1_W\in {\mathrm{Base}}_W$$
15	4 13 14	3syl	$$⊢\phi \to 1_W\in {\mathrm{Base}}_W$$
16	10 2 6 3 12 5 15	lmodvscld	$$⊢\phi \to C{\cdot }_W{1}_W\in {\mathrm{Base}}_W$$
17	9 16	eqeltrd	$$⊢\phi \to A\left(C\right)\in {\mathrm{Base}}_W$$