Step |
Hyp |
Ref |
Expression |
1 |
|
hhnmo.1 |
โข ๐ = โจ โจ +โ , ยทโ โฉ , normโ โฉ |
2 |
|
hhblo.2 |
โข ๐ต = ( ๐ BLnOp ๐ ) |
3 |
|
df-bdop |
โข BndLinOp = { ๐ฅ โ LinOp โฃ ( normop โ ๐ฅ ) < +โ } |
4 |
1
|
hhnv |
โข ๐ โ NrmCVec |
5 |
|
eqid |
โข ( ๐ normOpOLD ๐ ) = ( ๐ normOpOLD ๐ ) |
6 |
1 5
|
hhnmoi |
โข normop = ( ๐ normOpOLD ๐ ) |
7 |
|
eqid |
โข ( ๐ LnOp ๐ ) = ( ๐ LnOp ๐ ) |
8 |
1 7
|
hhlnoi |
โข LinOp = ( ๐ LnOp ๐ ) |
9 |
6 8 2
|
bloval |
โข ( ( ๐ โ NrmCVec โง ๐ โ NrmCVec ) โ ๐ต = { ๐ฅ โ LinOp โฃ ( normop โ ๐ฅ ) < +โ } ) |
10 |
4 4 9
|
mp2an |
โข ๐ต = { ๐ฅ โ LinOp โฃ ( normop โ ๐ฅ ) < +โ } |
11 |
3 10
|
eqtr4i |
โข BndLinOp = ๐ต |