Description: Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | adj2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | adj1 | |
|
2 | simp2 | |
|
3 | dmadjop | |
|
4 | 3 | ffvelrnda | |
5 | 4 | 3adant2 | |
6 | ax-his1 | |
|
7 | 2 5 6 | syl2anc | |
8 | adjcl | |
|
9 | 8 | 3adant3 | |
10 | simp3 | |
|
11 | ax-his1 | |
|
12 | 9 10 11 | syl2anc | |
13 | 1 7 12 | 3eqtr3d | |
14 | hicl | |
|
15 | 5 2 14 | syl2anc | |
16 | hicl | |
|
17 | 10 9 16 | syl2anc | |
18 | cj11 | |
|
19 | 15 17 18 | syl2anc | |
20 | 13 19 | mpbid | |
21 | 20 | 3com23 | |