Metamath Proof Explorer

Theorem unopf1o

Description: A unitary operator in Hilbert space is one-to-one and onto. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion unopf1o ⊢ T ∈ UniOp → T : ℋ ⟶ 1-1 onto ℋ

Proof

Step Hyp Ref Expression
1 elunop ⊢ T ∈ UniOp ↔ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y
2 1 simplbi ⊢ T ∈ UniOp → T : ℋ ⟶ onto ℋ
3 fof ⊢ T : ℋ ⟶ onto ℋ → T : ℋ ⟶ ℋ
4 2 3 syl ⊢ T ∈ UniOp → T : ℋ ⟶ ℋ
5 unop ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ x ∈ ℋ → T ⁡ x ⋅ ih T ⁡ x = x ⋅ ih x
6 5 3anidm23 ⊢ T ∈ UniOp ∧ x ∈ ℋ → T ⁡ x ⋅ ih T ⁡ x = x ⋅ ih x
7 6 3adant3 ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ⋅ ih T ⁡ x = x ⋅ ih x
8 unop ⊢ T ∈ UniOp ∧ y ∈ ℋ ∧ y ∈ ℋ → T ⁡ y ⋅ ih T ⁡ y = y ⋅ ih y
9 8 3anidm23 ⊢ T ∈ UniOp ∧ y ∈ ℋ → T ⁡ y ⋅ ih T ⁡ y = y ⋅ ih y
10 9 3adant2 ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ y ⋅ ih T ⁡ y = y ⋅ ih y
11 7 10 oveq12d ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ⋅ ih T ⁡ x + T ⁡ y ⋅ ih T ⁡ y = x ⋅ ih x + y ⋅ ih y
12 unop ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y
13 unop ⊢ T ∈ UniOp ∧ y ∈ ℋ ∧ x ∈ ℋ → T ⁡ y ⋅ ih T ⁡ x = y ⋅ ih x
14 13 3com23 ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ y ⋅ ih T ⁡ x = y ⋅ ih x
15 12 14 oveq12d ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ⋅ ih T ⁡ y + T ⁡ y ⋅ ih T ⁡ x = x ⋅ ih y + y ⋅ ih x
16 11 15 oveq12d ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ⋅ ih T ⁡ x + T ⁡ y ⋅ ih T ⁡ y - T ⁡ x ⋅ ih T ⁡ y + T ⁡ y ⋅ ih T ⁡ x = x ⋅ ih x + y ⋅ ih y - x ⋅ ih y + y ⋅ ih x
17 16 3expb ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ⋅ ih T ⁡ x + T ⁡ y ⋅ ih T ⁡ y - T ⁡ x ⋅ ih T ⁡ y + T ⁡ y ⋅ ih T ⁡ x = x ⋅ ih x + y ⋅ ih y - x ⋅ ih y + y ⋅ ih x
18 ffvelcdm ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → T ⁡ x ∈ ℋ
19 ffvelcdm ⊢ T : ℋ ⟶ ℋ ∧ y ∈ ℋ → T ⁡ y ∈ ℋ
20 18 19 anim12dan ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ∈ ℋ ∧ T ⁡ y ∈ ℋ
21 4 20 sylan ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ∈ ℋ ∧ T ⁡ y ∈ ℋ
22 normlem9at ⊢ T ⁡ x ∈ ℋ ∧ T ⁡ y ∈ ℋ → T ⁡ x - ℎ T ⁡ y ⋅ ih T ⁡ x - ℎ T ⁡ y = T ⁡ x ⋅ ih T ⁡ x + T ⁡ y ⋅ ih T ⁡ y - T ⁡ x ⋅ ih T ⁡ y + T ⁡ y ⋅ ih T ⁡ x
23 21 22 syl ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x - ℎ T ⁡ y ⋅ ih T ⁡ x - ℎ T ⁡ y = T ⁡ x ⋅ ih T ⁡ x + T ⁡ y ⋅ ih T ⁡ y - T ⁡ x ⋅ ih T ⁡ y + T ⁡ y ⋅ ih T ⁡ x
24 normlem9at ⊢ x ∈ ℋ ∧ y ∈ ℋ → x - ℎ y ⋅ ih x - ℎ y = x ⋅ ih x + y ⋅ ih y - x ⋅ ih y + y ⋅ ih x
25 24 adantl ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x - ℎ y ⋅ ih x - ℎ y = x ⋅ ih x + y ⋅ ih y - x ⋅ ih y + y ⋅ ih x
26 17 23 25 3eqtr4rd ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x - ℎ y ⋅ ih x - ℎ y = T ⁡ x - ℎ T ⁡ y ⋅ ih T ⁡ x - ℎ T ⁡ y
27 26 eqeq1d ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x - ℎ y ⋅ ih x - ℎ y = 0 ↔ T ⁡ x - ℎ T ⁡ y ⋅ ih T ⁡ x - ℎ T ⁡ y = 0
28 hvsubcl ⊢ x ∈ ℋ ∧ y ∈ ℋ → x - ℎ y ∈ ℋ
29 his6 ⊢ x - ℎ y ∈ ℋ → x - ℎ y ⋅ ih x - ℎ y = 0 ↔ x - ℎ y = 0 ℎ
30 28 29 syl ⊢ x ∈ ℋ ∧ y ∈ ℋ → x - ℎ y ⋅ ih x - ℎ y = 0 ↔ x - ℎ y = 0 ℎ
31 hvsubeq0 ⊢ x ∈ ℋ ∧ y ∈ ℋ → x - ℎ y = 0 ℎ ↔ x = y
32 30 31 bitrd ⊢ x ∈ ℋ ∧ y ∈ ℋ → x - ℎ y ⋅ ih x - ℎ y = 0 ↔ x = y
33 32 adantl ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x - ℎ y ⋅ ih x - ℎ y = 0 ↔ x = y
34 hvsubcl ⊢ T ⁡ x ∈ ℋ ∧ T ⁡ y ∈ ℋ → T ⁡ x - ℎ T ⁡ y ∈ ℋ
35 his6 ⊢ T ⁡ x - ℎ T ⁡ y ∈ ℋ → T ⁡ x - ℎ T ⁡ y ⋅ ih T ⁡ x - ℎ T ⁡ y = 0 ↔ T ⁡ x - ℎ T ⁡ y = 0 ℎ
36 34 35 syl ⊢ T ⁡ x ∈ ℋ ∧ T ⁡ y ∈ ℋ → T ⁡ x - ℎ T ⁡ y ⋅ ih T ⁡ x - ℎ T ⁡ y = 0 ↔ T ⁡ x - ℎ T ⁡ y = 0 ℎ
37 hvsubeq0 ⊢ T ⁡ x ∈ ℋ ∧ T ⁡ y ∈ ℋ → T ⁡ x - ℎ T ⁡ y = 0 ℎ ↔ T ⁡ x = T ⁡ y
38 36 37 bitrd ⊢ T ⁡ x ∈ ℋ ∧ T ⁡ y ∈ ℋ → T ⁡ x - ℎ T ⁡ y ⋅ ih T ⁡ x - ℎ T ⁡ y = 0 ↔ T ⁡ x = T ⁡ y
39 21 38 syl ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x - ℎ T ⁡ y ⋅ ih T ⁡ x - ℎ T ⁡ y = 0 ↔ T ⁡ x = T ⁡ y
40 27 33 39 3bitr3rd ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x = T ⁡ y ↔ x = y
41 40 biimpd ⊢ T ∈ UniOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x = T ⁡ y → x = y
42 41 ralrimivva ⊢ T ∈ UniOp → ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x = T ⁡ y → x = y
43 dff13 ⊢ T : ℋ ⟶ 1-1 ℋ ↔ T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x = T ⁡ y → x = y
44 4 42 43 sylanbrc ⊢ T ∈ UniOp → T : ℋ ⟶ 1-1 ℋ
45 df-f1o ⊢ T : ℋ ⟶ 1-1 onto ℋ ↔ T : ℋ ⟶ 1-1 ℋ ∧ T : ℋ ⟶ onto ℋ
46 44 2 45 sylanbrc ⊢ T ∈ UniOp → T : ℋ ⟶ 1-1 onto ℋ