Metamath Proof Explorer

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 ${setvar}{w}$
2 cvv ${class}\mathrm{V}$
3 vx ${setvar}{x}$
4 cbs ${class}\mathrm{Base}$
5 csca ${class}\mathrm{Scalar}$
6 1 cv ${setvar}{w}$
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 ${setvar}{x}$
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)$