Metamath Proof Explorer


Theorem unopadj2

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 TUniOpadjhT=T-1

Proof

Step Hyp Ref Expression
1 unoplin TUniOpTLinOp
2 lnopf TLinOpT:
3 1 2 syl TUniOpT:
4 cnvunop TUniOpT-1UniOp
5 unoplin T-1UniOpT-1LinOp
6 lnopf T-1LinOpT-1:
7 4 5 6 3syl TUniOpT-1:
8 unopadj TUniOpxyTxihy=xihT-1y
9 8 3expib TUniOpxyTxihy=xihT-1y
10 9 ralrimivv TUniOpxyTxihy=xihT-1y
11 adjeq T:T-1:xyTxihy=xihT-1yadjhT=T-1
12 3 7 10 11 syl3anc TUniOpadjhT=T-1