This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 unity element. This names the homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015)

Ref Expression
Assertion df-ascl ⊢ algSc = w ∈ V ⟼ x ∈ Base Scalar ⁡ w ⟼ x ⋅ w 1 w

Detailed syntax breakdown

Step Hyp Ref Expression
0 cascl class algSc
1 vw setvar w
2 cvv class V
3 vx setvar x
4 cbs class Base
5 csca class Scalar
6 1 cv setvar w
7 6 5 cfv class Scalar ⁡ w
8 7 4 cfv class Base Scalar ⁡ w
9 3 cv setvar x
10 cvsca class ⋅ 𝑠
11 6 10 cfv class ⋅ w
12 cur class 1 r
13 6 12 cfv class 1 w
14 9 13 11 co class x ⋅ w 1 w
15 3 8 14 cmpt class x ∈ Base Scalar ⁡ w ⟼ x ⋅ w 1 w
16 1 2 15 cmpt class w ∈ V ⟼ x ∈ Base Scalar ⁡ w ⟼ x ⋅ w 1 w
17 0 16 wceq wff algSc = w ∈ V ⟼ x ∈ Base Scalar ⁡ w ⟼ x ⋅ w 1 w