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

Proof

Step	Hyp	Ref	Expression
1		pjhmop.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
3		nmopval	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}\to {norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)=sup\left(\left\{x|\exists y\in \mathscr{H}\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 \mathscr{H}\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)\leftrightarrow 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)\leftrightarrow \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 \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\right)\right)\leftrightarrow \exists y\in \mathscr{H}\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 \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\right)\right)\right\}\leftrightarrow \exists y\in \mathscr{H}\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}}_{\mathscr{H}}\wedge y\in \mathscr{H}\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\right)\le {norm}_{ℎ}\left(y\right)$$
11	1 10	mpan	$$⊢y\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\right)\le {norm}_{ℎ}\left(y\right)$$
12	1	pjhcli	$$⊢y\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\in \mathscr{H}$$
13		normcl	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\right)\in ℝ$$
14	12 13	syl	$$⊢y\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\right)\in ℝ$$
15		normcl	$$⊢y\in \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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\leftrightarrow {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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\right)\right)\right\}z\le 1$$
29	1	cheli	$$⊢y\in H\to y\in \mathscr{H}$$
30	29	adantr	$$⊢\left(y\in H\wedge {norm}_{ℎ}\left(y\right)=1\right)\to y\in \mathscr{H}$$
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}}_{\mathscr{H}}\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 \mathscr{H}\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{norm}_{ℎ}\left(y\right)=1\to \exists y\in \mathscr{H}\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_{\mathscr{H}}\leftrightarrow \exists y\in Hy\ne 0_{ℎ}$$
43	1	chshii	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}$$
44	43	norm1exi	$$⊢\exists y\in Hy\ne 0_{ℎ}\leftrightarrow \exists y\in H{norm}_{ℎ}\left(y\right)=1$$
45	42 44	bitri	$$⊢H\ne 0_{\mathscr{H}}\leftrightarrow \exists y\in H{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)\leftrightarrow 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)\leftrightarrow \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 \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\right)\right)\leftrightarrow \exists y\in \mathscr{H}\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 \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\right)\right)\right\}\leftrightarrow \exists y\in \mathscr{H}\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_{\mathscr{H}}\to 1\in \left\{x|\exists y\in \mathscr{H}\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\leftrightarrow z<1\right)$$
53	52	rspcev	$$⊢\left(1\in \left\{x|\exists y\in \mathscr{H}\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 \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\right)\right)\right\}z<w$$
54	51 53	sylan	$$⊢\left(H\ne 0_{\mathscr{H}}\wedge z<1\right)\to \exists w\in \left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\right)\right)\right\}z<w$$
55	54	ex	$$⊢H\ne 0_{\mathscr{H}}\to \left(z<1\to \exists w\in \left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\right)\right)\right\}z<w\right)$$
56	55	ralrimivw	$$⊢H\ne 0_{\mathscr{H}}\to \forall z\in ℝ\left(z<1\to \exists w\in \left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\right)\right)\right\}z<w\right)$$
57		nmopsetretHIL	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}\to \left\{x|\exists y\in \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\right)\right)\right\}z\le 1\wedge \forall z\in ℝ\left(z<1\to \exists w\in \left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\right)\right)\right\}z<w\right)\right)\right)\to sup\left(\left\{x|\exists y\in \mathscr{H}\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 \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\right)\right)\right\}z\le 1\wedge \forall z\in ℝ\left(z<1\to \exists w\in \left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)\right)\right)\right\}z<w\right)\right)\to sup\left(\left\{x|\exists y\in \mathscr{H}\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_{\mathscr{H}}\to sup\left(\left\{x|\exists y\in \mathscr{H}\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_{\mathscr{H}}\to {norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)=1$$