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 | |
|
rnascl.o | |
||
rnascl.n | |
||
Assertion | rnascl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rnascl.a | |
|
2 | rnascl.o | |
|
3 | rnascl.n | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | 1 4 5 6 2 | asclfval | |
8 | 7 | rnmpt | |
9 | assalmod | |
|
10 | assaring | |
|
11 | eqid | |
|
12 | 11 2 | ringidcl | |
13 | 10 12 | syl | |
14 | 4 5 11 6 3 | lspsn | |
15 | 9 13 14 | syl2anc | |
16 | 8 15 | eqtr4id | |