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=algScW
rnascl.o 1˙=1W
rnascl.n N=LSpanW
Assertion rnascl WAssAlgranA=N1˙

Proof

Step Hyp Ref Expression
1 rnascl.a A=algScW
2 rnascl.o 1˙=1W
3 rnascl.n N=LSpanW
4 eqid ScalarW=ScalarW
5 eqid BaseScalarW=BaseScalarW
6 eqid W=W
7 1 4 5 6 2 asclfval A=yBaseScalarWyW1˙
8 7 rnmpt ranA=x|yBaseScalarWx=yW1˙
9 assalmod WAssAlgWLMod
10 assaring WAssAlgWRing
11 eqid BaseW=BaseW
12 11 2 ringidcl WRing1˙BaseW
13 10 12 syl WAssAlg1˙BaseW
14 4 5 11 6 3 lspsn WLMod1˙BaseWN1˙=x|yBaseScalarWx=yW1˙
15 9 13 14 syl2anc WAssAlgN1˙=x|yBaseScalarWx=yW1˙
16 8 15 eqtr4id WAssAlgranA=N1˙