This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ A = algSc (W)$
		asclelbas.f	$⊢ F = Scalar (W)$
		asclelbas.b	$⊢ B = {Base}_{F}$
		asclelbas.w	$⊢ φ \to W \in AssAlg$
		asclelbas.c	$⊢ φ \to C \in B$
	Assertion	asclelbas	$⊢ φ \to A (C) \in {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	$⊢ φ \to W \in AssAlg$
5		asclelbas.c	$⊢ φ \to C \in B$
6		assaring	$⊢ W \in AssAlg \to W \in Ring$
7	4 6	syl	$⊢ φ \to W \in Ring$
8		assalmod	$⊢ W \in AssAlg \to W \in LMod$
9	4 8	syl	$⊢ φ \to W \in LMod$
10		eqid	$⊢ {Base}_{W} = {Base}_{W}$
11	1 2 7 9 3 10	asclf	$⊢ φ \to A : B ⟶ {Base}_{W}$
12	11 5	ffvelcdmd	$⊢ φ \to A (C) \in {Base}_{W}$