Metamath Proof Explorer

Theorem pjnmopi

Description: The operator norm of a projector on a nonzero closed subspace is one. Part of Theorem 26.1 of Halmos p. 43. (Contributed by NM, 9-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypothesis pjhmop.1 ⊢ 𝐻 ∈ Cℋ
Assertion pjnmopi ( 𝐻 ≠ 0ℋ → ( normop ‘ ( projℎ ‘ 𝐻 ) ) = 1 )

Proof

Step Hyp Ref Expression
1 pjhmop.1 ⊢ 𝐻 ∈ Cℋ
2 1 pjfi ⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ
3 nmopval ⊢ ( ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ → ( normop ‘ ( projℎ ‘ 𝐻 ) ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } , ℝ* , < ) )
4 2 3 ax-mp ⊢ ( normop ‘ ( projℎ ‘ 𝐻 ) ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } , ℝ* , < )
5 vex ⊢ 𝑧 ∈ V
6 eqeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ↔ 𝑧 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) )
7 6 anbi2d ⊢ ( 𝑥 = 𝑧 → ( ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) ↔ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑧 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) ) )
8 7 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) ↔ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑧 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) ) )
9 5 8 elab ⊢ ( 𝑧 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } ↔ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑧 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) )
10 pjnorm ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ≤ ( normℎ ‘ 𝑦 ) )
11 1 10 mpan ⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ≤ ( normℎ ‘ 𝑦 ) )
12 1 pjhcli ⊢ ( 𝑦 ∈ ℋ → ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ∈ ℋ )
13 normcl ⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ∈ ℝ )
14 12 13 syl ⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ∈ ℝ )
15 normcl ⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ 𝑦 ) ∈ ℝ )
16 1re ⊢ 1 ∈ ℝ
17 letr ⊢ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ∈ ℝ ∧ ( normℎ ‘ 𝑦 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ≤ ( normℎ ‘ 𝑦 ) ∧ ( normℎ ‘ 𝑦 ) ≤ 1 ) → ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ≤ 1 ) )
18 16 17 mp3an3 ⊢ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ∈ ℝ ∧ ( normℎ ‘ 𝑦 ) ∈ ℝ ) → ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ≤ ( normℎ ‘ 𝑦 ) ∧ ( normℎ ‘ 𝑦 ) ≤ 1 ) → ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ≤ 1 ) )
19 14 15 18 syl2anc ⊢ ( 𝑦 ∈ ℋ → ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ≤ ( normℎ ‘ 𝑦 ) ∧ ( normℎ ‘ 𝑦 ) ≤ 1 ) → ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ≤ 1 ) )
20 11 19 mpand ⊢ ( 𝑦 ∈ ℋ → ( ( normℎ ‘ 𝑦 ) ≤ 1 → ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ≤ 1 ) )
21 20 imp ⊢ ( ( 𝑦 ∈ ℋ ∧ ( normℎ ‘ 𝑦 ) ≤ 1 ) → ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ≤ 1 )
22 breq1 ⊢ ( 𝑧 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) → ( 𝑧 ≤ 1 ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ≤ 1 ) )
23 22 biimparc ⊢ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ≤ 1 ∧ 𝑧 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) → 𝑧 ≤ 1 )
24 21 23 sylan ⊢ ( ( ( 𝑦 ∈ ℋ ∧ ( normℎ ‘ 𝑦 ) ≤ 1 ) ∧ 𝑧 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) → 𝑧 ≤ 1 )
25 24 expl ⊢ ( 𝑦 ∈ ℋ → ( ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑧 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) → 𝑧 ≤ 1 ) )
26 25 rexlimiv ⊢ ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑧 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) → 𝑧 ≤ 1 )
27 9 26 sylbi ⊢ ( 𝑧 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } → 𝑧 ≤ 1 )
28 27 rgen ⊢ ∀ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } 𝑧 ≤ 1
29 1 cheli ⊢ ( 𝑦 ∈ 𝐻 → 𝑦 ∈ ℋ )
30 29 adantr ⊢ ( ( 𝑦 ∈ 𝐻 ∧ ( normℎ ‘ 𝑦 ) = 1 ) → 𝑦 ∈ ℋ )
31 29 15 syl ⊢ ( 𝑦 ∈ 𝐻 → ( normℎ ‘ 𝑦 ) ∈ ℝ )
32 eqle ⊢ ( ( ( normℎ ‘ 𝑦 ) ∈ ℝ ∧ ( normℎ ‘ 𝑦 ) = 1 ) → ( normℎ ‘ 𝑦 ) ≤ 1 )
33 31 32 sylan ⊢ ( ( 𝑦 ∈ 𝐻 ∧ ( normℎ ‘ 𝑦 ) = 1 ) → ( normℎ ‘ 𝑦 ) ≤ 1 )
34 pjid ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝑦 ∈ 𝐻 ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) = 𝑦 )
35 1 34 mpan ⊢ ( 𝑦 ∈ 𝐻 → ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) = 𝑦 )
36 35 fveq2d ⊢ ( 𝑦 ∈ 𝐻 → ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) = ( normℎ ‘ 𝑦 ) )
37 36 adantr ⊢ ( ( 𝑦 ∈ 𝐻 ∧ ( normℎ ‘ 𝑦 ) = 1 ) → ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) = ( normℎ ‘ 𝑦 ) )
38 simpr ⊢ ( ( 𝑦 ∈ 𝐻 ∧ ( normℎ ‘ 𝑦 ) = 1 ) → ( normℎ ‘ 𝑦 ) = 1 )
39 37 38 eqtr2d ⊢ ( ( 𝑦 ∈ 𝐻 ∧ ( normℎ ‘ 𝑦 ) = 1 ) → 1 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) )
40 30 33 39 jca32 ⊢ ( ( 𝑦 ∈ 𝐻 ∧ ( normℎ ‘ 𝑦 ) = 1 ) → ( 𝑦 ∈ ℋ ∧ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 1 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) ) )
41 40 reximi2 ⊢ ( ∃ 𝑦 ∈ 𝐻 ( normℎ ‘ 𝑦 ) = 1 → ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 1 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) )
42 1 chne0i ⊢ ( 𝐻 ≠ 0ℋ ↔ ∃ 𝑦 ∈ 𝐻 𝑦 ≠ 0ℎ )
43 1 chshii ⊢ 𝐻 ∈ Sℋ
44 43 norm1exi ⊢ ( ∃ 𝑦 ∈ 𝐻 𝑦 ≠ 0ℎ ↔ ∃ 𝑦 ∈ 𝐻 ( normℎ ‘ 𝑦 ) = 1 )
45 42 44 bitri ⊢ ( 𝐻 ≠ 0ℋ ↔ ∃ 𝑦 ∈ 𝐻 ( normℎ ‘ 𝑦 ) = 1 )
46 1ex ⊢ 1 ∈ V
47 eqeq1 ⊢ ( 𝑥 = 1 → ( 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ↔ 1 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) )
48 47 anbi2d ⊢ ( 𝑥 = 1 → ( ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) ↔ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 1 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) ) )
49 48 rexbidv ⊢ ( 𝑥 = 1 → ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) ↔ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 1 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) ) )
50 46 49 elab ⊢ ( 1 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } ↔ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 1 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) )
51 41 45 50 3imtr4i ⊢ ( 𝐻 ≠ 0ℋ → 1 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } )
52 breq2 ⊢ ( 𝑤 = 1 → ( 𝑧 < 𝑤 ↔ 𝑧 < 1 ) )
53 52 rspcev ⊢ ( ( 1 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } ∧ 𝑧 < 1 ) → ∃ 𝑤 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } 𝑧 < 𝑤 )
54 51 53 sylan ⊢ ( ( 𝐻 ≠ 0ℋ ∧ 𝑧 < 1 ) → ∃ 𝑤 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } 𝑧 < 𝑤 )
55 54 ex ⊢ ( 𝐻 ≠ 0ℋ → ( 𝑧 < 1 → ∃ 𝑤 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } 𝑧 < 𝑤 ) )
56 55 ralrimivw ⊢ ( 𝐻 ≠ 0ℋ → ∀ 𝑧 ∈ ℝ ( 𝑧 < 1 → ∃ 𝑤 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } 𝑧 < 𝑤 ) )
57 nmopsetretHIL ⊢ ( ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } ⊆ ℝ )
58 2 57 ax-mp ⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } ⊆ ℝ
59 ressxr ⊢ ℝ ⊆ ℝ*
60 58 59 sstri ⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } ⊆ ℝ*
61 1xr ⊢ 1 ∈ ℝ*
62 supxr2 ⊢ ( ( ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } ⊆ ℝ* ∧ 1 ∈ ℝ* ) ∧ ( ∀ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } 𝑧 ≤ 1 ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < 1 → ∃ 𝑤 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } 𝑧 < 𝑤 ) ) ) → sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } , ℝ* , < ) = 1 )
63 60 61 62 mpanl12 ⊢ ( ( ∀ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } 𝑧 ≤ 1 ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < 1 → ∃ 𝑤 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } 𝑧 < 𝑤 ) ) → sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } , ℝ* , < ) = 1 )
64 28 56 63 sylancr ⊢ ( 𝐻 ≠ 0ℋ → sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) ) } , ℝ* , < ) = 1 )
65 4 64 syl5eq ⊢ ( 𝐻 ≠ 0ℋ → ( normop ‘ ( projℎ ‘ 𝐻 ) ) = 1 )