# 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}\in {\mathbf{C}}_{ℋ}$
Assertion pjnmopi ${⊢}{H}\ne {0}_{ℋ}\to {norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\right)=1$

### Proof

Step Hyp Ref Expression
1 pjhmop.1 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
2 1 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ$
3 nmopval ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ\to {norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\right)=sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
4 2 3 ax-mp ${⊢}{norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\right)=sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
5 vex ${⊢}{z}\in \mathrm{V}$
6 eqeq1 ${⊢}{x}={z}\to \left({x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)↔{z}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)$
7 6 anbi2d ${⊢}{x}={z}\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)↔\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {z}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right)$
8 7 rexbidv ${⊢}{x}={z}\to \left(\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {z}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right)$
9 5 8 elab ${⊢}{z}\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {z}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)$
10 pjnorm ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {y}\in ℋ\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\le {norm}_{ℎ}\left({y}\right)$
11 1 10 mpan ${⊢}{y}\in ℋ\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\le {norm}_{ℎ}\left({y}\right)$
12 1 pjhcli ${⊢}{y}\in ℋ\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\in ℋ$
13 normcl ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\in ℋ\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\in ℝ$
14 12 13 syl ${⊢}{y}\in ℋ\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\in ℝ$
15 normcl ${⊢}{y}\in ℋ\to {norm}_{ℎ}\left({y}\right)\in ℝ$
16 1re ${⊢}1\in ℝ$
17 letr ${⊢}\left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\in ℝ\wedge {norm}_{ℎ}\left({y}\right)\in ℝ\wedge 1\in ℝ\right)\to \left(\left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\le {norm}_{ℎ}\left({y}\right)\wedge {norm}_{ℎ}\left({y}\right)\le 1\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\le 1\right)$
18 16 17 mp3an3 ${⊢}\left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\in ℝ\wedge {norm}_{ℎ}\left({y}\right)\in ℝ\right)\to \left(\left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\le {norm}_{ℎ}\left({y}\right)\wedge {norm}_{ℎ}\left({y}\right)\le 1\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\le 1\right)$
19 14 15 18 syl2anc ${⊢}{y}\in ℋ\to \left(\left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\le {norm}_{ℎ}\left({y}\right)\wedge {norm}_{ℎ}\left({y}\right)\le 1\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\le 1\right)$
20 11 19 mpand ${⊢}{y}\in ℋ\to \left({norm}_{ℎ}\left({y}\right)\le 1\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\le 1\right)$
21 20 imp ${⊢}\left({y}\in ℋ\wedge {norm}_{ℎ}\left({y}\right)\le 1\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\le 1$
22 breq1 ${⊢}{z}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\to \left({z}\le 1↔{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\le 1\right)$
23 22 biimparc ${⊢}\left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\le 1\wedge {z}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\to {z}\le 1$
24 21 23 sylan ${⊢}\left(\left({y}\in ℋ\wedge {norm}_{ℎ}\left({y}\right)\le 1\right)\wedge {z}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\to {z}\le 1$
25 24 expl ${⊢}{y}\in ℋ\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {z}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\to {z}\le 1\right)$
26 25 rexlimiv ${⊢}\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {z}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\to {z}\le 1$
27 9 26 sylbi ${⊢}{z}\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}\to {z}\le 1$
28 27 rgen ${⊢}\forall {z}\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}\le 1$
29 1 cheli ${⊢}{y}\in {H}\to {y}\in ℋ$
30 29 adantr ${⊢}\left({y}\in {H}\wedge {norm}_{ℎ}\left({y}\right)=1\right)\to {y}\in ℋ$
31 29 15 syl ${⊢}{y}\in {H}\to {norm}_{ℎ}\left({y}\right)\in ℝ$
32 eqle ${⊢}\left({norm}_{ℎ}\left({y}\right)\in ℝ\wedge {norm}_{ℎ}\left({y}\right)=1\right)\to {norm}_{ℎ}\left({y}\right)\le 1$
33 31 32 sylan ${⊢}\left({y}\in {H}\wedge {norm}_{ℎ}\left({y}\right)=1\right)\to {norm}_{ℎ}\left({y}\right)\le 1$
34 pjid ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {y}\in {H}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)={y}$
35 1 34 mpan ${⊢}{y}\in {H}\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)={y}$
36 35 fveq2d ${⊢}{y}\in {H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)$
37 36 adantr ${⊢}\left({y}\in {H}\wedge {norm}_{ℎ}\left({y}\right)=1\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)$
38 simpr ${⊢}\left({y}\in {H}\wedge {norm}_{ℎ}\left({y}\right)=1\right)\to {norm}_{ℎ}\left({y}\right)=1$
39 37 38 eqtr2d ${⊢}\left({y}\in {H}\wedge {norm}_{ℎ}\left({y}\right)=1\right)\to 1={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)$
40 30 33 39 jca32 ${⊢}\left({y}\in {H}\wedge {norm}_{ℎ}\left({y}\right)=1\right)\to \left({y}\in ℋ\wedge \left({norm}_{ℎ}\left({y}\right)\le 1\wedge 1={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right)$
41 40 reximi2 ${⊢}\exists {y}\in {H}\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({y}\right)=1\to \exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge 1={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)$
42 1 chne0i ${⊢}{H}\ne {0}_{ℋ}↔\exists {y}\in {H}\phantom{\rule{.4em}{0ex}}{y}\ne {0}_{ℎ}$
43 1 chshii ${⊢}{H}\in {\mathbf{S}}_{ℋ}$
44 43 norm1exi ${⊢}\exists {y}\in {H}\phantom{\rule{.4em}{0ex}}{y}\ne {0}_{ℎ}↔\exists {y}\in {H}\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({y}\right)=1$
45 42 44 bitri ${⊢}{H}\ne {0}_{ℋ}↔\exists {y}\in {H}\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({y}\right)=1$
46 1ex ${⊢}1\in \mathrm{V}$
47 eqeq1 ${⊢}{x}=1\to \left({x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)↔1={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)$
48 47 anbi2d ${⊢}{x}=1\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)↔\left({norm}_{ℎ}\left({y}\right)\le 1\wedge 1={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right)$
49 48 rexbidv ${⊢}{x}=1\to \left(\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge 1={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right)$
50 46 49 elab ${⊢}1\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge 1={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)$
51 41 45 50 3imtr4i ${⊢}{H}\ne {0}_{ℋ}\to 1\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}$
52 breq2 ${⊢}{w}=1\to \left({z}<{w}↔{z}<1\right)$
53 52 rspcev ${⊢}\left(1\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}\wedge {z}<1\right)\to \exists {w}\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}<{w}$
54 51 53 sylan ${⊢}\left({H}\ne {0}_{ℋ}\wedge {z}<1\right)\to \exists {w}\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}<{w}$
55 54 ex ${⊢}{H}\ne {0}_{ℋ}\to \left({z}<1\to \exists {w}\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}<{w}\right)$
56 55 ralrimivw ${⊢}{H}\ne {0}_{ℋ}\to \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<1\to \exists {w}\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}<{w}\right)$
57 nmopsetretHIL ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ\to \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}\subseteq ℝ$
58 2 57 ax-mp ${⊢}\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}\subseteq ℝ$
59 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
60 58 59 sstri ${⊢}\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}\subseteq {ℝ}^{*}$
61 1xr ${⊢}1\in {ℝ}^{*}$
62 supxr2 ${⊢}\left(\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}\subseteq {ℝ}^{*}\wedge 1\in {ℝ}^{*}\right)\wedge \left(\forall {z}\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}\le 1\wedge \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<1\to \exists {w}\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}<{w}\right)\right)\right)\to sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)=1$
63 60 61 62 mpanl12 ${⊢}\left(\forall {z}\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}\le 1\wedge \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left({z}<1\to \exists {w}\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}<{w}\right)\right)\to sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)=1$
64 28 56 63 sylancr ${⊢}{H}\ne {0}_{ℋ}\to sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)=1$
65 4 64 syl5eq ${⊢}{H}\ne {0}_{ℋ}\to {norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\right)=1$