Step |
Hyp |
Ref |
Expression |
1 |
|
nmophm.1 |
โข ๐ โ BndLinOp |
2 |
|
bdopln |
โข ( ๐ โ BndLinOp โ ๐ โ LinOp ) |
3 |
1 2
|
ax-mp |
โข ๐ โ LinOp |
4 |
3
|
lnopmi |
โข ( ๐ด โ โ โ ( ๐ด ยทop ๐ ) โ LinOp ) |
5 |
1
|
nmophmi |
โข ( ๐ด โ โ โ ( normop โ ( ๐ด ยทop ๐ ) ) = ( ( abs โ ๐ด ) ยท ( normop โ ๐ ) ) ) |
6 |
|
abscl |
โข ( ๐ด โ โ โ ( abs โ ๐ด ) โ โ ) |
7 |
|
nmopre |
โข ( ๐ โ BndLinOp โ ( normop โ ๐ ) โ โ ) |
8 |
1 7
|
ax-mp |
โข ( normop โ ๐ ) โ โ |
9 |
|
remulcl |
โข ( ( ( abs โ ๐ด ) โ โ โง ( normop โ ๐ ) โ โ ) โ ( ( abs โ ๐ด ) ยท ( normop โ ๐ ) ) โ โ ) |
10 |
6 8 9
|
sylancl |
โข ( ๐ด โ โ โ ( ( abs โ ๐ด ) ยท ( normop โ ๐ ) ) โ โ ) |
11 |
5 10
|
eqeltrd |
โข ( ๐ด โ โ โ ( normop โ ( ๐ด ยทop ๐ ) ) โ โ ) |
12 |
|
elbdop2 |
โข ( ( ๐ด ยทop ๐ ) โ BndLinOp โ ( ( ๐ด ยทop ๐ ) โ LinOp โง ( normop โ ( ๐ด ยทop ๐ ) ) โ โ ) ) |
13 |
4 11 12
|
sylanbrc |
โข ( ๐ด โ โ โ ( ๐ด ยทop ๐ ) โ BndLinOp ) |