Theorem asclelbas

Description: Lifted scalars are in the base set of the algebra. (Contributed by Zhi Wang, 11-Sep-2025) (Proof shortened by Thierry Arnoux, 22-Sep-2025)

	Ref	Expression
Hypotheses	asclelbas.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	asclelbas.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	asclelbas.b	$$⊢B={\mathrm{Base}}_F$$
	asclelbas.w	$$⊢\phi \to W\in \mathrm{AssAlg}$$
	asclelbas.c	$$⊢\phi \to C\in B$$
Assertion	asclelbas	$$⊢\phi \to A\left(C\right)\in {\mathrm{Base}}_W$$

Proof

Step	Hyp	Ref	Expression
1		asclelbas.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
2		asclelbas.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		asclelbas.b	$$⊢B={\mathrm{Base}}_F$$
4		asclelbas.w	$$⊢\phi \to W\in \mathrm{AssAlg}$$
5		asclelbas.c	$$⊢\phi \to C\in B$$
6		assaring	$$⊢W\in \mathrm{AssAlg}\to W\in \mathrm{Ring}$$
7	4 6	syl	$$⊢\phi \to W\in \mathrm{Ring}$$
8		assalmod	$$⊢W\in \mathrm{AssAlg}\to W\in \mathrm{LMod}$$
9	4 8	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
10		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
11	1 2 7 9 3 10	asclf	$$⊢\phi \to A:B⟶{\mathrm{Base}}_W$$
12	11 5	ffvelcdmd	$$⊢\phi \to A\left(C\right)\in {\mathrm{Base}}_W$$