Theorem asclcntr

Description: The algebra scalar lifting function maps into the center of the algebra. Equivalently, a lifted scalar is a center 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 )
	asclcntr.m	|- M = ( mulGrp ` W )
Assertion	asclcntr	|- ( ph -> ( A ` C ) e. ( Cntr ` M ) )

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		asclcntr.m	|- M = ( mulGrp ` W )
7		eqid	|- ( Base ` W ) = ( Base ` W )
8		eqid	|- ( Cntr ` M ) = ( Cntr ` M )
9	1 2 3 4 5	asclelbas	|- ( ph -> ( A ` C ) e. ( Base ` W ) )
10	4	adantr	|- ( ( ph /\ x e. ( Base ` W ) ) -> W e. AssAlg )
11	5	adantr	|- ( ( ph /\ x e. ( Base ` W ) ) -> C e. B )
12		simpr	|- ( ( ph /\ x e. ( Base ` W ) ) -> x e. ( Base ` W ) )
13		eqid	|- ( .r ` W ) = ( .r ` W )
14		eqid	|- ( .s ` W ) = ( .s ` W )
15	1 2 3 7 13 14	asclmul1	|- ( ( W e. AssAlg /\ C e. B /\ x e. ( Base ` W ) ) -> ( ( A ` C ) ( .r ` W ) x ) = ( C ( .s ` W ) x ) )
16	1 2 3 7 13 14	asclmul2	|- ( ( W e. AssAlg /\ C e. B /\ x e. ( Base ` W ) ) -> ( x ( .r ` W ) ( A ` C ) ) = ( C ( .s ` W ) x ) )
17	15 16	eqtr4d	|- ( ( W e. AssAlg /\ C e. B /\ x e. ( Base ` W ) ) -> ( ( A ` C ) ( .r ` W ) x ) = ( x ( .r ` W ) ( A ` C ) ) )
18	10 11 12 17	syl3anc	|- ( ( ph /\ x e. ( Base ` W ) ) -> ( ( A ` C ) ( .r ` W ) x ) = ( x ( .r ` W ) ( A ` C ) ) )
19	7 6 8 9 18	elmgpcntrd	|- ( ph -> ( A ` C ) e. ( Cntr ` M ) )