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 ⊢H∈Cℋ
Assertion pjnmopi ⊢H≠0ℋ→normop⁡projℎ⁡H=1

Proof

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