Description: The adjoint of a unitary operator is its inverse (converse). Equation 2 of AkhiezerGlazman p. 72. (Contributed by NM, 23-Feb-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | unopadj2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unoplin | |
|
2 | lnopf | |
|
3 | 1 2 | syl | |
4 | cnvunop | |
|
5 | unoplin | |
|
6 | lnopf | |
|
7 | 4 5 6 | 3syl | |
8 | unopadj | |
|
9 | 8 | 3expib | |
10 | 9 | ralrimivv | |
11 | adjeq | |
|
12 | 3 7 10 11 | syl3anc | |