Theorem hmopidmch 10017

Description: An idempotent Hermitian operator generates a closed subspace. Part of proof of Theorem of [AkhiezerGlazman] p. 64.

Hypotheses

Ref	Expression
hmopidmch.1	|- H = {x e. H~ | (T` x) = x}
hmopidmch.2	|- (T e. HrmOp /\ (T o. T) = T)

Assertion

Ref	Expression
hmopidmch	|- H e. CH

Distinct variable group:   x,T

Proof of Theorem hmopidmch

Step	Hyp	Ref	Expression
1		closedsub 9032	. 2 |- (H e. CH <-> (H e. SH /\ A.fA.y((f:NN-->H /\ f ~~>v y) -> y e. H)))
2		hmopidmch.1	. . . . 5 |- H = {x e. H~ | (T` x) = x}
3		ssrab2 2127	. . . . 5 |- {x e. H~ | (T` x) = x} (_ H~
4	2, 3	eqsstr 2087	. . . 4 |- H (_ H~
5		sh2 9030	. . . 4 |- (H (_ H~ -> (H e. SH <-> (0h e. H /\ (A.y e. H A.z e. H (y +h z) e. H /\ A.y e. CC A.z e. H (y .h z) e. H))))
6	4, 5	ax-mp 7	. . 3 |- (H e. SH <-> (0h e. H /\ (A.y e. H A.z e. H (y +h z) e. H /\ A.y e. CC A.z e. H (y .h z) e. H)))
7		fveq2 3715	. . . . . . 7 |- (x = 0h -> (T` x) = (T` 0h))
8		id 59	. . . . . . 7 |- (x = 0h -> x = 0h)
9	7, 8	eqeq12d 1486	. . . . . 6 |- (x = 0h -> ((T` x) = x <-> (T` 0h) = 0h))
10	9	elrab 1901	. . . . 5 |- (0h e. {x e. H~ | (T` x) = x} <-> (0h e. H~ /\ (T` 0h) = 0h))
11		ax-hv0cl 8812	. . . . 5 |- 0h e. H~
12		hmopidmch.2	. . . . . . . 8 |- (T e. HrmOp /\ (T o. T) = T)
13	12	pm3.26i 320	. . . . . . 7 |- T e. HrmOp
14		hmoplint 9805	. . . . . . 7 |- (T e. HrmOp -> T e. LinOp)
15	13, 14	ax-mp 7	. . . . . 6 |- T e. LinOp
16	15	lnop0 9833	. . . . 5 |- (T` 0h) = 0h
17	10, 11, 16	mpbir2an 729	. . . 4 |- 0h e. {x e. H~ | (T` x) = x}
18	17, 2	eleqtrr 1544	. . 3 |- 0h e. H
19		hvaddclt 8821	. . . . . . . . . 10 |- ((y e. H~ /\ z e. H~) -> (y +h z) e. H~)
20	19	ad2ant2r 409	. . . . . . . . 9 |- (((y e. H~ /\ (T` y) = y) /\ (z e. H~ /\ (T` z) = z)) -> (y +h z) e. H~)
21	15	lnopadd 9834	. . . . . . . . . . 11 |- ((y e. H~ /\ z e. H~) -> (T` (y +h z)) = ((T` y) +h (T` z)))
22		opreq12 3961	. . . . . . . . . . 11 |- (((T` y) = y /\ (T` z) = z) -> ((T` y) +h (T` z)) = (y +h z))
23	21, 22	sylan9eq 1524	. . . . . . . . . 10 |- (((y e. H~ /\ z e. H~) /\ ((T` y) = y /\ (T` z) = z)) -> (T` (y +h z)) = (y +h z))
24	23	an4s 508	. . . . . . . . 9 |- (((y e. H~ /\ (T` y) = y) /\ (z e. H~ /\ (T` z) = z)) -> (T` (y +h z)) = (y +h z))
25	20, 24	jca 288	. . . . . . . 8 |- (((y e. H~ /\ (T` y) = y) /\ (z e. H~ /\ (T` z) = z)) -> ((y +h z) e. H~ /\ (T` (y +h z)) = (y +h z)))
26		fveq2 3715	. . . . . . . . . 10 |- (x = y -> (T` x) = (T` y))
27		id 59	. . . . . . . . . 10 |- (x = y -> x = y)
28	26, 27	eqeq12d 1486	. . . . . . . . 9 |- (x = y -> ((T` x) = x <-> (T` y) = y))
29	28, 2	elrab2 1903	. . . . . . . 8 |- (y e. H <-> (y e. H~ /\ (T` y) = y))
30		fveq2 3715	. . . . . . . . . 10 |- (x = z -> (T` x) = (T` z))
31		id 59	. . . . . . . . . 10 |- (x = z -> x = z)
32	30, 31	eqeq12d 1486	. . . . . . . . 9 |- (x = z -> ((T` x) = x <-> (T` z) = z))
33	32, 2	elrab2 1903	. . . . . . . 8 |- (z e. H <-> (z e. H~ /\ (T` z) = z))
34	25, 29, 33	syl2anb 455	. . . . . . 7 |- ((y e. H /\ z e. H) -> ((y +h z) e. H~ /\ (T` (y +h z)) = (y +h z)))
35		fveq2 3715	. . . . . . . . 9 |- (x = (y +h z) -> (T` x) = (T` (y +h z)))
36		id 59	. . . . . . . . 9 |- (x = (y +h z) -> x = (y +h z))
37	35, 36	eqeq12d 1486	. . . . . . . 8 |- (x = (y +h z) -> ((T` x) = x <-> (T` (y +h z)) = (y +h z)))
38	37	elrab 1901	. . . . . . 7 |- ((y +h z) e. {x e. H~ | (T` x) = x} <-> ((y +h z) e. H~ /\ (T` (y +h z)) = (y +h z)))
39	34, 38	sylibr 200	. . . . . 6 |- ((y e. H /\ z e. H) -> (y +h z) e. {x e. H~ | (T` x) = x})
40	39, 2	syl6eleqr 1556	. . . . 5 |- ((y e. H /\ z e. H) -> (y +h z) e. H)
41	40	rgen2a 1696	. . . 4 |- A.y e. H A.z e. H (y +h z) e. H
42		hvmulclt 8822	. . . . . . . . . . 11 |- ((y e. CC /\ z e. H~) -> (y .h z) e. H~)
43	42	adantr 389	. . . . . . . . . 10 |- (((y e. CC /\ z e. H~) /\ (T` z) = z) -> (y .h z) e. H~)
44	15	lnopmul 9835	. . . . . . . . . . 11 |- ((y e. CC /\ z e. H~) -> (T` (y .h z)) = (y .h (T` z)))
45		opreq2 3960	. . . . . . . . . . 11 |- ((T` z) = z -> (y .h (T` z)) = (y .h z))
46	44, 45	sylan9eq 1524	. . . . . . . . . 10 |- (((y e. CC /\ z e. H~) /\ (T` z) = z) -> (T` (y .h z)) = (y .h z))
47	43, 46	jca 288	. . . . . . . . 9 |- (((y e. CC /\ z e. H~) /\ (T` z) = z) -> ((y .h z) e. H~ /\ (T` (y .h z)) = (y .h z)))
48	47	anasss 440	. . . . . . . 8 |- ((y e. CC /\ (z e. H~ /\ (T` z) = z)) -> ((y .h z) e. H~ /\ (T` (y .h z)) = (y .h z)))
49	48, 33	sylan2b 452	. . . . . . 7 |- ((y e. CC /\ z e. H) -> ((y .h z) e. H~ /\ (T` (y .h z)) = (y .h z)))
50		fveq2 3715	. . . . . . . . 9 |- (x = (y .h z) -> (T` x) = (T` (y .h z)))
51		id 59	. . . . . . . . 9 |- (x = (y .h z) -> x = (y .h z))
52	50, 51	eqeq12d 1486	. . . . . . . 8 |- (x = (y .h z) -> ((T` x) = x <-> (T` (y .h z)) = (y .h z)))
53	52	elrab 1901	. . . . . . 7 |- ((y .h z) e. {x e. H~ | (T` x) = x} <-> ((y .h z) e. H~ /\ (T` (y .h z)) = (y .h z)))
54	49, 53	sylibr 200	. . . . . 6 |- ((y e. CC /\ z e. H) -> (y .h z) e. {x e. H~ | (T` x) = x})
55	54, 2	syl6eleqr 1556	. . . . 5 |- ((y e. CC /\ z e. H) -> (y .h z) e. H)
56	55	rgen2 1720	. . . 4 |- A.y e. CC A.z e. H (y .h z) e. H
57	41, 56	pm3.2i 285	. . 3 |- (A.y e. H A.z e. H (y +h z) e. H /\ A.y e. CC A.z e. H (y .h z) e. H)
58	6, 18, 57	mpbir2an 729	. 2 |- H e. SH
59		visset 1809	. . . . . . 7 |- f e. V
60		visset 1809	. . . . . . 7 |- y e. V
61	59, 60	hlimvec 8997	. . . . . 6 |- (f ~~>v y -> y e. H~)
62	61	adantl 388	. . . . 5 |- ((f:NN-->H /\ f ~~>v y) -> y e. H~)
63		squeeze0 5880	. . . . . . . . 9 |- ((((normh` ((T` y) -h y)) / 2) e. RR /\ 0 <_ ((normh` ((T` y) -h y)) / 2) /\ A.z e. RR (0 < z -> ((normh` ((T` y) -h y)) / 2) < z)) -> ((normh` ((T` y) -h y)) / 2) = 0)
64		hvsubclt 8826	. . . . . . . . . . . . 13 |- (((T` y) e. H~ /\ y e. H~) -> ((T` y) -h y) e. H~)
65	15	lnopf 9832	. . . . . . . . . . . . . . 15 |- T:H~-->H~
66	65	ffvelrni 3806	. . . . . . . . . . . . . 14 |- (y e. H~ -> (T` y) e. H~)
67	61, 66	syl 10	. . . . . . . . . . . . 13 |- (f ~~>v y -> (T` y) e. H~)
68	64, 67, 61	sylanc 471	. . . . . . . . . . . 12 |- (f ~~>v y -> ((T` y) -h y) e. H~)
69		normclt 8930	. . . . . . . . . . . 12 |- (((T` y) -h y) e. H~ -> (normh` ((T` y) -h y)) e. RR)
70	68, 69	syl 10	. . . . . . . . . . 11 |- (f ~~>v y -> (normh` ((T` y) -h y)) e. RR)
71		rehalfclt 5989	. . . . . . . . . . 11 |- ((normh` ((T` y) -h y)) e. RR -> ((normh` ((T` y) -h y)) / 2) e. RR)
72	70, 71	syl 10	. . . . . . . . . 10 |- (f ~~>v y -> ((normh` ((T` y) -h y)) / 2) e. RR)
73	72	adantl 388	. . . . . . . . 9 |- ((f:NN-->H /\ f ~~>v y) -> ((normh` ((T` y) -h y)) / 2) e. RR)
74		normge0t 8931	. . . . . . . . . . . 12 |- (((T` y) -h y) e. H~ -> 0 <_ (normh` ((T` y) -h y)))
75	68, 74	syl 10	. . . . . . . . . . 11 |- (f ~~>v y -> 0 <_ (normh` ((T` y) -h y)