Step |
Hyp |
Ref |
Expression |
1 |
|
lssss.v |
โข ๐ = ( Base โ ๐ ) |
2 |
|
lssss.s |
โข ๐ = ( LSubSp โ ๐ ) |
3 |
|
eqidd |
โข ( ๐ โ LMod โ ( Scalar โ ๐ ) = ( Scalar โ ๐ ) ) |
4 |
|
eqidd |
โข ( ๐ โ LMod โ ( Base โ ( Scalar โ ๐ ) ) = ( Base โ ( Scalar โ ๐ ) ) ) |
5 |
1
|
a1i |
โข ( ๐ โ LMod โ ๐ = ( Base โ ๐ ) ) |
6 |
|
eqidd |
โข ( ๐ โ LMod โ ( +g โ ๐ ) = ( +g โ ๐ ) ) |
7 |
|
eqidd |
โข ( ๐ โ LMod โ ( ยท๐ โ ๐ ) = ( ยท๐ โ ๐ ) ) |
8 |
2
|
a1i |
โข ( ๐ โ LMod โ ๐ = ( LSubSp โ ๐ ) ) |
9 |
|
ssidd |
โข ( ๐ โ LMod โ ๐ โ ๐ ) |
10 |
1
|
lmodbn0 |
โข ( ๐ โ LMod โ ๐ โ โ
) |
11 |
|
simpl |
โข ( ( ๐ โ LMod โง ( ๐ฅ โ ( Base โ ( Scalar โ ๐ ) ) โง ๐ โ ๐ โง ๐ โ ๐ ) ) โ ๐ โ LMod ) |
12 |
|
eqid |
โข ( Scalar โ ๐ ) = ( Scalar โ ๐ ) |
13 |
|
eqid |
โข ( ยท๐ โ ๐ ) = ( ยท๐ โ ๐ ) |
14 |
|
eqid |
โข ( Base โ ( Scalar โ ๐ ) ) = ( Base โ ( Scalar โ ๐ ) ) |
15 |
1 12 13 14
|
lmodvscl |
โข ( ( ๐ โ LMod โง ๐ฅ โ ( Base โ ( Scalar โ ๐ ) ) โง ๐ โ ๐ ) โ ( ๐ฅ ( ยท๐ โ ๐ ) ๐ ) โ ๐ ) |
16 |
15
|
3adant3r3 |
โข ( ( ๐ โ LMod โง ( ๐ฅ โ ( Base โ ( Scalar โ ๐ ) ) โง ๐ โ ๐ โง ๐ โ ๐ ) ) โ ( ๐ฅ ( ยท๐ โ ๐ ) ๐ ) โ ๐ ) |
17 |
|
simpr3 |
โข ( ( ๐ โ LMod โง ( ๐ฅ โ ( Base โ ( Scalar โ ๐ ) ) โง ๐ โ ๐ โง ๐ โ ๐ ) ) โ ๐ โ ๐ ) |
18 |
|
eqid |
โข ( +g โ ๐ ) = ( +g โ ๐ ) |
19 |
1 18
|
lmodvacl |
โข ( ( ๐ โ LMod โง ( ๐ฅ ( ยท๐ โ ๐ ) ๐ ) โ ๐ โง ๐ โ ๐ ) โ ( ( ๐ฅ ( ยท๐ โ ๐ ) ๐ ) ( +g โ ๐ ) ๐ ) โ ๐ ) |
20 |
11 16 17 19
|
syl3anc |
โข ( ( ๐ โ LMod โง ( ๐ฅ โ ( Base โ ( Scalar โ ๐ ) ) โง ๐ โ ๐ โง ๐ โ ๐ ) ) โ ( ( ๐ฅ ( ยท๐ โ ๐ ) ๐ ) ( +g โ ๐ ) ๐ ) โ ๐ ) |
21 |
3 4 5 6 7 8 9 10 20
|
islssd |
โข ( ๐ โ LMod โ ๐ โ ๐ ) |