Step |
Hyp |
Ref |
Expression |
1 |
|
rspsnel.1 |
|- B = ( Base ` R ) |
2 |
|
rspsnel.2 |
|- .x. = ( .r ` R ) |
3 |
|
rspsnel.3 |
|- K = ( RSpan ` R ) |
4 |
|
rlmlmod |
|- ( R e. Ring -> ( ringLMod ` R ) e. LMod ) |
5 |
|
simpr |
|- ( ( R e. Ring /\ X e. B ) -> X e. B ) |
6 |
5 1
|
eleqtrdi |
|- ( ( R e. Ring /\ X e. B ) -> X e. ( Base ` R ) ) |
7 |
|
eqid |
|- ( Scalar ` ( ringLMod ` R ) ) = ( Scalar ` ( ringLMod ` R ) ) |
8 |
|
eqid |
|- ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) = ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) |
9 |
|
rlmbas |
|- ( Base ` R ) = ( Base ` ( ringLMod ` R ) ) |
10 |
|
rlmvsca |
|- ( .r ` R ) = ( .s ` ( ringLMod ` R ) ) |
11 |
2 10
|
eqtri |
|- .x. = ( .s ` ( ringLMod ` R ) ) |
12 |
|
rspval |
|- ( RSpan ` R ) = ( LSpan ` ( ringLMod ` R ) ) |
13 |
3 12
|
eqtri |
|- K = ( LSpan ` ( ringLMod ` R ) ) |
14 |
7 8 9 11 13
|
lspsnel |
|- ( ( ( ringLMod ` R ) e. LMod /\ X e. ( Base ` R ) ) -> ( I e. ( K ` { X } ) <-> E. x e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) I = ( x .x. X ) ) ) |
15 |
4 6 14
|
syl2an2r |
|- ( ( R e. Ring /\ X e. B ) -> ( I e. ( K ` { X } ) <-> E. x e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) I = ( x .x. X ) ) ) |
16 |
|
rlmsca |
|- ( R e. Ring -> R = ( Scalar ` ( ringLMod ` R ) ) ) |
17 |
16
|
adantr |
|- ( ( R e. Ring /\ X e. B ) -> R = ( Scalar ` ( ringLMod ` R ) ) ) |
18 |
17
|
fveq2d |
|- ( ( R e. Ring /\ X e. B ) -> ( Base ` R ) = ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) ) |
19 |
1 18
|
eqtr2id |
|- ( ( R e. Ring /\ X e. B ) -> ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) = B ) |
20 |
19
|
rexeqdv |
|- ( ( R e. Ring /\ X e. B ) -> ( E. x e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) I = ( x .x. X ) <-> E. x e. B I = ( x .x. X ) ) ) |
21 |
15 20
|
bitrd |
|- ( ( R e. Ring /\ X e. B ) -> ( I e. ( K ` { X } ) <-> E. x e. B I = ( x .x. X ) ) ) |