Step |
Hyp |
Ref |
Expression |
1 |
|
nmcopex |
โข ( ( ๐ โ LinOp โง ๐ โ ContOp ) โ ( normop โ ๐ ) โ โ ) |
2 |
1
|
ex |
โข ( ๐ โ LinOp โ ( ๐ โ ContOp โ ( normop โ ๐ ) โ โ ) ) |
3 |
|
elbdop2 |
โข ( ๐ โ BndLinOp โ ( ๐ โ LinOp โง ( normop โ ๐ ) โ โ ) ) |
4 |
3
|
baibr |
โข ( ๐ โ LinOp โ ( ( normop โ ๐ ) โ โ โ ๐ โ BndLinOp ) ) |
5 |
2 4
|
sylibd |
โข ( ๐ โ LinOp โ ( ๐ โ ContOp โ ๐ โ BndLinOp ) ) |
6 |
|
nmopre |
โข ( ๐ โ BndLinOp โ ( normop โ ๐ ) โ โ ) |
7 |
|
nmbdoplb |
โข ( ( ๐ โ BndLinOp โง ๐ฆ โ โ ) โ ( normโ โ ( ๐ โ ๐ฆ ) ) โค ( ( normop โ ๐ ) ยท ( normโ โ ๐ฆ ) ) ) |
8 |
7
|
ralrimiva |
โข ( ๐ โ BndLinOp โ โ ๐ฆ โ โ ( normโ โ ( ๐ โ ๐ฆ ) ) โค ( ( normop โ ๐ ) ยท ( normโ โ ๐ฆ ) ) ) |
9 |
|
oveq1 |
โข ( ๐ฅ = ( normop โ ๐ ) โ ( ๐ฅ ยท ( normโ โ ๐ฆ ) ) = ( ( normop โ ๐ ) ยท ( normโ โ ๐ฆ ) ) ) |
10 |
9
|
breq2d |
โข ( ๐ฅ = ( normop โ ๐ ) โ ( ( normโ โ ( ๐ โ ๐ฆ ) ) โค ( ๐ฅ ยท ( normโ โ ๐ฆ ) ) โ ( normโ โ ( ๐ โ ๐ฆ ) ) โค ( ( normop โ ๐ ) ยท ( normโ โ ๐ฆ ) ) ) ) |
11 |
10
|
ralbidv |
โข ( ๐ฅ = ( normop โ ๐ ) โ ( โ ๐ฆ โ โ ( normโ โ ( ๐ โ ๐ฆ ) ) โค ( ๐ฅ ยท ( normโ โ ๐ฆ ) ) โ โ ๐ฆ โ โ ( normโ โ ( ๐ โ ๐ฆ ) ) โค ( ( normop โ ๐ ) ยท ( normโ โ ๐ฆ ) ) ) ) |
12 |
11
|
rspcev |
โข ( ( ( normop โ ๐ ) โ โ โง โ ๐ฆ โ โ ( normโ โ ( ๐ โ ๐ฆ ) ) โค ( ( normop โ ๐ ) ยท ( normโ โ ๐ฆ ) ) ) โ โ ๐ฅ โ โ โ ๐ฆ โ โ ( normโ โ ( ๐ โ ๐ฆ ) ) โค ( ๐ฅ ยท ( normโ โ ๐ฆ ) ) ) |
13 |
6 8 12
|
syl2anc |
โข ( ๐ โ BndLinOp โ โ ๐ฅ โ โ โ ๐ฆ โ โ ( normโ โ ( ๐ โ ๐ฆ ) ) โค ( ๐ฅ ยท ( normโ โ ๐ฆ ) ) ) |
14 |
|
lnopcon |
โข ( ๐ โ LinOp โ ( ๐ โ ContOp โ โ ๐ฅ โ โ โ ๐ฆ โ โ ( normโ โ ( ๐ โ ๐ฆ ) ) โค ( ๐ฅ ยท ( normโ โ ๐ฆ ) ) ) ) |
15 |
13 14
|
imbitrrid |
โข ( ๐ โ LinOp โ ( ๐ โ BndLinOp โ ๐ โ ContOp ) ) |
16 |
5 15
|
impbid |
โข ( ๐ โ LinOp โ ( ๐ โ ContOp โ ๐ โ BndLinOp ) ) |