Step |
Hyp |
Ref |
Expression |
1 |
|
bloval.3 |
|- N = ( U normOpOLD W ) |
2 |
|
bloval.4 |
|- L = ( U LnOp W ) |
3 |
|
bloval.5 |
|- B = ( U BLnOp W ) |
4 |
1 2 3
|
bloval |
|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> B = { t e. L | ( N ` t ) < +oo } ) |
5 |
4
|
eleq2d |
|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( T e. B <-> T e. { t e. L | ( N ` t ) < +oo } ) ) |
6 |
|
fveq2 |
|- ( t = T -> ( N ` t ) = ( N ` T ) ) |
7 |
6
|
breq1d |
|- ( t = T -> ( ( N ` t ) < +oo <-> ( N ` T ) < +oo ) ) |
8 |
7
|
elrab |
|- ( T e. { t e. L | ( N ` t ) < +oo } <-> ( T e. L /\ ( N ` T ) < +oo ) ) |
9 |
5 8
|
syl6bb |
|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( T e. B <-> ( T e. L /\ ( N ` T ) < +oo ) ) ) |