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 = ( 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		eqid	|- ( .s ` W ) = ( .s ` W )
7		eqid	|- ( 1r ` W ) = ( 1r ` W )
8	1 2 3 6 7	asclval	|- ( C e. B -> ( A ` C ) = ( C ( .s ` W ) ( 1r ` W ) ) )
9	5 8	syl	|- ( ph -> ( A ` C ) = ( C ( .s ` W ) ( 1r ` W ) ) )
10		eqid	|- ( Base ` W ) = ( Base ` W )
11		assalmod	|- ( W e. AssAlg -> W e. LMod )
12	4 11	syl	|- ( ph -> W e. LMod )
13		assaring	|- ( W e. AssAlg -> W e. Ring )
14	10 7	ringidcl	|- ( W e. Ring -> ( 1r ` W ) e. ( Base ` W ) )
15	4 13 14	3syl	|- ( ph -> ( 1r ` W ) e. ( Base ` W ) )
16	10 2 6 3 12 5 15	lmodvscld	|- ( ph -> ( C ( .s ` W ) ( 1r ` W ) ) e. ( Base ` W ) )
17	9 16	eqeltrd	|- ( ph -> ( A ` C ) e. ( Base ` W ) )