Metamath Proof Explorer

Theorem nmopun

Description: Norm of a unitary Hilbert space operator. (Contributed by NM, 25-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopun ⊢ ℋ ≠ 0 ℋ ∧ T ∈ UniOp → norm op ⁡ T = 1

Proof

Step Hyp Ref Expression
1 unoplin ⊢ T ∈ UniOp → T ∈ LinOp
2 lnopf ⊢ T ∈ LinOp → T : ℋ ⟶ ℋ
3 1 2 syl ⊢ T ∈ UniOp → T : ℋ ⟶ ℋ
4 nmopval ⊢ T : ℋ ⟶ ℋ → norm op ⁡ T = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ℝ * <
5 3 4 syl ⊢ T ∈ UniOp → norm op ⁡ T = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ℝ * <
6 5 adantl ⊢ ℋ ≠ 0 ℋ ∧ T ∈ UniOp → norm op ⁡ T = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ℝ * <
7 nmopsetretHIL ⊢ T : ℋ ⟶ ℋ → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ⊆ ℝ
8 ressxr ⊢ ℝ ⊆ ℝ *
9 7 8 sstrdi ⊢ T : ℋ ⟶ ℋ → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ⊆ ℝ *
10 3 9 syl ⊢ T ∈ UniOp → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ⊆ ℝ *
11 10 adantl ⊢ ℋ ≠ 0 ℋ ∧ T ∈ UniOp → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ⊆ ℝ *
12 1xr ⊢ 1 ∈ ℝ *
13 11 12 jctir ⊢ ℋ ≠ 0 ℋ ∧ T ∈ UniOp → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ⊆ ℝ * ∧ 1 ∈ ℝ *
14 vex ⊢ z ∈ V
15 eqeq1 ⊢ x = z → x = norm ℎ ⁡ T ⁡ y ↔ z = norm ℎ ⁡ T ⁡ y
16 15 anbi2d ⊢ x = z → norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ↔ norm ℎ ⁡ y ≤ 1 ∧ z = norm ℎ ⁡ T ⁡ y
17 16 rexbidv ⊢ x = z → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ z = norm ℎ ⁡ T ⁡ y
18 14 17 elab ⊢ z ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ z = norm ℎ ⁡ T ⁡ y
19 unopnorm ⊢ T ∈ UniOp ∧ y ∈ ℋ → norm ℎ ⁡ T ⁡ y = norm ℎ ⁡ y
20 19 eqeq2d ⊢ T ∈ UniOp ∧ y ∈ ℋ → z = norm ℎ ⁡ T ⁡ y ↔ z = norm ℎ ⁡ y
21 20 anbi2d ⊢ T ∈ UniOp ∧ y ∈ ℋ → norm ℎ ⁡ y ≤ 1 ∧ z = norm ℎ ⁡ T ⁡ y ↔ norm ℎ ⁡ y ≤ 1 ∧ z = norm ℎ ⁡ y
22 breq1 ⊢ z = norm ℎ ⁡ y → z ≤ 1 ↔ norm ℎ ⁡ y ≤ 1
23 22 biimparc ⊢ norm ℎ ⁡ y ≤ 1 ∧ z = norm ℎ ⁡ y → z ≤ 1
24 21 23 syl6bi ⊢ T ∈ UniOp ∧ y ∈ ℋ → norm ℎ ⁡ y ≤ 1 ∧ z = norm ℎ ⁡ T ⁡ y → z ≤ 1
25 24 rexlimdva ⊢ T ∈ UniOp → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ z = norm ℎ ⁡ T ⁡ y → z ≤ 1
26 25 imp ⊢ T ∈ UniOp ∧ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ z = norm ℎ ⁡ T ⁡ y → z ≤ 1
27 18 26 sylan2b ⊢ T ∈ UniOp ∧ z ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y → z ≤ 1
28 27 ralrimiva ⊢ T ∈ UniOp → ∀ z ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y z ≤ 1
29 28 adantl ⊢ ℋ ≠ 0 ℋ ∧ T ∈ UniOp → ∀ z ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y z ≤ 1
30 hne0 ⊢ ℋ ≠ 0 ℋ ↔ ∃ y ∈ ℋ y ≠ 0 ℎ
31 norm1hex ⊢ ∃ y ∈ ℋ y ≠ 0 ℎ ↔ ∃ y ∈ ℋ norm ℎ ⁡ y = 1
32 30 31 sylbb ⊢ ℋ ≠ 0 ℋ → ∃ y ∈ ℋ norm ℎ ⁡ y = 1
33 32 adantr ⊢ ℋ ≠ 0 ℋ ∧ T ∈ UniOp → ∃ y ∈ ℋ norm ℎ ⁡ y = 1
34 1le1 ⊢ 1 ≤ 1
35 breq1 ⊢ norm ℎ ⁡ y = 1 → norm ℎ ⁡ y ≤ 1 ↔ 1 ≤ 1
36 34 35 mpbiri ⊢ norm ℎ ⁡ y = 1 → norm ℎ ⁡ y ≤ 1
37 36 a1i ⊢ T ∈ UniOp ∧ y ∈ ℋ → norm ℎ ⁡ y = 1 → norm ℎ ⁡ y ≤ 1
38 19 adantr ⊢ T ∈ UniOp ∧ y ∈ ℋ ∧ norm ℎ ⁡ y = 1 → norm ℎ ⁡ T ⁡ y = norm ℎ ⁡ y
39 eqeq2 ⊢ norm ℎ ⁡ y = 1 → norm ℎ ⁡ T ⁡ y = norm ℎ ⁡ y ↔ norm ℎ ⁡ T ⁡ y = 1
40 39 adantl ⊢ T ∈ UniOp ∧ y ∈ ℋ ∧ norm ℎ ⁡ y = 1 → norm ℎ ⁡ T ⁡ y = norm ℎ ⁡ y ↔ norm ℎ ⁡ T ⁡ y = 1
41 38 40 mpbid ⊢ T ∈ UniOp ∧ y ∈ ℋ ∧ norm ℎ ⁡ y = 1 → norm ℎ ⁡ T ⁡ y = 1
42 41 eqcomd ⊢ T ∈ UniOp ∧ y ∈ ℋ ∧ norm ℎ ⁡ y = 1 → 1 = norm ℎ ⁡ T ⁡ y
43 42 ex ⊢ T ∈ UniOp ∧ y ∈ ℋ → norm ℎ ⁡ y = 1 → 1 = norm ℎ ⁡ T ⁡ y
44 37 43 jcad ⊢ T ∈ UniOp ∧ y ∈ ℋ → norm ℎ ⁡ y = 1 → norm ℎ ⁡ y ≤ 1 ∧ 1 = norm ℎ ⁡ T ⁡ y
45 44 adantll ⊢ ℋ ≠ 0 ℋ ∧ T ∈ UniOp ∧ y ∈ ℋ → norm ℎ ⁡ y = 1 → norm ℎ ⁡ y ≤ 1 ∧ 1 = norm ℎ ⁡ T ⁡ y
46 45 reximdva ⊢ ℋ ≠ 0 ℋ ∧ T ∈ UniOp → ∃ y ∈ ℋ norm ℎ ⁡ y = 1 → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ 1 = norm ℎ ⁡ T ⁡ y
47 33 46 mpd ⊢ ℋ ≠ 0 ℋ ∧ T ∈ UniOp → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ 1 = norm ℎ ⁡ T ⁡ y
48 1ex ⊢ 1 ∈ V
49 eqeq1 ⊢ x = 1 → x = norm ℎ ⁡ T ⁡ y ↔ 1 = norm ℎ ⁡ T ⁡ y
50 49 anbi2d ⊢ x = 1 → norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ↔ norm ℎ ⁡ y ≤ 1 ∧ 1 = norm ℎ ⁡ T ⁡ y
51 50 rexbidv ⊢ x = 1 → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ 1 = norm ℎ ⁡ T ⁡ y
52 48 51 elab ⊢ 1 ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ↔ ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ 1 = norm ℎ ⁡ T ⁡ y
53 47 52 sylibr ⊢ ℋ ≠ 0 ℋ ∧ T ∈ UniOp → 1 ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y
54 53 adantr ⊢ ℋ ≠ 0 ℋ ∧ T ∈ UniOp ∧ z ∈ ℝ → 1 ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y
55 breq2 ⊢ w = 1 → z < w ↔ z < 1
56 55 rspcev ⊢ 1 ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ∧ z < 1 → ∃ w ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y z < w
57 54 56 sylan ⊢ ℋ ≠ 0 ℋ ∧ T ∈ UniOp ∧ z ∈ ℝ ∧ z < 1 → ∃ w ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y z < w
58 57 ex ⊢ ℋ ≠ 0 ℋ ∧ T ∈ UniOp ∧ z ∈ ℝ → z < 1 → ∃ w ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y z < w
59 58 ralrimiva ⊢ ℋ ≠ 0 ℋ ∧ T ∈ UniOp → ∀ z ∈ ℝ z < 1 → ∃ w ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y z < w
60 supxr2 ⊢ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ⊆ ℝ * ∧ 1 ∈ ℝ * ∧ ∀ z ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y z ≤ 1 ∧ ∀ z ∈ ℝ z < 1 → ∃ w ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y z < w → sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ℝ * < = 1
61 13 29 59 60 syl12anc ⊢ ℋ ≠ 0 ℋ ∧ T ∈ UniOp → sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ℝ * < = 1
62 6 61 eqtrd ⊢ ℋ ≠ 0 ℋ ∧ T ∈ UniOp → norm op ⁡ T = 1