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 = ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) ( 1r ‘ 𝑤 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cascl ⊢ algSc
1 vw ⊢ 𝑤
2 cvv ⊢ V
3 vx ⊢ 𝑥
4 cbs ⊢ Base
5 csca ⊢ Scalar
6 1 cv ⊢ 𝑤
7 6 5 cfv ⊢ ( Scalar ‘ 𝑤 )
8 7 4 cfv ⊢ ( Base ‘ ( Scalar ‘ 𝑤 ) )
9 3 cv ⊢ 𝑥
10 cvsca ⊢ ·𝑠
11 6 10 cfv ⊢ ( ·𝑠 ‘ 𝑤 )
12 cur ⊢ 1r
13 6 12 cfv ⊢ ( 1r ‘ 𝑤 )
14 9 13 11 co ⊢ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) ( 1r ‘ 𝑤 ) )
15 3 8 14 cmpt ⊢ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) ( 1r ‘ 𝑤 ) ) )
16 1 2 15 cmpt ⊢ ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) ( 1r ‘ 𝑤 ) ) ) )
17 0 16 wceq ⊢ algSc = ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) ( 1r ‘ 𝑤 ) ) ) )