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	$$⊢\mathrm{algSc}=\left(w\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}⟼x{\cdot }_w{1}_w\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cascl	$$class\mathrm{algSc}$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5		csca	$$class\mathrm{Scalar}$$
6	1	cv	$$setvarw$$
7	6 5	cfv	$$class\mathrm{Scalar}\left(w\right)$$
8	7 4	cfv	$$class{\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}$$
9	3	cv	$$setvarx$$
10		cvsca	$$class{\cdot }_{𝑠}$$
11	6 10	cfv	$$class{\cdot }_w$$
12		cur	$$class{1}_r$$
13	6 12	cfv	$$class{1}_w$$
14	9 13 11	co	$$class\left(x{\cdot }_w{1}_w\right)$$
15	3 8 14	cmpt	$$class\left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}⟼x{\cdot }_w{1}_w\right)$$
16	1 2 15	cmpt	$$class\left(w\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}⟼x{\cdot }_w{1}_w\right)\right)$$
17	0 16	wceq	$$wff\mathrm{algSc}=\left(w\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}⟼x{\cdot }_w{1}_w\right)\right)$$