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

Definition df-ascl 21277
Description: Every unital algebra contains a canonical homomorphic image of its ring of scalars as scalar multiples of the unity element. This names the homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015.)
Assertion
Ref Expression
df-ascl algSc = (𝑀 ∈ V ↦ (π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘€)) ↦ (π‘₯( ·𝑠 β€˜π‘€)(1rβ€˜π‘€))))
Distinct variable group:   π‘₯,𝑀

Detailed syntax breakdown of Definition df-ascl
StepHypRef Expression
1 cascl 21274 . 2 class algSc
2 vw . . 3 setvar 𝑀
3 cvv 3444 . . 3 class V
4 vx . . . 4 setvar π‘₯
52cv 1541 . . . . . 6 class 𝑀
6 csca 17141 . . . . . 6 class Scalar
75, 6cfv 6497 . . . . 5 class (Scalarβ€˜π‘€)
8 cbs 17088 . . . . 5 class Base
97, 8cfv 6497 . . . 4 class (Baseβ€˜(Scalarβ€˜π‘€))
104cv 1541 . . . . 5 class π‘₯
11 cur 19918 . . . . . 6 class 1r
125, 11cfv 6497 . . . . 5 class (1rβ€˜π‘€)
13 cvsca 17142 . . . . . 6 class ·𝑠
145, 13cfv 6497 . . . . 5 class ( ·𝑠 β€˜π‘€)
1510, 12, 14co 7358 . . . 4 class (π‘₯( ·𝑠 β€˜π‘€)(1rβ€˜π‘€))
164, 9, 15cmpt 5189 . . 3 class (π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘€)) ↦ (π‘₯( ·𝑠 β€˜π‘€)(1rβ€˜π‘€)))
172, 3, 16cmpt 5189 . 2 class (𝑀 ∈ V ↦ (π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘€)) ↦ (π‘₯( ·𝑠 β€˜π‘€)(1rβ€˜π‘€))))
181, 17wceq 1542 1 wff algSc = (𝑀 ∈ V ↦ (π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘€)) ↦ (π‘₯( ·𝑠 β€˜π‘€)(1rβ€˜π‘€))))
Colors of variables: wff setvar class
This definition is referenced by:  asclfval  21298
  Copyright terms: Public domain W3C validator