Step |
Hyp |
Ref |
Expression |
1 |
|
nvnegneg.1 |
โข ๐ = ( BaseSet โ ๐ ) |
2 |
|
nvnegneg.4 |
โข ๐ = ( ยท๐ OLD โ ๐ ) |
3 |
|
neg1cn |
โข - 1 โ โ |
4 |
1 2
|
nvscl |
โข ( ( ๐ โ NrmCVec โง - 1 โ โ โง ๐ด โ ๐ ) โ ( - 1 ๐ ๐ด ) โ ๐ ) |
5 |
3 4
|
mp3an2 |
โข ( ( ๐ โ NrmCVec โง ๐ด โ ๐ ) โ ( - 1 ๐ ๐ด ) โ ๐ ) |
6 |
|
eqid |
โข ( +๐ฃ โ ๐ ) = ( +๐ฃ โ ๐ ) |
7 |
|
eqid |
โข ( inv โ ( +๐ฃ โ ๐ ) ) = ( inv โ ( +๐ฃ โ ๐ ) ) |
8 |
1 6 2 7
|
nvinv |
โข ( ( ๐ โ NrmCVec โง ( - 1 ๐ ๐ด ) โ ๐ ) โ ( - 1 ๐ ( - 1 ๐ ๐ด ) ) = ( ( inv โ ( +๐ฃ โ ๐ ) ) โ ( - 1 ๐ ๐ด ) ) ) |
9 |
5 8
|
syldan |
โข ( ( ๐ โ NrmCVec โง ๐ด โ ๐ ) โ ( - 1 ๐ ( - 1 ๐ ๐ด ) ) = ( ( inv โ ( +๐ฃ โ ๐ ) ) โ ( - 1 ๐ ๐ด ) ) ) |
10 |
1 6 2 7
|
nvinv |
โข ( ( ๐ โ NrmCVec โง ๐ด โ ๐ ) โ ( - 1 ๐ ๐ด ) = ( ( inv โ ( +๐ฃ โ ๐ ) ) โ ๐ด ) ) |
11 |
10
|
fveq2d |
โข ( ( ๐ โ NrmCVec โง ๐ด โ ๐ ) โ ( ( inv โ ( +๐ฃ โ ๐ ) ) โ ( - 1 ๐ ๐ด ) ) = ( ( inv โ ( +๐ฃ โ ๐ ) ) โ ( ( inv โ ( +๐ฃ โ ๐ ) ) โ ๐ด ) ) ) |
12 |
6
|
nvgrp |
โข ( ๐ โ NrmCVec โ ( +๐ฃ โ ๐ ) โ GrpOp ) |
13 |
1 6
|
bafval |
โข ๐ = ran ( +๐ฃ โ ๐ ) |
14 |
13 7
|
grpo2inv |
โข ( ( ( +๐ฃ โ ๐ ) โ GrpOp โง ๐ด โ ๐ ) โ ( ( inv โ ( +๐ฃ โ ๐ ) ) โ ( ( inv โ ( +๐ฃ โ ๐ ) ) โ ๐ด ) ) = ๐ด ) |
15 |
12 14
|
sylan |
โข ( ( ๐ โ NrmCVec โง ๐ด โ ๐ ) โ ( ( inv โ ( +๐ฃ โ ๐ ) ) โ ( ( inv โ ( +๐ฃ โ ๐ ) ) โ ๐ด ) ) = ๐ด ) |
16 |
9 11 15
|
3eqtrd |
โข ( ( ๐ โ NrmCVec โง ๐ด โ ๐ ) โ ( - 1 ๐ ( - 1 ๐ ๐ด ) ) = ๐ด ) |