Metamath Proof Explorer

Theorem 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 ∈ UniOp → T -1 ∈ UniOp

Proof

Step Hyp Ref Expression
1 unopf1o ⊢ T ∈ UniOp → T : ℋ ⟶ 1-1 onto ℋ
2 f1ocnv ⊢ T : ℋ ⟶ 1-1 onto ℋ → T -1 : ℋ ⟶ 1-1 onto ℋ
3 f1ofo ⊢ T -1 : ℋ ⟶ 1-1 onto ℋ → T -1 : ℋ ⟶ onto ℋ
4 2 3 syl ⊢ T : ℋ ⟶ 1-1 onto ℋ → T -1 : ℋ ⟶ onto ℋ
5 1 4 syl ⊢ T ∈ UniOp → T -1 : ℋ ⟶ onto ℋ
6 simpl ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ∈ UniOp
7 fof ⊢ T -1 : ℋ ⟶ onto ℋ → T -1 : ℋ ⟶ ℋ
8 5 7 syl ⊢ T ∈ UniOp → T -1 : ℋ ⟶ ℋ
9 8 ffvelcdmda ⊢ T ∈ UniOp ∧ x ∈ ℋ → T -1 ⁡ x ∈ ℋ
10 9 adantrr ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T -1 ⁡ x ∈ ℋ
11 8 ffvelcdmda ⊢ T ∈ UniOp ∧ y ∈ ℋ → T -1 ⁡ y ∈ ℋ
12 11 adantrl ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T -1 ⁡ y ∈ ℋ
13 unop ⊢ T ∈ UniOp ∧ T -1 ⁡ x ∈ ℋ ∧ T -1 ⁡ y ∈ ℋ → T ⁡ T -1 ⁡ x ⋅ ih T ⁡ T -1 ⁡ y = T -1 ⁡ x ⋅ ih T -1 ⁡ y
14 6 10 12 13 syl3anc ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ T -1 ⁡ x ⋅ ih T ⁡ T -1 ⁡ y = T -1 ⁡ x ⋅ ih T -1 ⁡ y
15 f1ocnvfv2 ⊢ T : ℋ ⟶ 1-1 onto ℋ ∧ x ∈ ℋ → T ⁡ T -1 ⁡ x = x
16 15 adantrr ⊢ T : ℋ ⟶ 1-1 onto ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ T -1 ⁡ x = x
17 f1ocnvfv2 ⊢ T : ℋ ⟶ 1-1 onto ℋ ∧ y ∈ ℋ → T ⁡ T -1 ⁡ y = y
18 17 adantrl ⊢ T : ℋ ⟶ 1-1 onto ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ T -1 ⁡ y = y
19 16 18 oveq12d ⊢ T : ℋ ⟶ 1-1 onto ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ T -1 ⁡ x ⋅ ih T ⁡ T -1 ⁡ y = x ⋅ ih y
20 1 19 sylan ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ T -1 ⁡ x ⋅ ih T ⁡ T -1 ⁡ y = x ⋅ ih y
21 14 20 eqtr3d ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T -1 ⁡ x ⋅ ih T -1 ⁡ y = x ⋅ ih y
22 21 ralrimivva ⊢ T ∈ UniOp → ∀ x ∈ ℋ ∀ y ∈ ℋ T -1 ⁡ x ⋅ ih T -1 ⁡ y = x ⋅ ih y
23 elunop ⊢ T -1 ∈ UniOp ↔ T -1 : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T -1 ⁡ x ⋅ ih T -1 ⁡ y = x ⋅ ih y
24 5 22 23 sylanbrc ⊢ T ∈ UniOp → T -1 ∈ UniOp