Description: An operator is bounded and linear iff its adjoint is. (Contributed by NM, 19-Feb-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | adjbdlnb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | adjbdln | |
|
2 | bdopadj | |
|
3 | dmadjrnb | |
|
4 | 2 3 | sylibr | |
5 | cnvadj | |
|
6 | 5 | fveq1i | |
7 | adj1o | |
|
8 | simpl | |
|
9 | f1ocnvfv1 | |
|
10 | 7 8 9 | sylancr | |
11 | 6 10 | eqtr3id | |
12 | adjbdln | |
|
13 | 12 | adantl | |
14 | 11 13 | eqeltrrd | |
15 | 4 14 | mpancom | |
16 | 1 15 | impbii | |