Theorem asclelbasALT

Description: Alternate proof of asclelbas . (Contributed by Zhi Wang, 11-Sep-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	asclelbasALT.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	asclelbasALT.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	asclelbasALT.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
	asclelbasALT.w	⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
	asclelbasALT.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
Assertion	asclelbasALT	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐶 ) ∈ ( Base ‘ 𝑊 ) )

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		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 ‘ 𝑊 ) )