| Step |
Hyp |
Ref |
Expression |
| 1 |
|
nmcopex |
|- ( ( T e. LinOp /\ T e. ContOp ) -> ( normop ` T ) e. RR ) |
| 2 |
1
|
ex |
|- ( T e. LinOp -> ( T e. ContOp -> ( normop ` T ) e. RR ) ) |
| 3 |
|
elbdop2 |
|- ( T e. BndLinOp <-> ( T e. LinOp /\ ( normop ` T ) e. RR ) ) |
| 4 |
3
|
baibr |
|- ( T e. LinOp -> ( ( normop ` T ) e. RR <-> T e. BndLinOp ) ) |
| 5 |
2 4
|
sylibd |
|- ( T e. LinOp -> ( T e. ContOp -> T e. BndLinOp ) ) |
| 6 |
|
nmopre |
|- ( T e. BndLinOp -> ( normop ` T ) e. RR ) |
| 7 |
|
nmbdoplb |
|- ( ( T e. BndLinOp /\ y e. ~H ) -> ( normh ` ( T ` y ) ) <_ ( ( normop ` T ) x. ( normh ` y ) ) ) |
| 8 |
7
|
ralrimiva |
|- ( T e. BndLinOp -> A. y e. ~H ( normh ` ( T ` y ) ) <_ ( ( normop ` T ) x. ( normh ` y ) ) ) |
| 9 |
|
oveq1 |
|- ( x = ( normop ` T ) -> ( x x. ( normh ` y ) ) = ( ( normop ` T ) x. ( normh ` y ) ) ) |
| 10 |
9
|
breq2d |
|- ( x = ( normop ` T ) -> ( ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) <-> ( normh ` ( T ` y ) ) <_ ( ( normop ` T ) x. ( normh ` y ) ) ) ) |
| 11 |
10
|
ralbidv |
|- ( x = ( normop ` T ) -> ( A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) <-> A. y e. ~H ( normh ` ( T ` y ) ) <_ ( ( normop ` T ) x. ( normh ` y ) ) ) ) |
| 12 |
11
|
rspcev |
|- ( ( ( normop ` T ) e. RR /\ A. y e. ~H ( normh ` ( T ` y ) ) <_ ( ( normop ` T ) x. ( normh ` y ) ) ) -> E. x e. RR A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) |
| 13 |
6 8 12
|
syl2anc |
|- ( T e. BndLinOp -> E. x e. RR A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) |
| 14 |
|
lnopcon |
|- ( T e. LinOp -> ( T e. ContOp <-> E. x e. RR A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) ) |
| 15 |
13 14
|
imbitrrid |
|- ( T e. LinOp -> ( T e. BndLinOp -> T e. ContOp ) ) |
| 16 |
5 15
|
impbid |
|- ( T e. LinOp -> ( T e. ContOp <-> T e. BndLinOp ) ) |