# Metamath Proof Explorer

## Theorem rnascl

Description: The set of injected scalars is also interpretable as the span of the identity. (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Hypotheses rnascl.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
rnascl.o
rnascl.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
Assertion rnascl

### Proof

Step Hyp Ref Expression
1 rnascl.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
2 rnascl.o
3 rnascl.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
4 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
5 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
6 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
7 1 4 5 6 2 asclfval
8 7 rnmpt
9 assalmod ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{LMod}$
10 assaring ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{Ring}$
11 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
12 11 2 ringidcl
13 10 12 syl
14 4 5 11 6 3 lspsn
15 9 13 14 syl2anc
16 8 15 eqtr4id