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 = ( w e. _V |-> ( x e. ( Base ` ( Scalar ` w ) ) |-> ( x ( .s ` w ) ( 1r ` w ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cascl | |- algSc |
|
| 1 | vw | |- w |
|
| 2 | cvv | |- _V |
|
| 3 | vx | |- x |
|
| 4 | cbs | |- Base |
|
| 5 | csca | |- Scalar |
|
| 6 | 1 | cv | |- w |
| 7 | 6 5 | cfv | |- ( Scalar ` w ) |
| 8 | 7 4 | cfv | |- ( Base ` ( Scalar ` w ) ) |
| 9 | 3 | cv | |- x |
| 10 | cvsca | |- .s |
|
| 11 | 6 10 | cfv | |- ( .s ` w ) |
| 12 | cur | |- 1r |
|
| 13 | 6 12 | cfv | |- ( 1r ` w ) |
| 14 | 9 13 11 | co | |- ( x ( .s ` w ) ( 1r ` w ) ) |
| 15 | 3 8 14 | cmpt | |- ( x e. ( Base ` ( Scalar ` w ) ) |-> ( x ( .s ` w ) ( 1r ` w ) ) ) |
| 16 | 1 2 15 | cmpt | |- ( w e. _V |-> ( x e. ( Base ` ( Scalar ` w ) ) |-> ( x ( .s ` w ) ( 1r ` w ) ) ) ) |
| 17 | 0 16 | wceq | |- algSc = ( w e. _V |-> ( x e. ( Base ` ( Scalar ` w ) ) |-> ( x ( .s ` w ) ( 1r ` w ) ) ) ) |