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ℋ ∧ 𝑇 ∈ UniOp ) → ( normop ‘ 𝑇 ) = 1 )

Proof

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