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	$⊢ T \in UniOp \to {adj}_{h} (T) = T^{-1}$

Proof

Step	Hyp	Ref	Expression
1		unoplin	$⊢ T \in UniOp \to T \in LinOp$
2		lnopf	$⊢ T \in LinOp \to T : ℋ ⟶ ℋ$
3	1 2	syl	$⊢ T \in UniOp \to T : ℋ ⟶ ℋ$
4		cnvunop	$⊢ T \in UniOp \to T^{-1} \in UniOp$
5		unoplin	$⊢ T^{-1} \in UniOp \to T^{-1} \in LinOp$
6		lnopf	$⊢ T^{-1} \in LinOp \to T^{-1} : ℋ ⟶ ℋ$
7	4 5 6	3syl	$⊢ T \in UniOp \to T^{-1} : ℋ ⟶ ℋ$
8		unopadj	$⊢ (T \in UniOp \land x \in ℋ \land y \in ℋ) \to T (x) \cdot_{ih} y = x \cdot_{ih} T^{-1} (y)$
9	8	3expib	$⊢ T \in UniOp \to ((x \in ℋ \land y \in ℋ) \to T (x) \cdot_{ih} y = x \cdot_{ih} T^{-1} (y))$
10	9	ralrimivv	$⊢ T \in UniOp \to \forall x \in ℋ \forall y \in ℋ T (x) \cdot_{ih} y = x \cdot_{ih} T^{-1} (y)$
11		adjeq	$⊢ (T : ℋ ⟶ ℋ \land T^{-1} : ℋ ⟶ ℋ \land \forall x \in ℋ \forall y \in ℋ T (x) \cdot_{ih} y = x \cdot_{ih} T^{-1} (y)) \to {adj}_{h} (T) = T^{-1}$
12	3 7 10 11	syl3anc	$⊢ T \in UniOp \to {adj}_{h} (T) = T^{-1}$