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 = ( algSc ` W )
	asclelbas.f	|- F = ( Scalar ` W )
	asclelbas.b	|- B = ( Base ` F )
	asclelbas.w	|- ( ph -> W e. AssAlg )
	asclelbas.c	|- ( ph -> C e. B )
Assertion	asclelbas	|- ( ph -> ( A ` C ) e. ( Base ` W ) )

Proof

Step	Hyp	Ref	Expression
1		asclelbas.a	|- A = ( algSc ` W )
2		asclelbas.f	|- F = ( Scalar ` W )
3		asclelbas.b	|- B = ( Base ` F )
4		asclelbas.w	|- ( ph -> W e. AssAlg )
5		asclelbas.c	|- ( ph -> C e. B )
6		assaring	|- ( W e. AssAlg -> W e. Ring )
7	4 6	syl	|- ( ph -> W e. Ring )
8		assalmod	|- ( W e. AssAlg -> W e. LMod )
9	4 8	syl	|- ( ph -> W e. LMod )
10		eqid	|- ( Base ` W ) = ( Base ` W )
11	1 2 7 9 3 10	asclf	|- ( ph -> A : B --> ( Base ` W ) )
12	11 5	ffvelcdmd	|- ( ph -> ( A ` C ) e. ( Base ` W ) )