Step |
Hyp |
Ref |
Expression |
1 |
|
lssvnegcl.s |
โข ๐ = ( LSubSp โ ๐ ) |
2 |
|
lssvnegcl.n |
โข ๐ = ( invg โ ๐ ) |
3 |
|
eqid |
โข ( Base โ ๐ ) = ( Base โ ๐ ) |
4 |
3 1
|
lssel |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ๐ โ ( Base โ ๐ ) ) |
5 |
|
eqid |
โข ( Scalar โ ๐ ) = ( Scalar โ ๐ ) |
6 |
|
eqid |
โข ( ยท๐ โ ๐ ) = ( ยท๐ โ ๐ ) |
7 |
|
eqid |
โข ( 1r โ ( Scalar โ ๐ ) ) = ( 1r โ ( Scalar โ ๐ ) ) |
8 |
|
eqid |
โข ( invg โ ( Scalar โ ๐ ) ) = ( invg โ ( Scalar โ ๐ ) ) |
9 |
3 2 5 6 7 8
|
lmodvneg1 |
โข ( ( ๐ โ LMod โง ๐ โ ( Base โ ๐ ) ) โ ( ( ( invg โ ( Scalar โ ๐ ) ) โ ( 1r โ ( Scalar โ ๐ ) ) ) ( ยท๐ โ ๐ ) ๐ ) = ( ๐ โ ๐ ) ) |
10 |
4 9
|
sylan2 |
โข ( ( ๐ โ LMod โง ( ๐ โ ๐ โง ๐ โ ๐ ) ) โ ( ( ( invg โ ( Scalar โ ๐ ) ) โ ( 1r โ ( Scalar โ ๐ ) ) ) ( ยท๐ โ ๐ ) ๐ ) = ( ๐ โ ๐ ) ) |
11 |
10
|
3impb |
โข ( ( ๐ โ LMod โง ๐ โ ๐ โง ๐ โ ๐ ) โ ( ( ( invg โ ( Scalar โ ๐ ) ) โ ( 1r โ ( Scalar โ ๐ ) ) ) ( ยท๐ โ ๐ ) ๐ ) = ( ๐ โ ๐ ) ) |
12 |
|
simp1 |
โข ( ( ๐ โ LMod โง ๐ โ ๐ โง ๐ โ ๐ ) โ ๐ โ LMod ) |
13 |
|
simp2 |
โข ( ( ๐ โ LMod โง ๐ โ ๐ โง ๐ โ ๐ ) โ ๐ โ ๐ ) |
14 |
5
|
lmodring |
โข ( ๐ โ LMod โ ( Scalar โ ๐ ) โ Ring ) |
15 |
14
|
3ad2ant1 |
โข ( ( ๐ โ LMod โง ๐ โ ๐ โง ๐ โ ๐ ) โ ( Scalar โ ๐ ) โ Ring ) |
16 |
|
ringgrp |
โข ( ( Scalar โ ๐ ) โ Ring โ ( Scalar โ ๐ ) โ Grp ) |
17 |
15 16
|
syl |
โข ( ( ๐ โ LMod โง ๐ โ ๐ โง ๐ โ ๐ ) โ ( Scalar โ ๐ ) โ Grp ) |
18 |
|
eqid |
โข ( Base โ ( Scalar โ ๐ ) ) = ( Base โ ( Scalar โ ๐ ) ) |
19 |
18 7
|
ringidcl |
โข ( ( Scalar โ ๐ ) โ Ring โ ( 1r โ ( Scalar โ ๐ ) ) โ ( Base โ ( Scalar โ ๐ ) ) ) |
20 |
15 19
|
syl |
โข ( ( ๐ โ LMod โง ๐ โ ๐ โง ๐ โ ๐ ) โ ( 1r โ ( Scalar โ ๐ ) ) โ ( Base โ ( Scalar โ ๐ ) ) ) |
21 |
18 8
|
grpinvcl |
โข ( ( ( Scalar โ ๐ ) โ Grp โง ( 1r โ ( Scalar โ ๐ ) ) โ ( Base โ ( Scalar โ ๐ ) ) ) โ ( ( invg โ ( Scalar โ ๐ ) ) โ ( 1r โ ( Scalar โ ๐ ) ) ) โ ( Base โ ( Scalar โ ๐ ) ) ) |
22 |
17 20 21
|
syl2anc |
โข ( ( ๐ โ LMod โง ๐ โ ๐ โง ๐ โ ๐ ) โ ( ( invg โ ( Scalar โ ๐ ) ) โ ( 1r โ ( Scalar โ ๐ ) ) ) โ ( Base โ ( Scalar โ ๐ ) ) ) |
23 |
|
simp3 |
โข ( ( ๐ โ LMod โง ๐ โ ๐ โง ๐ โ ๐ ) โ ๐ โ ๐ ) |
24 |
5 6 18 1
|
lssvscl |
โข ( ( ( ๐ โ LMod โง ๐ โ ๐ ) โง ( ( ( invg โ ( Scalar โ ๐ ) ) โ ( 1r โ ( Scalar โ ๐ ) ) ) โ ( Base โ ( Scalar โ ๐ ) ) โง ๐ โ ๐ ) ) โ ( ( ( invg โ ( Scalar โ ๐ ) ) โ ( 1r โ ( Scalar โ ๐ ) ) ) ( ยท๐ โ ๐ ) ๐ ) โ ๐ ) |
25 |
12 13 22 23 24
|
syl22anc |
โข ( ( ๐ โ LMod โง ๐ โ ๐ โง ๐ โ ๐ ) โ ( ( ( invg โ ( Scalar โ ๐ ) ) โ ( 1r โ ( Scalar โ ๐ ) ) ) ( ยท๐ โ ๐ ) ๐ ) โ ๐ ) |
26 |
11 25
|
eqeltrrd |
โข ( ( ๐ โ LMod โง ๐ โ ๐ โง ๐ โ ๐ ) โ ( ๐ โ ๐ ) โ ๐ ) |