Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ascl Structured version   Unicode version

Definition df-ascl 17366
 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.)
Assertion
Ref Expression
df-ascl algSc Scalar
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-ascl
StepHypRef Expression
1 cascl 17363 . 2 algSc
2 vw . . 3
3 cvv 2967 . . 3
4 vx . . . 4
52cv 1368 . . . . . 6
6 csca 14233 . . . . . 6 Scalar
75, 6cfv 5413 . . . . 5 Scalar
8 cbs 14166 . . . . 5
97, 8cfv 5413 . . . 4 Scalar
104cv 1368 . . . . 5
11 cur 16593 . . . . . 6
125, 11cfv 5413 . . . . 5
13 cvsca 14234 . . . . . 6
145, 13cfv 5413 . . . . 5
1510, 12, 14co 6086 . . . 4
164, 9, 15cmpt 4345 . . 3 Scalar
172, 3, 16cmpt 4345 . 2 Scalar
181, 17wceq 1369 1 algSc Scalar
 Colors of variables: wff setvar class This definition is referenced by:  asclfval  17385
 Copyright terms: Public domain W3C validator