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	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	asclelbas.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	asclelbas.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
	asclelbas.w	⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
	asclelbas.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
Assertion	asclelbas	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐶 ) ∈ ( Base ‘ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		asclelbas.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
2		asclelbas.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		asclelbas.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
4		asclelbas.w	⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
5		asclelbas.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
6		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
7		eqid	⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
8	1 2 3 6 7	asclval	⊢ ( 𝐶 ∈ 𝐵 → ( 𝐴 ‘ 𝐶 ) = ( 𝐶 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
9	5 8	syl	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐶 ) = ( 𝐶 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
10		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
11		assalmod	⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
12	4 11	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
13		assaring	⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
14	10 7	ringidcl	⊢ ( 𝑊 ∈ Ring → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
15	4 13 14	3syl	⊢ ( 𝜑 → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
16	10 2 6 3 12 5 15	lmodvscld	⊢ ( 𝜑 → ( 𝐶 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ∈ ( Base ‘ 𝑊 ) )
17	9 16	eqeltrd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐶 ) ∈ ( Base ‘ 𝑊 ) )