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⋅ihT⁡y=x⋅ihy
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⋅ihT⁡x=x⋅ihx
6 5 3anidm23 ⊢T∈UniOp∧x∈ℋ→T⁡x⋅ihT⁡x=x⋅ihx
7 6 3adant3 ⊢T∈UniOp∧x∈ℋ∧y∈ℋ→T⁡x⋅ihT⁡x=x⋅ihx
8 unop ⊢T∈UniOp∧y∈ℋ∧y∈ℋ→T⁡y⋅ihT⁡y=y⋅ihy
9 8 3anidm23 ⊢T∈UniOp∧y∈ℋ→T⁡y⋅ihT⁡y=y⋅ihy
10 9 3adant2 ⊢T∈UniOp∧x∈ℋ∧y∈ℋ→T⁡y⋅ihT⁡y=y⋅ihy
11 7 10 oveq12d ⊢T∈UniOp∧x∈ℋ∧y∈ℋ→T⁡x⋅ihT⁡x+T⁡y⋅ihT⁡y=x⋅ihx+y⋅ihy
12 unop ⊢T∈UniOp∧x∈ℋ∧y∈ℋ→T⁡x⋅ihT⁡y=x⋅ihy
13 unop ⊢T∈UniOp∧y∈ℋ∧x∈ℋ→T⁡y⋅ihT⁡x=y⋅ihx
14 13 3com23 ⊢T∈UniOp∧x∈ℋ∧y∈ℋ→T⁡y⋅ihT⁡x=y⋅ihx
15 12 14 oveq12d ⊢T∈UniOp∧x∈ℋ∧y∈ℋ→T⁡x⋅ihT⁡y+T⁡y⋅ihT⁡x=x⋅ihy+y⋅ihx
16 11 15 oveq12d ⊢T∈UniOp∧x∈ℋ∧y∈ℋ→T⁡x⋅ihT⁡x+T⁡y⋅ihT⁡y-T⁡x⋅ihT⁡y+T⁡y⋅ihT⁡x=x⋅ihx+y⋅ihy-x⋅ihy+y⋅ihx
17 16 3expb ⊢T∈UniOp∧x∈ℋ∧y∈ℋ→T⁡x⋅ihT⁡x+T⁡y⋅ihT⁡y-T⁡x⋅ihT⁡y+T⁡y⋅ihT⁡x=x⋅ihx+y⋅ihy-x⋅ihy+y⋅ihx
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⋅ihT⁡x-ℎT⁡y=T⁡x⋅ihT⁡x+T⁡y⋅ihT⁡y-T⁡x⋅ihT⁡y+T⁡y⋅ihT⁡x
23 21 22 syl ⊢T∈UniOp∧x∈ℋ∧y∈ℋ→T⁡x-ℎT⁡y⋅ihT⁡x-ℎT⁡y=T⁡x⋅ihT⁡x+T⁡y⋅ihT⁡y-T⁡x⋅ihT⁡y+T⁡y⋅ihT⁡x
24 normlem9at ⊢x∈ℋ∧y∈ℋ→x-ℎy⋅ihx-ℎy=x⋅ihx+y⋅ihy-x⋅ihy+y⋅ihx
25 24 adantl ⊢T∈UniOp∧x∈ℋ∧y∈ℋ→x-ℎy⋅ihx-ℎy=x⋅ihx+y⋅ihy-x⋅ihy+y⋅ihx
26 17 23 25 3eqtr4rd ⊢T∈UniOp∧x∈ℋ∧y∈ℋ→x-ℎy⋅ihx-ℎy=T⁡x-ℎT⁡y⋅ihT⁡x-ℎT⁡y
27 26 eqeq1d ⊢T∈UniOp∧x∈ℋ∧y∈ℋ→x-ℎy⋅ihx-ℎy=0↔T⁡x-ℎT⁡y⋅ihT⁡x-ℎT⁡y=0
28 hvsubcl ⊢x∈ℋ∧y∈ℋ→x-ℎy∈ℋ
29 his6 ⊢x-ℎy∈ℋ→x-ℎy⋅ihx-ℎy=0↔x-ℎy=0ℎ
30 28 29 syl ⊢x∈ℋ∧y∈ℋ→x-ℎy⋅ihx-ℎy=0↔x-ℎy=0ℎ
31 hvsubeq0 ⊢x∈ℋ∧y∈ℋ→x-ℎy=0ℎ↔x=y
32 30 31 bitrd ⊢x∈ℋ∧y∈ℋ→x-ℎy⋅ihx-ℎy=0↔x=y
33 32 adantl ⊢T∈UniOp∧x∈ℋ∧y∈ℋ→x-ℎy⋅ihx-ℎy=0↔x=y
34 hvsubcl ⊢T⁡x∈ℋ∧T⁡y∈ℋ→T⁡x-ℎT⁡y∈ℋ
35 his6 ⊢T⁡x-ℎT⁡y∈ℋ→T⁡x-ℎT⁡y⋅ihT⁡x-ℎT⁡y=0↔T⁡x-ℎT⁡y=0ℎ
36 34 35 syl ⊢T⁡x∈ℋ∧T⁡y∈ℋ→T⁡x-ℎT⁡y⋅ihT⁡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⋅ihT⁡x-ℎT⁡y=0↔T⁡x=T⁡y
39 21 38 syl ⊢T∈UniOp∧x∈ℋ∧y∈ℋ→T⁡x-ℎT⁡y⋅ihT⁡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ℋ