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→normop⁡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:ℋ⟶ℋ→normop⁡T=supx|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yℝ*<
5 3 4 syl ⊢T∈UniOp→normop⁡T=supx|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yℝ*<
6 5 adantl ⊢ℋ≠0ℋ∧T∈UniOp→normop⁡T=supx|∃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⁡yz≤1
29 28 adantl ⊢ℋ≠0ℋ∧T∈UniOp→∀z∈x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yz≤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⁡yz<w
57 54 56 sylan ⊢ℋ≠0ℋ∧T∈UniOp∧z∈ℝ∧z<1→∃w∈x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yz<w
58 57 ex ⊢ℋ≠0ℋ∧T∈UniOp∧z∈ℝ→z<1→∃w∈x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yz<w
59 58 ralrimiva ⊢ℋ≠0ℋ∧T∈UniOp→∀z∈ℝz<1→∃w∈x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yz<w
60 supxr2 ⊢x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡y⊆ℝ*∧1∈ℝ*∧∀z∈x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yz≤1∧∀z∈ℝz<1→∃w∈x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yz<w→supx|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yℝ*<=1
61 13 29 59 60 syl12anc ⊢ℋ≠0ℋ∧T∈UniOp→supx|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡T⁡yℝ*<=1
62 6 61 eqtrd ⊢ℋ≠0ℋ∧T∈UniOp→normop⁡T=1