cnvunop

Description: The inverse (converse) of a unitary operator in Hilbert space is unitary. Theorem in AkhiezerGlazman p. 72. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	cnvunop	$⊢ T \in UniOp \to T^{-1} \in UniOp$

Proof

Step	Hyp	Ref	Expression
1		unopf1o	$⊢ T \in UniOp \to T : ℋ \underset{1-1 onto}{⟶} ℋ$
2		f1ocnv	$⊢ T : ℋ \underset{1-1 onto}{⟶} ℋ \to T^{-1} : ℋ \underset{1-1 onto}{⟶} ℋ$
3		f1ofo	$⊢ T^{-1} : ℋ \underset{1-1 onto}{⟶} ℋ \to T^{-1} : ℋ \underset{onto}{⟶} ℋ$
4	2 3	syl	$⊢ T : ℋ \underset{1-1 onto}{⟶} ℋ \to T^{-1} : ℋ \underset{onto}{⟶} ℋ$
5	1 4	syl	$⊢ T \in UniOp \to T^{-1} : ℋ \underset{onto}{⟶} ℋ$
6		simpl	$⊢ (T \in UniOp \land (x \in ℋ \land y \in ℋ)) \to T \in UniOp$
7		fof	$⊢ T^{-1} : ℋ \underset{onto}{⟶} ℋ \to T^{-1} : ℋ ⟶ ℋ$
8	5 7	syl	$⊢ T \in UniOp \to T^{-1} : ℋ ⟶ ℋ$
9	8	ffvelcdmda	$⊢ (T \in UniOp \land x \in ℋ) \to T^{-1} (x) \in ℋ$
10	9	adantrr	$⊢ (T \in UniOp \land (x \in ℋ \land y \in ℋ)) \to T^{-1} (x) \in ℋ$
11	8	ffvelcdmda	$⊢ (T \in UniOp \land y \in ℋ) \to T^{-1} (y) \in ℋ$
12	11	adantrl	$⊢ (T \in UniOp \land (x \in ℋ \land y \in ℋ)) \to T^{-1} (y) \in ℋ$
13		unop	$⊢ (T \in UniOp \land T^{-1} (x) \in ℋ \land T^{-1} (y) \in ℋ) \to T (T^{-1} (x)) \cdot_{ih} T (T^{-1} (y)) = T^{-1} (x) \cdot_{ih} T^{-1} (y)$
14	6 10 12 13	syl3anc	$⊢ (T \in UniOp \land (x \in ℋ \land y \in ℋ)) \to T (T^{-1} (x)) \cdot_{ih} T (T^{-1} (y)) = T^{-1} (x) \cdot_{ih} T^{-1} (y)$
15		f1ocnvfv2	$⊢ (T : ℋ \underset{1-1 onto}{⟶} ℋ \land x \in ℋ) \to T (T^{-1} (x)) = x$
16	15	adantrr	$⊢ (T : ℋ \underset{1-1 onto}{⟶} ℋ \land (x \in ℋ \land y \in ℋ)) \to T (T^{-1} (x)) = x$
17		f1ocnvfv2	$⊢ (T : ℋ \underset{1-1 onto}{⟶} ℋ \land y \in ℋ) \to T (T^{-1} (y)) = y$
18	17	adantrl	$⊢ (T : ℋ \underset{1-1 onto}{⟶} ℋ \land (x \in ℋ \land y \in ℋ)) \to T (T^{-1} (y)) = y$
19	16 18	oveq12d	$⊢ (T : ℋ \underset{1-1 onto}{⟶} ℋ \land (x \in ℋ \land y \in ℋ)) \to T (T^{-1} (x)) \cdot_{ih} T (T^{-1} (y)) = x \cdot_{ih} y$
20	1 19	sylan	$⊢ (T \in UniOp \land (x \in ℋ \land y \in ℋ)) \to T (T^{-1} (x)) \cdot_{ih} T (T^{-1} (y)) = x \cdot_{ih} y$
21	14 20	eqtr3d	$⊢ (T \in UniOp \land (x \in ℋ \land y \in ℋ)) \to T^{-1} (x) \cdot_{ih} T^{-1} (y) = x \cdot_{ih} y$
22	21	ralrimivva	$⊢ T \in UniOp \to \forall x \in ℋ \forall y \in ℋ T^{-1} (x) \cdot_{ih} T^{-1} (y) = x \cdot_{ih} y$
23		elunop	$⊢ T^{-1} \in UniOp \leftrightarrow (T^{-1} : ℋ \underset{onto}{⟶} ℋ \land \forall x \in ℋ \forall y \in ℋ T^{-1} (x) \cdot_{ih} T^{-1} (y) = x \cdot_{ih} y)$
24	5 22 23	sylanbrc	$⊢ T \in UniOp \to T^{-1} \in UniOp$

Metamath Proof Explorer

Theorem cnvunop

Proof