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 19081
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 = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑤)) ↦ (𝑥( ·𝑠𝑤)(1r𝑤))))
Distinct variable group:   𝑥,𝑤

Detailed syntax breakdown of Definition df-ascl
StepHypRef Expression
1 cascl 19078 . 2 class algSc
2 vw . . 3 setvar 𝑤
3 cvv 3172 . . 3 class V
4 vx . . . 4 setvar 𝑥
52cv 1473 . . . . . 6 class 𝑤
6 csca 15717 . . . . . 6 class Scalar
75, 6cfv 5790 . . . . 5 class (Scalar‘𝑤)
8 cbs 15641 . . . . 5 class Base
97, 8cfv 5790 . . . 4 class (Base‘(Scalar‘𝑤))
104cv 1473 . . . . 5 class 𝑥
11 cur 18270 . . . . . 6 class 1r
125, 11cfv 5790 . . . . 5 class (1r𝑤)
13 cvsca 15718 . . . . . 6 class ·𝑠
145, 13cfv 5790 . . . . 5 class ( ·𝑠𝑤)
1510, 12, 14co 6527 . . . 4 class (𝑥( ·𝑠𝑤)(1r𝑤))
164, 9, 15cmpt 4637 . . 3 class (𝑥 ∈ (Base‘(Scalar‘𝑤)) ↦ (𝑥( ·𝑠𝑤)(1r𝑤)))
172, 3, 16cmpt 4637 . 2 class (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑤)) ↦ (𝑥( ·𝑠𝑤)(1r𝑤))))
181, 17wceq 1474 1 wff algSc = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑤)) ↦ (𝑥( ·𝑠𝑤)(1r𝑤))))
Colors of variables: wff setvar class
This definition is referenced by:  asclfval  19101
  Copyright terms: Public domain W3C validator