Step |
Hyp |
Ref |
Expression |
1 |
|
hldi.1 |
โข ๐ = ( BaseSet โ ๐ ) |
2 |
|
hldi.2 |
โข ๐บ = ( +๐ฃ โ ๐ ) |
3 |
|
hldi.4 |
โข ๐ = ( ยท๐ OLD โ ๐ ) |
4 |
|
hlnv |
โข ( ๐ โ CHilOLD โ ๐ โ NrmCVec ) |
5 |
1 2 3
|
nvdir |
โข ( ( ๐ โ NrmCVec โง ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ ๐ ) ) โ ( ( ๐ด + ๐ต ) ๐ ๐ถ ) = ( ( ๐ด ๐ ๐ถ ) ๐บ ( ๐ต ๐ ๐ถ ) ) ) |
6 |
4 5
|
sylan |
โข ( ( ๐ โ CHilOLD โง ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ ๐ ) ) โ ( ( ๐ด + ๐ต ) ๐ ๐ถ ) = ( ( ๐ด ๐ ๐ถ ) ๐บ ( ๐ต ๐ ๐ถ ) ) ) |