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	asclelbasALT.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	asclelbasALT.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	asclelbasALT.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
	asclelbasALT.w	⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
	asclelbasALT.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
	asclcntr.m	⊢ 𝑀 = ( mulGrp ‘ 𝑊 )
Assertion	asclcntr	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐶 ) ∈ ( Cntr ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		asclelbasALT.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
2		asclelbasALT.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		asclelbasALT.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
4		asclelbasALT.w	⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
5		asclelbasALT.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
6		asclcntr.m	⊢ 𝑀 = ( mulGrp ‘ 𝑊 )
7		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
8		eqid	⊢ ( Cntr ‘ 𝑀 ) = ( Cntr ‘ 𝑀 )
9	1 2 3 4 5	asclelbas	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐶 ) ∈ ( Base ‘ 𝑊 ) )
10	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → 𝑊 ∈ AssAlg )
11	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → 𝐶 ∈ 𝐵 )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
13		eqid	⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
14		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
15	1 2 3 7 13 14	asclmul1	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝐴 ‘ 𝐶 ) ( .r ‘ 𝑊 ) 𝑥 ) = ( 𝐶 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) )
16	1 2 3 7 13 14	asclmul2	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ( .r ‘ 𝑊 ) ( 𝐴 ‘ 𝐶 ) ) = ( 𝐶 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) )
17	15 16	eqtr4d	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝐴 ‘ 𝐶 ) ( .r ‘ 𝑊 ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑊 ) ( 𝐴 ‘ 𝐶 ) ) )
18	10 11 12 17	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝐴 ‘ 𝐶 ) ( .r ‘ 𝑊 ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑊 ) ( 𝐴 ‘ 𝐶 ) ) )
19	7 6 8 9 18	elmgpcntrd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐶 ) ∈ ( Cntr ‘ 𝑀 ) )