Theorem asclelbas

Description: Lifted scalars are in the base set of the algebra. (Contributed by Zhi Wang, 11-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		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$$