Step |
Hyp |
Ref |
Expression |
1 |
|
rspsnel.1 |
โข ๐ต = ( Base โ ๐
) |
2 |
|
rspsnel.2 |
โข ยท = ( .r โ ๐
) |
3 |
|
rspsnel.3 |
โข ๐พ = ( RSpan โ ๐
) |
4 |
|
rlmlmod |
โข ( ๐
โ Ring โ ( ringLMod โ ๐
) โ LMod ) |
5 |
|
simpr |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ๐ โ ๐ต ) |
6 |
5 1
|
eleqtrdi |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ๐ โ ( Base โ ๐
) ) |
7 |
|
eqid |
โข ( Scalar โ ( ringLMod โ ๐
) ) = ( Scalar โ ( ringLMod โ ๐
) ) |
8 |
|
eqid |
โข ( Base โ ( Scalar โ ( ringLMod โ ๐
) ) ) = ( Base โ ( Scalar โ ( ringLMod โ ๐
) ) ) |
9 |
|
rlmbas |
โข ( Base โ ๐
) = ( Base โ ( ringLMod โ ๐
) ) |
10 |
|
rlmvsca |
โข ( .r โ ๐
) = ( ยท๐ โ ( ringLMod โ ๐
) ) |
11 |
2 10
|
eqtri |
โข ยท = ( ยท๐ โ ( ringLMod โ ๐
) ) |
12 |
|
rspval |
โข ( RSpan โ ๐
) = ( LSpan โ ( ringLMod โ ๐
) ) |
13 |
3 12
|
eqtri |
โข ๐พ = ( LSpan โ ( ringLMod โ ๐
) ) |
14 |
7 8 9 11 13
|
lspsnel |
โข ( ( ( ringLMod โ ๐
) โ LMod โง ๐ โ ( Base โ ๐
) ) โ ( ๐ผ โ ( ๐พ โ { ๐ } ) โ โ ๐ฅ โ ( Base โ ( Scalar โ ( ringLMod โ ๐
) ) ) ๐ผ = ( ๐ฅ ยท ๐ ) ) ) |
15 |
4 6 14
|
syl2an2r |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ( ๐ผ โ ( ๐พ โ { ๐ } ) โ โ ๐ฅ โ ( Base โ ( Scalar โ ( ringLMod โ ๐
) ) ) ๐ผ = ( ๐ฅ ยท ๐ ) ) ) |
16 |
|
rlmsca |
โข ( ๐
โ Ring โ ๐
= ( Scalar โ ( ringLMod โ ๐
) ) ) |
17 |
16
|
adantr |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ๐
= ( Scalar โ ( ringLMod โ ๐
) ) ) |
18 |
17
|
fveq2d |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ( Base โ ๐
) = ( Base โ ( Scalar โ ( ringLMod โ ๐
) ) ) ) |
19 |
1 18
|
eqtr2id |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ( Base โ ( Scalar โ ( ringLMod โ ๐
) ) ) = ๐ต ) |
20 |
19
|
rexeqdv |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ( โ ๐ฅ โ ( Base โ ( Scalar โ ( ringLMod โ ๐
) ) ) ๐ผ = ( ๐ฅ ยท ๐ ) โ โ ๐ฅ โ ๐ต ๐ผ = ( ๐ฅ ยท ๐ ) ) ) |
21 |
15 20
|
bitrd |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ( ๐ผ โ ( ๐พ โ { ๐ } ) โ โ ๐ฅ โ ๐ต ๐ผ = ( ๐ฅ ยท ๐ ) ) ) |