Definition df-ascl

Description: Every unital algebra contains a canonical homomorphic image of its ring of scalars as scalar multiples of the unit. This names the homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015)

	Ref	Expression
Assertion	df-ascl	⊢ algSc = ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) ( 1r ‘ 𝑤 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cascl	⊢ algSc
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5		csca	⊢ Scalar
6	1	cv	⊢ 𝑤
7	6 5	cfv	⊢ ( Scalar ‘ 𝑤 )
8	7 4	cfv	⊢ ( Base ‘ ( Scalar ‘ 𝑤 ) )
9	3	cv	⊢ 𝑥
10		cvsca	⊢ ·𝑠
11	6 10	cfv	⊢ ( ·𝑠 ‘ 𝑤 )
12		cur	⊢ 1r
13	6 12	cfv	⊢ ( 1r ‘ 𝑤 )
14	9 13 11	co	⊢ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) ( 1r ‘ 𝑤 ) )
15	3 8 14	cmpt	⊢ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) ( 1r ‘ 𝑤 ) ) )
16	1 2 15	cmpt	⊢ ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) ( 1r ‘ 𝑤 ) ) ) )
17	0 16	wceq	⊢ algSc = ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) ( 1r ‘ 𝑤 ) ) ) )