Step |
Hyp |
Ref |
Expression |
1 |
|
axhil.1 |
โข ๐ = โจ โจ +โ , ยทโ โฉ , normโ โฉ |
2 |
|
axhil.2 |
โข ๐ โ CHilOLD |
3 |
|
df-hba |
โข โ = ( BaseSet โ โจ โจ +โ , ยทโ โฉ , normโ โฉ ) |
4 |
1
|
fveq2i |
โข ( BaseSet โ ๐ ) = ( BaseSet โ โจ โจ +โ , ยทโ โฉ , normโ โฉ ) |
5 |
3 4
|
eqtr4i |
โข โ = ( BaseSet โ ๐ ) |
6 |
2
|
hlnvi |
โข ๐ โ NrmCVec |
7 |
1 6
|
h2hva |
โข +โ = ( +๐ฃ โ ๐ ) |
8 |
5 7
|
hladdf |
โข ( ๐ โ CHilOLD โ +โ : ( โ ร โ ) โถ โ ) |
9 |
2 8
|
ax-mp |
โข +โ : ( โ ร โ ) โถ โ |