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	⊢ 𝐴 = ( 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		assaring	⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
7	4 6	syl	⊢ ( 𝜑 → 𝑊 ∈ Ring )
8		assalmod	⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
9	4 8	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
10		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
11	1 2 7 9 3 10	asclf	⊢ ( 𝜑 → 𝐴 : 𝐵 ⟶ ( Base ‘ 𝑊 ) )
12	11 5	ffvelcdmd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐶 ) ∈ ( Base ‘ 𝑊 ) )