Step |
Hyp |
Ref |
Expression |
1 |
|
lspsn.f |
โข ๐น = ( Scalar โ ๐ ) |
2 |
|
lspsn.k |
โข ๐พ = ( Base โ ๐น ) |
3 |
|
lspsn.v |
โข ๐ = ( Base โ ๐ ) |
4 |
|
lspsn.t |
โข ยท = ( ยท๐ โ ๐ ) |
5 |
|
lspsn.n |
โข ๐ = ( LSpan โ ๐ ) |
6 |
|
eqid |
โข ( LSubSp โ ๐ ) = ( LSubSp โ ๐ ) |
7 |
|
simp1 |
โข ( ( ๐ โ LMod โง ๐
โ ๐พ โง ๐ โ ๐ ) โ ๐ โ LMod ) |
8 |
|
simp3 |
โข ( ( ๐ โ LMod โง ๐
โ ๐พ โง ๐ โ ๐ ) โ ๐ โ ๐ ) |
9 |
8
|
snssd |
โข ( ( ๐ โ LMod โง ๐
โ ๐พ โง ๐ โ ๐ ) โ { ๐ } โ ๐ ) |
10 |
3 6 5
|
lspcl |
โข ( ( ๐ โ LMod โง { ๐ } โ ๐ ) โ ( ๐ โ { ๐ } ) โ ( LSubSp โ ๐ ) ) |
11 |
7 9 10
|
syl2anc |
โข ( ( ๐ โ LMod โง ๐
โ ๐พ โง ๐ โ ๐ ) โ ( ๐ โ { ๐ } ) โ ( LSubSp โ ๐ ) ) |
12 |
|
simp2 |
โข ( ( ๐ โ LMod โง ๐
โ ๐พ โง ๐ โ ๐ ) โ ๐
โ ๐พ ) |
13 |
3 4 1 2 5 7 12 8
|
lspsneli |
โข ( ( ๐ โ LMod โง ๐
โ ๐พ โง ๐ โ ๐ ) โ ( ๐
ยท ๐ ) โ ( ๐ โ { ๐ } ) ) |
14 |
6 5 7 11 13
|
lspsnel5a |
โข ( ( ๐ โ LMod โง ๐
โ ๐พ โง ๐ โ ๐ ) โ ( ๐ โ { ( ๐
ยท ๐ ) } ) โ ( ๐ โ { ๐ } ) ) |