Theorem pjnmop 10070

Description: The operator norm of a projector on a non-zero closed subspace is one. Part of Theorem 26.1 of [Halmos] p. 43.

Hypothesis

Ref	Expression
pjhmop.1	|- H e. CH

Assertion

Ref	Expression
pjnmop	|- (H =/= 0H -> (normop` (proj` H)) = 1)

Proof of Theorem pjnmop

Step	Hyp	Ref	Expression
1		breq2 2628	. . . . . . . 8 |- (w = 1 -> (z < w <-> z < 1))
2	1	rcla4ev 1880	. . . . . . 7 |- ((1 e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` ((proj` H)` y)))} /\ z < 1) -> E.w e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` ((proj` H)` y)))}z < w)
3		pjhmop.1	. . . . . . . . . . . 12 |- H e. CH
4	3	chel 9097	. . . . . . . . . . 11 |- (y e. H -> y e. H~)
5	4	adantr 391	. . . . . . . . . 10 |- ((y e. H /\ (normh` y) = 1) -> y e. H~)
6		eqlet 5583	. . . . . . . . . . . 12 |- (((normh` y) e. RR /\ (normh` y) = 1) -> (normh` y) <_ 1)
7		normclt 8986	. . . . . . . . . . . . 13 |- (y e. H~ -> (normh` y) e. RR)
8	4, 7	syl 10	. . . . . . . . . . . 12 |- (y e. H -> (normh` y) e. RR)
9	6, 8	sylan 450	. . . . . . . . . . 11 |- ((y e. H /\ (normh` y) = 1) -> (normh` y) <_ 1)
10		pjidt 9635	. . . . . . . . . . . . . . 15 |- ((H e. CH /\ y e. H) -> ((proj` H)` y) = y)
11	3, 10	mpan 697	. . . . . . . . . . . . . 14 |- (y e. H -> ((proj` H)` y) = y)
12	11	fveq2d 3734	. . . . . . . . . . . . 13 |- (y e. H -> (normh` ((proj` H)` y)) = (normh` y))
13	12	adantr 391	. . . . . . . . . . . 12 |- ((y e. H /\ (normh` y) = 1) -> (normh` ((proj` H)` y)) = (normh` y))
14		pm3.27 323	. . . . . . . . . . . 12 |- ((y e. H /\ (normh` y) = 1) -> (normh` y) = 1)
15	13, 14	eqtr2d 1511	. . . . . . . . . . 11 |- ((y e. H /\ (normh` y) = 1) -> 1 = (normh` ((proj` H)` y)))
16	9, 15	jca 288	. . . . . . . . . 10 |- ((y e. H /\ (normh` y) = 1) -> ((normh` y) <_ 1 /\ 1 = (normh` ((proj` H)` y))))
17	5, 16	jca 288	. . . . . . . . 9 |- ((y e. H /\ (normh` y) = 1) -> (y e. H~ /\ ((normh` y) <_ 1 /\ 1 = (normh` ((proj` H)` y)))))
18	17	r19.22i2 1736	. . . . . . . 8 |- (E.y e. H (normh` y) = 1 -> E.y e. H~ ((normh` y) <_ 1 /\ 1 = (normh` ((proj` H)` y))))
19	3	chne0 9371	. . . . . . . . 9 |- (H =/= 0H <-> E.y e. H y =/= 0h)
20	3	chshi 9092	. . . . . . . . . 10 |- H e. SH
21	20	norm1ex 9117	. . . . . . . . 9 |- (E.y e. H y =/= 0h <-> E.y e. H (normh` y) = 1)
22	19, 21	bitr 173	. . . . . . . 8 |- (H =/= 0H <-> E.y e. H (normh` y) = 1)
23		1re 5447	. . . . . . . . . 10 |- 1 e. RR
24	23	elisseti 1821	. . . . . . . . 9 |- 1 e. V
25		eqeq1 1484	. . . . . . . . . . 11 |- (x = 1 -> (x = (normh` ((proj` H)` y)) <-> 1 = (normh` ((proj` H)` y))))
26	25	anbi2d 618	. . . . . . . . . 10 |- (x = 1 -> (((normh` y) <_ 1 /\ x = (normh` ((proj` H)` y))) <-> ((normh` y) <_ 1 /\ 1 = (normh` ((proj` H)` y)))))
27	26	rexbidv 1667	. . . . . . . . 9 |- (x = 1 -> (E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` ((proj` H)` y))) <-> E.y e. H~ ((normh` y) <_ 1 /\ 1 = (normh` ((proj` H)` y)))))
28	24, 27	elab 1900	. . . . . . . 8 |- (1 e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` ((proj` H)` y)))} <-> E.y e. H~ ((normh` y) <_ 1 /\ 1 = (normh` ((proj` H)` y))))
29	18, 22, 28	3imtr4 219	. . . . . . 7 |- (H =/= 0H -> 1 e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` ((proj` H)` y)))})
30	2, 29	sylan 450	. . . . . 6 |- ((H =/= 0H /\ z < 1) -> E.w e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` ((proj` H)` y)))}z < w)
31	30	ex 373	. . . . 5 |- (H =/= 0H -> (z < 1 -> E.w e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` ((proj` H)` y)))}z < w))
32	31	a1d 12	. . . 4 |- (H =/= 0H -> (z e. RR -> (z < 1 -> E.w e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` ((proj` H)` y)))}z < w)))
33	32	r19.21aiv 1716	. . 3 |- (H =/= 0H -> A.z e. RR (z < 1 -> E.w e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` ((proj` H)` y)))}z < w))
34		visset 1816	. . . . . . 7 |- z e. V
35		eqeq1 1484	. . . . . . . . 9 |- (x = z -> (x = (normh` ((proj` H)` y)) <-> z = (normh` ((proj` H)` y))))
36	35	anbi2d 618	. . . . . . . 8 |- (x = z -> (((normh` y) <_ 1 /\ x = (normh` ((proj` H)` y))) <-> ((normh` y) <_ 1 /\ z = (normh` ((proj` H)` y)))))
37	36	rexbidv 1667	. . . . . . 7 |- (x = z -> (E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` ((proj` H)` y))) <-> E.y e. H~ ((normh` y) <_ 1 /\ z = (normh` ((proj` H)` y)))))
38	34, 37	elab 1900	. . . . . 6 |- (z e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` ((proj` H)` y)))} <-> E.y e. H~ ((normh` y) <_ 1 /\ z = (normh` ((proj` H)` y))))
39		breq1 2627	. . . . . . . . . . 11 |- (z = (normh` ((proj` H)` y)) -> (z <_ 1 <-> (normh` ((proj` H)` y)) <_ 1))
40	39	biimparc 421	. . . . . . . . . 10 |- (((normh` ((proj` H)` y)) <_ 1 /\ z = (normh` ((proj` H)` y))) -> z <_ 1)
41		pjnormt 9664	. . . . . . . . . . . . 13 |- ((H e. CH /\ y e. H~) -> (normh` ((proj` H)` y)) <_ (normh` y))
42	3, 41	mpan 697	. . . . . . . . . . . 12 |- (y e. H~ -> (normh` ((proj` H)` y)) <_ (normh` y))
43		letrt 5537	. . . . . . . . . . . . . 14 |- (((normh` ((proj` H)` y)) e. RR /\ (normh` y) e. RR /\ 1 e. RR) -> (((normh` ((proj` H)` y)) <_ (normh` y) /\ (normh` y) <_ 1) -> (normh` ((proj` H)` y)) <_ 1))
44	23, 43	mp3an3 907	. . . . . . . . . . . . 13 |- (((normh` ((proj` H)` y)) e. RR /\ (normh` y) e. RR) -> (((normh` ((proj` H)` y)) <_ (normh` y) /\ (normh` y) <_ 1) -> (normh` ((proj` H)` y)) <_ 1))
45	3	pjhcl 9247	. . . . . . . . . . . . . 14 |- (y e. H~ -> ((proj` H)` y) e. H~)
46		normclt 8986	. . . . . . . . . . . . . 14 |- (((proj` H)` y) e. H~ -> (normh` ((proj` H)` y)) e. RR)
47	45, 46	syl 10	. . . . . . . . . . . . 13 |- (y e. H~ -> (normh` ((proj` H)` y)) e. RR)
48	44, 47, 7	sylanc 473	. . . . . . . . . . . 12 |- (y e. H~ -> (((normh` ((proj` H)` y)) <_ (normh` y) /\ (normh` y) <_ 1) -> (normh` ((proj` H)` y)) <_ 1))
49	42, 48	mpand 703	. . . . . . . . . . 11 |- (y e. H~ -> ((normh` y) <_ 1 -> (normh` ((proj` H)` y)) <_ 1))
50	49	imp 350	. . . . . . . . . 10 |- ((y e. H~ /\ (normh` y) <_ 1) -> (normh` ((proj` H)` y)) <_ 1)
51	40, 50	sylan 450	. . . . . . . . 9 |- (((y e. H~ /\ (normh` y) <_ 1) /\ z = (normh` ((proj` H)` y))) -> z <_ 1)
52	51	exp31 378	. . . . . . . 8 |- (y e. H~ -> ((normh` y) <_ 1 -> (z = (normh` ((proj` H)` y)) -> z <_ 1)))
53	52	imp3a 361	. . . . . . 7 |- (y e. H~ -> (((normh` y) <_ 1 /\ z = (normh` ((proj` H)` y))) -> z <_ 1))
54	53	r19.23aiv 1746	. . . . . 6 |- (E.y e. H~ ((normh` y) <_ 1 /\ z = (normh` ((proj` H)` y))) -> z <_ 1)
55	38, 54	sylbi 199	. . . . 5 |- (z e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` ((proj` H)` y)))} -> z <_ 1)
56	55	rgen 1701	. . . 4 |- A.z e. {x | E.y e. H~ ((normh` y) <_ 1 /\ x = (normh` ((proj` H)` y)))}z <_ 1
57	3	pjf 9644	. . . . . . 7 |- (proj` H):H~-->H~
58		nmopsetretHIL 9786