Metamath Proof Explorer

Theorem unopadj

Description: The inverse (converse) of a unitary operator is its adjoint. Equation 2 of AkhiezerGlazman p. 72. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	unopadj	$⊢ (T \in UniOp \land A \in ℋ \land B \in ℋ) \to T (A) \cdot_{ih} B = A \cdot_{ih} T^{-1} (B)$

Proof

Step	Hyp	Ref	Expression
1		unopf1o	$⊢ T \in UniOp \to T : ℋ \underset{1-1 onto}{⟶} ℋ$
2		f1ocnvfv2	$⊢ (T : ℋ \underset{1-1 onto}{⟶} ℋ \land B \in ℋ) \to T (T^{-1} (B)) = B$
3	1 2	sylan	$⊢ (T \in UniOp \land B \in ℋ) \to T (T^{-1} (B)) = B$
4	3	3adant2	$⊢ (T \in UniOp \land A \in ℋ \land B \in ℋ) \to T (T^{-1} (B)) = B$
5	4	oveq2d	$⊢ (T \in UniOp \land A \in ℋ \land B \in ℋ) \to T (A) \cdot_{ih} T (T^{-1} (B)) = T (A) \cdot_{ih} B$
6		f1ocnv	$⊢ T : ℋ \underset{1-1 onto}{⟶} ℋ \to T^{-1} : ℋ \underset{1-1 onto}{⟶} ℋ$
7		f1of	$⊢ T^{-1} : ℋ \underset{1-1 onto}{⟶} ℋ \to T^{-1} : ℋ ⟶ ℋ$
8	1 6 7	3syl	$⊢ T \in UniOp \to T^{-1} : ℋ ⟶ ℋ$
9	8	ffvelcdmda	$⊢ (T \in UniOp \land B \in ℋ) \to T^{-1} (B) \in ℋ$
10	9	3adant2	$⊢ (T \in UniOp \land A \in ℋ \land B \in ℋ) \to T^{-1} (B) \in ℋ$
11		unop	$⊢ (T \in UniOp \land A \in ℋ \land T^{-1} (B) \in ℋ) \to T (A) \cdot_{ih} T (T^{-1} (B)) = A \cdot_{ih} T^{-1} (B)$
12	10 11	syld3an3	$⊢ (T \in UniOp \land A \in ℋ \land B \in ℋ) \to T (A) \cdot_{ih} T (T^{-1} (B)) = A \cdot_{ih} T^{-1} (B)$
13	5 12	eqtr3d	$⊢ (T \in UniOp \land A \in ℋ \land B \in ℋ) \to T (A) \cdot_{ih} B = A \cdot_{ih} T^{-1} (B)$