# 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 )