Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
โข โจ โจ +โ , ยทโ โฉ , normโ โฉ = โจ โจ +โ , ยทโ โฉ , normโ โฉ |
2 |
1
|
hhnv |
โข โจ โจ +โ , ยทโ โฉ , normโ โฉ โ NrmCVec |
3 |
|
df-hba |
โข โ = ( BaseSet โ โจ โจ +โ , ยทโ โฉ , normโ โฉ ) |
4 |
1
|
hhnm |
โข normโ = ( normCV โ โจ โจ +โ , ยทโ โฉ , normโ โฉ ) |
5 |
3 4
|
nmosetre |
โข ( ( โจ โจ +โ , ยทโ โฉ , normโ โฉ โ NrmCVec โง ๐ : โ โถ โ ) โ { ๐ฅ โฃ โ ๐ฆ โ โ ( ( normโ โ ๐ฆ ) โค 1 โง ๐ฅ = ( normโ โ ( ๐ โ ๐ฆ ) ) ) } โ โ ) |
6 |
2 5
|
mpan |
โข ( ๐ : โ โถ โ โ { ๐ฅ โฃ โ ๐ฆ โ โ ( ( normโ โ ๐ฆ ) โค 1 โง ๐ฅ = ( normโ โ ( ๐ โ ๐ฆ ) ) ) } โ โ ) |