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 ( 𝑇 ∈ UniOp → 𝑇 : ℋ –1-1-onto→ ℋ )

Proof

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