Theorem hmopidmchi 12712

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
hmopidmchi	|- H e. CH

Distinct variable group:   x,T

Proof of Theorem hmopidmchi

Step	Hyp	Ref	Expression
1		closedsub 11718	. 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 2949	. . . . 5 |- {x e. ~H | (T` x) = x} C_ ~H
4	2, 3	eqsstri 2906	. . . 4 |- H C_ ~H
5		sh2 11716	. . . 4 |- (H C_ ~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 4804	. . . . . . 7 |- (x = 0h -> (T` x) = (T` 0h))
8		id 15	. . . . . . 7 |- (x = 0h -> x = 0h)
9	7, 8	eqeq12d 2184	. . . . . 6 |- (x = 0h -> ((T` x) = x <-> (T` 0h) = 0h))
10	9	elrab 2685	. . . . 5 |- (0h e. {x e. ~H | (T` x) = x} <-> (0h e. ~H /\ (T` 0h) = 0h))
11		ax-hv0cl 11501	. . . . 5 |- 0h e. ~H
12		hmopidmch.2	. . . . . . . 8 |- (T e. HrmOp /\ (T o. T) = T)
13	12	simpli 535	. . . . . . 7 |- T e. HrmOp
14		hmoplin 12493	. . . . . . 7 |- (T e. HrmOp -> T e. LinOp)
15	13, 14	ax-mp 7	. . . . . 6 |- T e. LinOp
16	15	lnop0i 12521	. . . . 5 |- (T` 0h) = 0h
17	10, 11, 16	mpbir2an 1062	. . . 4 |- 0h e. {x e. ~H | (T` x) = x}
18	17, 2	eleqtrri 2246	. . 3 |- 0h e. H
19		fveq2 4804	. . . . . . . . . 10 |- (x = y -> (T` x) = (T` y))
20		id 15	. . . . . . . . . 10 |- (x = y -> x = y)
21	19, 20	eqeq12d 2184	. . . . . . . . 9 |- (x = y -> ((T` x) = x <-> (T` y) = y))
22	21, 2	elrab2 2687	. . . . . . . 8 |- (y e. H <-> (y e. ~H /\ (T` y) = y))
23		fveq2 4804	. . . . . . . . . 10 |- (x = z -> (T` x) = (T` z))
24		id 15	. . . . . . . . . 10 |- (x = z -> x = z)
25	23, 24	eqeq12d 2184	. . . . . . . . 9 |- (x = z -> ((T` x) = x <-> (T` z) = z))
26	25, 2	elrab2 2687	. . . . . . . 8 |- (z e. H <-> (z e. ~H /\ (T` z) = z))
27		hvaddcl 11510	. . . . . . . . . 10 |- ((y e. ~H /\ z e. ~H) -> (y +h z) e. ~H)
28	27	ad2ant2r 864	. . . . . . . . 9 |- (((y e. ~H /\ (T` y) = y) /\ (z e. ~H /\ (T` z) = z)) -> (y +h z) e. ~H)
29	15	lnopaddi 12522	. . . . . . . . . . 11 |- ((y e. ~H /\ z e. ~H) -> (T` (y +h z)) = ((T` y) +h (T` z)))
30		opreq12 5027	. . . . . . . . . . 11 |- (((T` y) = y /\ (T` z) = z) -> ((T` y) +h (T` z)) = (y +h z))
31	29, 30	sylan9eq 2226	. . . . . . . . . 10 |- (((y e. ~H /\ z e. ~H) /\ ((T` y) = y /\ (T` z) = z)) -> (T` (y +h z)) = (y +h z))
32	31	an4s 941	. . . . . . . . 9 |- (((y e. ~H /\ (T` y) = y) /\ (z e. ~H /\ (T` z) = z)) -> (T` (y +h z)) = (y +h z))
33	28, 32	jca 590	. . . . . . . 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)))
34	22, 26, 33	syl2anb 700	. . . . . . 7 |- ((y e. H /\ z e. H) -> ((y +h z) e. ~H /\ (T` (y +h z)) = (y +h z)))
35		fveq2 4804	. . . . . . . . 9 |- (x = (y +h z) -> (T` x) = (T` (y +h z)))
36		id 15	. . . . . . . . 9 |- (x = (y +h z) -> x = (y +h z))
37	35, 36	eqeq12d 2184	. . . . . . . 8 |- (x = (y +h z) -> ((T` x) = x <-> (T` (y +h z)) = (y +h z)))
38	37	elrab 2685	. . . . . . 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 264	. . . . . 6 |- ((y e. H /\ z e. H) -> (y +h z) e. {x e. ~H | (T` x) = x})
40	39, 2	syl6eleqr 2262	. . . . 5 |- ((y e. H /\ z e. H) -> (y +h z) e. H)
41	40	rgen2a 2441	. . . 4 |- A.y e. H A.z e. H (y +h z) e. H
42		hvmulcl 11511	. . . . . . . . . . 11 |- ((y e. CC /\ z e. ~H) -> (y .h z) e. ~H)
43	42	adantr 543	. . . . . . . . . 10 |- (((y e. CC /\ z e. ~H) /\ (T` z) = z) -> (y .h z) e. ~H)
44	15	lnopmuli 12523	. . . . . . . . . . 11 |- ((y e. CC /\ z e. ~H) -> (T` (y .h z)) = (y .h (T` z)))
45		opreq2 5026	. . . . . . . . . . 11 |- ((T` z) = z -> (y .h (T` z)) = (y .h z))
46	44, 45	sylan9eq 2226	. . . . . . . . . 10 |- (((y e. CC /\ z e. ~H) /\ (T` z) = z) -> (T` (y .h z)) = (y .h z))
47	43, 46	jca 590	. . . . . . . . 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 727	. . . . . . . 8 |- ((y e. CC /\ (z e. ~H /\ (T` z) = z)) -> ((y .h z) e. ~H /\ (T` (y .h z)) = (y .h z)))
49	26, 48	sylan2b 697	. . . . . . 7 |- ((y e. CC /\ z e. H) -> ((y .h z) e. ~H /\ (T` (y .h z)) = (y .h z)))
50		fveq2 4804	. . . . . . . . 9 |- (x = (y .h z) -> (T` x) = (T` (y .h z)))
51		id 15	. . . . . . . . 9 |- (x = (y .h z) -> x = (y .h z))
52	50, 51	eqeq12d 2184	. . . . . . . 8 |- (x = (y .h z) -> ((T` x) = x <-> (T` (y .h z)) = (y .h z)))
53	52	elrab 2685	. . . . . . 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 264	. . . . . 6 |- ((y e. CC /\ z e. H) -> (y .h z) e. {x e. ~H | (T` x) = x})
55	54, 2	syl6eleqr 2262	. . . . 5 |- ((y e. CC /\ z e. H) -> (y .h z) e. H)
56	55	rgen2 2467	. . . 4 |- A.y e. CC A.z e. H (y .h z) e. H
57	41, 56	pm3.2i 514	. . 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 1062	. 2 |- H e. SH
59		visset 2572	. . . . . 6 |- f e. _V
60		visset 2572	. . . . . 6 |- y e. _V
61	59, 60	hlimveci 11685	. . . . 5 |- (f ~~>v y -> y e. ~H)
62	61	adantl 544	. . . 4 |- ((f:NN-->H /\ f ~~>v y) -> y e. ~H)
63	15	lnopfi 12520	. . . . . . . . . . . . . 14 |- T:~H-->~H
64	63	ffvelrni 4917	. . . . . . . . . . . . 13 |- (y e. ~H -> (T` y) e. ~H)
65	61, 64	syl 13	. . . . . . . . . . . 12 |- (f ~~>v y -> (T` y) e. ~H)
66		hvsubcl 11515	. . . . . . . . . . . 12 |- (((T` y) e. ~H /\ y e. ~H) -> ((T` y) -h y) e. ~H)
67	65, 61, 66	syl11anc 755	. . . . . . . . . . 11 |- (f ~~>v y -> ((T` y) -h y) e. ~H)
68		normcl 11619	. . . . . . . . . . 11 |- (((T` y) -h y) e. ~H -> (normh` ((T` y) -h y)) e. RR)
69	67, 68	syl 13	. . . . . . . . . 10 |- (f ~~>v y -> (normh` ((T` y) -h y)) e. RR)
70		rehalfcl 7666	. . . . . . . . . 10 |- ((normh` ((T` y) -h y)) e. RR -> ((normh` ((T` y) -h y)) / 2) e. RR)
71	69, 70	syl 13	. . . . . . . . 9 |- (f ~~>v y -> ((normh` ((T` y) -h y)) / 2) e. RR)
72	71	adantl 544	. . . . . . . 8 |- ((f:NN-->H /\ f ~~>v y) -> ((normh` ((T` y) -h y)) / 2) e. RR)
73		normge0 11620	. . . . . . . . . . 11 |- (((T` y) -h y) e. ~H -> 0 <_ (normh` ((T` y) -h y)))
74	67, 73	syl 13	. . . . . . . . . 10 |- (f ~~>v y -> 0 <_ (normh` ((T` y) -h y)))
75		halfnneg2 7670	. . . . . . . . . . 11 |- ((normh` ((T` y) -h y)) e. RR -> (0 <_ (normh` ((T` y) -h y)) <-> 0 <_ ((normh` ((T` y) -h y)) / 2)))
76	69, 75	syl 13	. . . . . . . . . 10 |- (f ~~>v y -> (0 <_ (normh` ((T` y) -h y)) <-> 0 <_ ((normh` ((T` y) -h y)) / 2)))
77	74, 76	mpbid 256	. . . . . . . . 9 |- (f ~~>v y -> 0 <_ ((normh` ((T` y) -h y)) / 2))
78	77	adantl 544	. . . . . . . 8 |- ((f:NN-->H /\ f ~~>v y) -> 0 <_ ((normh` ((T` y) -h y)) / 2))
79	59, 60	hlimconvi 11686	. . . . . . . . . 10 |- (f ~~>v y -> A.z e. RR (0 < z -> E.m e. NN A.n e. NN (m <_ n -> (normh` ((f` n) -h y)) < z)))
80	79	adantl 544	. . . . . . . . 9 |- ((f:NN-->H /\ f ~~>v y) -> A.z e. RR (0 < z -> E.m e. NN A.n e. NN (m <_ n -> (normh` ((f` n) -h y)) < z)))
81		nnre 7547	. . . . . . . . . . . . . . . 16 |- (m e. NN -> m e. RR)
82		leid 6992	. . . . . . . . . . . . . . . 16 |- (m e. RR -> m <_ m)
83	81, 82	syl 13	. . . . . . . . . . . . . . 15 |- (m e. NN -> m <_ m)
84		breq2 3543	. . . . . . . . . . . . . . . . 17 |- (n = m -> (m <_ n <-> m <_ m))
85		fveq2 4804	. . . . . . . . . . . . . . . . . . . 20 |- (n = m -> (f` n) = (f` m))
86	85	opreq1d 5032	. . . . . . . . . . . . . . . . . . 19 |- (n = m -> ((f` n) -h y) = ((f` m) -h y))
87	86	fveq2d 4808	. . . . . . . . . . . . . . . . . 18 |- (n = m -> (normh` ((f` n) -h y)) = (normh` ((f` m) -h y)))
88	87	breq1d 3549	. . . . . . . . . . . . . . . . 17 |- (n = m -> ((normh` ((f` n) -h y)) < z <-> (normh` ((f` m) -h y)) < z))
89	84, 88	imbi12d 384	. . . . . . . . . . . . . . . 16 |- (n = m -> ((m <_ n -> (normh` ((f` n) -h y)) < z) <-> (m <_ m -> (normh` ((f` m) -h y)) < z)))
90	89	rcla4v 2647	. . . . . . . . . . . . . . 15 |- (m e. NN -> (A.n e. NN (m <_ n -> (normh` ((f` n) -h y)) < z) -> (m <_ m -> (normh` ((f` m) -h y)) < z)))
91	83, 90	mpid 21	. . . . . . . . . . . . . 14 |- (m e. NN -> (A.n e. NN (m <_ n -> (normh` ((f` n) -h y)) < z) -> (normh` ((f` m) -h y)) < z))
92	91	adantl 544	. . . . . . . . . . . . 13 |- ((((f:NN-->H /\ f ~~>v y) /\ z e. RR) /\ m e. NN) -> (A.n e. NN (m <_ n -> (normh` ((f` n) -h y)) < z) -> (normh` ((f` m) -h y)) < z))
93		ffvelrn 4916	. . . . . . . . . . . . . . . . 17 |- ((f:NN-->H /\ m e. NN) -> (f` m) e. H)
94	93, 61	anim12i 632	. . . . . . . . . . . . . . . 16 |- (((f:NN-->H /\ m e. NN) /\ f ~~>v y) -> ((f` m) e. H /\ y e. ~H))
95	94	an32s 912	. . . . . . . . . . . . . . 15 |- (((f:NN-->H /\ f ~~>v y) /\ m e. NN) -> ((f` m) e. H /\ y e. ~H))
96	64, 66	mpancom 771	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. ~H -> ((T` y) -h y) e. ~H)
97	96, 68	syl 13	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. ~H -> (normh` ((T` y) -h y)) e. RR)
98	97	adantl 544	. . . . . . . . . . . . . . . . . . . 20 |- (((f` m) e. H /\ y e. ~H) -> (normh` ((T` y) -h y)) e. RR)
99	4	sseli 2880	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((f` m) e. H -> (f` m) e. ~H)
100		hvsubcl 11515	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((T` y) e. ~H /\ (f` m) e. ~H) -> ((T` y) -h (f` m)) e. ~H)
101	64, 99, 100	syl2an 699	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. ~H /\ (f` m) e. H) -> ((T` y) -h (f` m)) e. ~H)
102	101	ancoms 512	. . . . . . . . . . . . . . . . . . . . . 22 |- (((f` m) e. H /\ y e. ~H) -> ((T` y) -h (f` m)) e. ~H)
103		normcl 11619	. . . . . . . . . . . . . . . . . . . . . 22 |- (((T` y) -h (f` m)) e. ~H -> (normh` ((T` y) -h (f` m))) e. RR)
104	102, 103	syl 13	. . . . . . . . . . . . . . . . . . . . 21 |- (((f` m) e. H /\ y e. ~H) -> (normh` ((T` y) -h (f` m))) e. RR)
105		hvsubcl 11515	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((f` m) e. ~H /\ y e. ~H) -> ((f` m) -h y) e. ~H)
106	99, 105	sylan 693	. . . . . . . . . . . . . . . . . . . . . 22 |- (((f` m) e. H /\ y e. ~H) -> ((f` m) -h y) e. ~H)
107		normcl 11619	. . . . . . . . . . . . . . . . . . . . . 22 |- (((f` m) -h y) e. ~H -> (normh` ((f` m) -h y)) e. RR)
108	106, 107	syl 13	. . . . . . . . . . . . . . . . . . . . 21 |- (((f` m) e. H /\ y e. ~H) -> (normh` ((f` m) -h y)) e. RR)
109		readdcl 6911	. . . . . . . . . . . . . . . . . . . . 21 |- (((normh` ((T` y) -h (f` m))) e. RR /\ (normh` ((f` m) -h y)) e. RR) -> ((normh` ((T` y) -h (f` m))) + (normh` ((f` m) -h y))) e. RR)
110	104, 108, 109	syl11anc 755	. . . . . . . . . . . . . . . . . . . 20 |- (((f` m) e. H /\ y e. ~H) -> ((normh` ((T` y) -h (f` m))) + (normh` ((f` m) -h y))) e. RR)
111		readdcl 6911	. . . . . . . . . . . . . . . . . . . . 21 |- (((normh` ((f` m) -h y)) e. RR /\ (normh` ((f` m) -h y)) e. RR) -> ((normh` ((f` m) -h y)) + (normh` ((f` m) -h y))) e. RR)
112	108, 108, 111	syl11anc 755	. . . . . . . . . . . . . . . . . . . 20 |- (((f` m) e. H /\ y e. ~H) -> ((normh` ((f` m) -h y)) + (normh` ((f` m) -h y))) e. RR)
113	64	adantl 544	. . . . . . . . . . . . . . . . . . . . 21 |- (((f` m) e. H /\ y e. ~H) -> (T` y) e. ~H)
114		simpr 538	. . . . . . . . . . . . . . . . . . . . 21 |- (((f` m) e. H /\ y e. ~H) -> y e. ~H)
115	99	adantr 543	. . . . . . . . . . . . . . . . . . . . 21 |- (((f` m) e. H /\ y e. ~H) -> (f` m) e. ~H)
116		norm3dif 11644	. . . . . . . . . . . . . . . . . . . . 21 |- (((T` y) e. ~H /\ y e. ~H /\ (f` m) e. ~H) -> (normh` ((T` y) -h y)) <_ ((normh` ((T` y) -h (f` m))) + (normh` ((f` m) -h y))))
117	113, 114, 115, 116	syl111anc 1377	. . . . . . . . . . . . . . . . . . . 20 |- (((f` m) e. H /\ y e. ~H) -> (normh` ((T` y) -h y)) <_ ((normh` ((T` y) -h (f` m))) + (normh` ((f` m) -h y))))
118		hvsubcl 11515	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. ~H /\ (f` m) e. ~H) -> (y -h (f` m)) e. ~H)
119	118	ancoms 512	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((f` m) e. ~H /\ y e. ~H) -> (y -h (f` m)) e. ~H)
120	99, 119	sylan 693	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((f` m) e. H /\ y e. ~H) -> (y -h (f` m)) e. ~H)
121	2, 12	hmopidmchlem 12711	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y -h (f` m)) e. ~H -> (normh` (T` (y -h (f` m)))) <_ (normh` (y -h (f` m))))
122	120, 121	syl 13	. . . . . . . . . . . . . . . . . . . . . 22 |- (((f` m) e. H /\ y e. ~H) -> (normh` (T` (y -h (f` m)))) <_ (normh` (y -h (f` m))))
123	15	lnopsubi 12525	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((y e. ~H /\ (f` m) e. ~H) -> (T` (y -h (f` m))) = ((T` y) -h (T` (f` m))))
124	123	ancoms 512	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((f` m) e. ~H /\ y e. ~H) -> (T` (y -h (f` m))) = ((T` y) -h (T` (f` m))))
125	99, 124	sylan 693	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((f` m) e. H /\ y e. ~H) -> (T` (y -h (f` m))) = ((T` y) -h (T` (f` m))))
126		fveq2 4804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x = (f` m) -> (T` x) = (T` (f` m)))
127		id 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x = (f` m) -> x = (f` m))
128	126, 127	eqeq12d 2184	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x = (f` m) -> ((T` x) = x <-> (T` (f` m)) = (f` m)))
129	128, 2	elrab2 2687	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((f` m) e. H <-> ((f` m) e. ~H /\ (T` (f` m)) = (f` m)))
130	129	simprbi 542	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f` m) e. H -> (T` (f` m)) = (f` m))
131	130	adantr 543	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((f` m) e. H /\ y e. ~H) -> (T` (f` m)) = (f` m))
132	131	opreq2d 5033	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((f` m) e. H /\ y e. ~H) -> ((T` y) -h (T` (f` m))) = ((T` y) -h (f` m)))
133	125, 132	eqtr2d 2203	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((f` m) e. H /\ y e. ~H) -> ((T` y) -h (f` m)) = (T` (y -h (f` m))))
134	133	fveq2d 4808	. . . . . . . . . . . . . . . . . . . . . 22 |- (((f` m) e. H /\ y e. ~H) -> (normh` ((T` y) -h (f` m))) = (normh` (T` (y -h (f` m)))))
135		normsub 11637	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((f` m) e. ~H /\ y e. ~H) -> (normh` ((f` m) -h y)) = (normh` (y -h (f` m))))
136	99, 135	sylan 693	. . . . . . . . . . . . . . . . . . . . . 22 |- (((f` m) e. H /\ y e. ~H) -> (normh` ((f` m) -h y)) = (normh` (y -h (f` m))))
137	122, 134, 136	3brtr4d 3569	. . . . . . . . . . . . . . . . . . . . 21 |- (((f` m) e. H /\ y e. ~H) -> (normh` ((T` y) -h (f` m))) <_ (normh` ((f` m) -h y)))
138		leadd1 7249	. . . . . . . . . . . . . . . . . . . . . 22 |- (((normh` ((T` y) -h (f` m))) e. RR /\ (normh` ((f` m) -h y)) e. RR /\ (normh` ((f` m) -h y)) e. RR) -> ((normh` ((T` y) -h (f` m))) <_ (normh` ((f` m) -h y)) <-> ((normh` ((T` y) -h (f` m))) + (normh` ((f` m) -h y))) <_ ((normh` ((f` m) -h y)) + (normh` ((f` m) -h y)))))
139	104, 108, 108, 138	syl111anc 1377	. . . . . . . . . . . . . . . . . . . . 21 |- (((f` m) e. H /\ y e. ~H) -> ((normh` ((T` y) -h (f` m))) <_ (normh` ((f` m) -h y)) <-> ((normh` ((T` y) -h (f` m))) + (normh` ((f` m) -h y))) <_ ((normh` ((f` m) -h y)) + (normh` ((f` m) -h y)))))
140	137, 139	mpbid 256	. . . . . . . . . . . . . . . . . . . 20 |- (((f` m) e. H /\ y e. ~H) -> ((normh` ((T` y) -h (f` m))) + (normh` ((f` m) -h y))) <_ ((normh` ((f` m) -h y)) + (normh` ((f` m) -h y))))
141	98, 110, 112, 117, 140	letrd 6987	. . . . . . . . . . . . . . . . . . 19 |- (((f` m) e. H /\ y e. ~H) -> (normh` ((T` y) -h y)) <_ ((normh` ((f` m) -h y)) + (normh` ((f` m) -h y))))
142	108	recnd 6921	. . . . . . . . . . . . . . . . . . . 20 |- (((f` m) e. H /\ y e. ~H) -> (normh` ((f` m) -h y)) e. CC)
143		2times 7625	. . . . . . . . . . . . . . . . . . . 20 |- ((normh` ((f` m) -h y)) e. CC -> (2 x. (normh` ((f` m) -h y))) = ((normh` ((f` m) -h y)) + (normh` ((f` m) -h y))))
144	142, 143	syl 13	. . . . . . . . . . . . . . . . . . 19 |- (((f` m) e. H /\ y e. ~H) -> (2 x. (normh` ((f` m) -h y))) = ((normh` ((f` m) -h y)) + (normh` ((f` m) -h y))))
145	141, 144	breqtrrd 3565	. . . . . . . . . . . . . . . . . 18 |- (((f` m) e. H /\ y e. ~H) -> (normh` ((T` y) -h y)) <_ (2 x. (normh` ((f` m) -h y))))
146		2re 7598	. . . . . . . . . . . . . . . . . . . 20 |- 2 e. RR
147		2pos 7609	. . . . . . . . . . . . . . . . . . . . 21 |- 0 < 2
148		ledivmulOLD 7487	. . . . . . . . . . . . . . . . . . . . 21 |- ((((normh` ((T` y) -h y)) e. RR /\ 2 e. RR /\ (normh` ((f` m) -h y)) e. RR) /\ 0 < 2) -> (((normh` ((T` y) -h y)) / 2) <_ (normh` ((f` m) -h y)) <-> (normh` ((T` y) -h y)) <_ (2 x. (normh` ((f` m) -h y)))))
149	147, 148	mpan2 775	. . . . . . . . . . . . . . . . . . . 20 |- (((normh` ((T` y) -h y)) e. RR /\ 2 e. RR /\ (normh` ((f` m) -h y)) e. RR) -> (((normh` ((T` y) -h y)) / 2) <_ (normh` ((f` m) -h y)) <-> (normh` ((T` y) -h y)) <_ (2 x. (normh` ((f` m) -h y)))))
150	146, 149	mp3an2 1482	. . . . . . . . . . . . . . . . . . 19 |- (((normh` ((T` y) -h y)) e. RR /\ (normh` ((f` m) -h y)) e. RR) -> (((normh` ((T` y) -h y)) / 2) <_ (normh` ((f` m) -h y)) <-> (normh` ((T` y) -h y)) <_ (2 x. (normh` ((f` m) -h y)))))
151	98, 108, 150	syl11anc 755	. . . . . . . . . . . . . . . . . 18 |- (((f` m) e. H /\ y e. ~H) -> (((normh` ((T` y) -h y)) / 2) <_ (normh` ((f` m) -h y)) <-> (normh` ((T` y) -h y)) <_ (2 x. (normh` ((f` m) -h y)))))
152	145, 151	mpbird 257	. . . . . . . . . . . . . . . . 17 |- (((f` m) e. H /\ y e. ~H) -> ((normh` ((T` y) -h y)) / 2) <_ (normh` ((f` m) -h y)))
153	152	adantr 543	. . . . . . . . . . . . . . . 16 |- ((((f` m) e. H /\ y e. ~H) /\ z e. RR) -> ((normh` ((T` y) -h y)) / 2) <_ (normh` ((f` m) -h y)))
154	97, 70	syl 13	. . . . . . . . . . . . . . . . . 18 |- (y e. ~H -> ((normh` ((T` y) -h y)) / 2) e. RR)
155	154	ad2antlr 859	. . . . . . . . . . . . . . . . 17 |- ((((f` m) e. H /\ y e. ~H) /\ z e. RR) -> ((normh` ((T` y) -h y)) / 2) e. RR)
156	108	adantr 543	. . . . . . . . . . . . . . . . 17 |- ((((f` m) e. H /\ y e. ~H) /\ z e. RR) -> (normh` ((f` m) -h y)) e. RR)
157		simpr 538	. . . . . . . . . . . . . . . . 17 |- ((((f` m) e. H /\ y e. ~H) /\ z e. RR) -> z e. RR)
158		lelttr 6984	. . . . . . . . . . . . . . . . 17 |- ((((normh` ((T` y) -h y)) / 2) e. RR /\ (normh` ((f` m) -h y)) e. RR /\ z e. RR) -> ((((normh` ((T` y) -h y)) / 2) <_ (normh` ((f` m) -h y)) /\ (normh` ((f` m) -h y)) < z) -> ((normh` ((T` y) -h y)) / 2) < z))
159	155, 156, 157, 158	syl111anc 1377	. . . . . . . . . . . . . . . 16 |- ((((f` m) e. H /\ y e. ~H) /\ z e. RR) -> ((((normh` ((T` y) -h y)) / 2) <_ (normh` ((f` m) -h y)) /\ (normh` ((f` m) -h y)) < z) -> ((normh` ((T` y) -h y)) / 2) < z))
160	153, 159	mpand 780	. . . . . . . . . . . . . . 15 |- ((((f` m) e. H /\ y e. ~H) /\ z e. RR) -> ((normh` ((f` m) -h y)) < z -> ((normh` ((T` y) -h y)) / 2) < z))
161	95, 160	sylan 693	. . . . . . . . . . . . . 14 |- ((((f:NN-->H /\ f ~~>v y) /\ m e. NN) /\ z e. RR) -> ((normh` ((f` m) -h y)) < z -> ((normh` ((T` y) -h y)) / 2) < z))
162	161	an32s 912	. . . . . . . . . . . . 13 |- ((((f:NN-->H /\ f ~~>v y) /\ z e. RR) /\ m e. NN) -> ((normh` ((f` m) -h y)) < z -> ((normh` ((T` y) -h y)) / 2) < z))
163	92, 162	syld 31	. . . . . . . . . . . 12 |- ((((f:NN-->H /\ f ~~>v y) /\ z e. RR) /\ m e. NN) -> (A.n e. NN (m <_ n -> (normh` ((f` n) -h y)) < z) -> ((normh` ((T` y) -h y)) / 2) < z))
164	163	r19.23adva 2494	. . . . . . . . . . 11 |- (((f:NN-->H /\ f ~~>v y) /\ z e. RR) -> (E.m e. NN A.n e. NN (m <_ n -> (normh` ((f` n) -h y)) < z) -> ((normh` ((T` y) -h y)) / 2) < z))
165	164	imim2d 28	. . . . . . . . . 10 |- (((f:NN-->H /\ f ~~>v y) /\ z e. RR) -> ((0 < z -> E.m e. NN A.n e. NN (m <_ n -> (normh` ((f` n) -h y)) < z)) -> (0 < z -> ((normh` ((T` y) -h y)) / 2) < z)))
166	165	ralimdva 2451	. . . . . . . . 9 |- ((f:NN-->H /\ f ~~>v y) -> (A.z e. RR (0 < z -> E.m e. NN A.n e. NN (m <_ n -> (normh` ((f` n) -h y)) < z)) -> A.z e. RR (0 < z -> ((normh` ((T` y) -h y)) / 2) < z)))
167	80, 166	mpd 11	. . . . . . . 8 |- ((f:NN-->H /\ f ~~>v y) -> A.z e. RR (0 < z -> ((normh` ((T` y) -h y)) / 2) < z))
168		squeeze0 7542	. . . . . . . 8 |- ((((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)
169	72, 78, 167, 168	syl111anc 1377	. . . . . . 7 |- ((f:NN-->H /\ f ~~>v y) -> ((normh` ((T` y) -h y)) / 2) = 0)
170	69	recnd 6921	. . . . . . . . 9 |- (f ~~>v y -> (normh` ((T` y) -h y)) e. CC)
171		half0 7667	. . . . . . . . 9 |- ((normh` ((T` y) -h y)) e. CC -> (((normh` ((T` y) -h y)) / 2) = 0 <-> (normh` ((T` y) -h y)) = 0))
172	170, 171	syl 13	. . . . . . . 8 |- (f ~~>v y -> (((normh` ((T` y) -h y)) / 2) = 0 <-> (normh` ((T` y) -h y)) = 0))
173	172	adantl 544	. . . . . . 7 |- ((f:NN-->H /\ f ~~>v y) -> (((normh` ((T` y) -h y)) / 2) = 0 <-> (normh` ((T` y) -h y)) = 0))
174	169, 173	mpbid 256	. . . . . 6 |- ((f:NN-->H /\ f ~~>v y) -> (normh` ((T` y) -h y)) = 0)
175		norm-i 11623	. . . . . . . 8 |- (((T` y) -h y) e. ~H -> ((normh` ((T` y) -h y)) = 0 <-> ((T` y) -h y) = 0h))
176	67, 175	syl 13	. . . . . . 7 |- (f ~~>v y -> ((normh` ((T` y) -h y)) = 0 <-> ((T` y) -h y) = 0h))
177	176	adantl 544	. . . . . 6 |- ((f:NN-->H /\ f ~~>v y) -> ((normh` ((T` y) -h y)) = 0 <-> ((T` y) -h y) = 0h))
178	174, 177	mpbid 256	. . . . 5 |- ((f:NN-->H /\ f ~~>v y) -> ((T` y) -h y) = 0h)
179		hvsubeq0 11563	. . . . . . 7 |- (((T` y) e. ~H /\ y e. ~H) -> (((T` y) -h y) = 0h <-> (T` y) = y))
180	65, 61, 179	syl11anc 755	. . . . . 6 |- (f ~~>v y -> (((T` y) -h y) = 0h <-> (T` y) = y))
181	180	adantl 544	. . . . 5 |- ((f:NN-->H /\ f ~~>v y) -> (((T` y) -h y) = 0h <-> (T` y) = y))
182	178, 181	mpbid 256	. . . 4 |- ((f:NN-->H /\ f ~~>v y) -> (T` y) = y)
183	62, 182, 22	sylanbrc 760	. . 3 |- ((f:NN-->H /\ f ~~>v y) -> y e. H)
184	183	gen2 1647	. 2 |- A.fA.y((f:NN-->H /\ f ~~>v y) -> y e. H)
185	1, 58, 184	mpbir2an 1062	1 |- H e. CH

Syntax hints:   -> wi 3   <-> wb 231   /\ wa 433   /\ w3a 1130  A.wal 1613   = wceq 1615   e. wcel 1617  A.wral 2385  E.wrex 2386  {crab 2388   C_ wss 2859   class class class wbr 3539   o. ccom 4155  -->wf 4159  ` cfv 4163  (class class class)co 5020  CCcc 6827  RRcr 6828  0cc0 6829   + caddc 6832   x. cmul 6834   <_ cle 6943   < clt 6947   / cdiv 7093  NNcn 7094  2c2 7580  ~Hchil 11416   +h cva 11417   .h csm 11418  0hc0v 11419   -h cmv 11420  normhcno 11422   ~~>v chli 11424  SHcsh 11425  CHcch 11426  LinOpclo 11444  HrmOpcho 11447

This theorem is referenced by:  hmopidmpji 12713  hmopidmch 12714

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1619  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961  ax-inf2 6008  ax-cc 6359  ax-cnex 6885  ax-resscn 6886  ax-1cn 6887  ax-icn 6888  ax-addcl 6889  ax-addrcl 6890  ax-mulcl 6891  ax-mulrcl 6892  ax-mulcom 6893  ax-addass 6894  ax-mulass 6895  ax-distr 6896  ax-i2m1 6897  ax-1ne0 6898  ax-1rid 6899  ax-rnegex 6900  ax-rrecex 6901  ax-cnre 6902  ax-pre-lttri 6903  ax-pre-lttrn 6904  ax-pre-ltadd 6905  ax-pre-mulgt0 6906  ax-pre-sup 6907  ax-addopr 6908  ax-mulopr 6909  ax-hilex 11497  ax-hfvadd 11498  ax-hvcom 11499  ax-hvass 11500  ax-hv0cl 11501  ax-hvaddid 11502  ax-hfvmul 11503  ax-hvmulid 11504  ax-hvmulass 11505  ax-hvdistr1 11506  ax-hvdistr2 11507  ax-hvmul0 11508  ax-hfi 11574  ax-his1 11577  ax-his2 11578  ax-his3 11579  ax-his4 11580

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-nel 2298  df-ral 2389  df-rex 2390  df-reu 2391  df-rab 2392  df-v 2571  df-sbc 2731  df-csb 2806  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-int 3433  df-iun 3470  df-iin 3471  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-id 3779  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-lim 3848  df-suc 3849  df-om 4118  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-f1 4176  df-fo 4177  df-f1o 4178  df-fv 4179  df-opr 5022  df-oprab 5023  df-mpt 5138  df-1st 5166  df-2nd 5167  df-iota 5259  df-rdg 5344  df-er 5519  df-map 5587  df-en 5631  df-dom 5632  df-sdom 5633  df-undef 5769  df-riota 5773  df-sup 5932  df-pnf 6948  df-mnf 6949  df-xr 6950  df-ltxr 6951  df-le 6952  df-sub 7111  df-neg 7113  df-div 7325  df-n 7543  df-2 7589  df-3 7590  df-4 7591  df-n0 7761  df-z 7798  df-q 7894  df-fl 7921  df-ioo 7986  df-uz 8046  df-fz 8113  df-seq1 8210  df-shft 8245  df-seqz 8267  df-exp 8312  df-sqr 8420  df-re 8501  df-im 8502  df-cj 8503  df-abs 8504  df-clim 8747  df-sum 8752  df-top 9842  df-bases 9844  df-topgen 9845  df-cld 9950  df-ntr 9951  df-cls 9952  df-cn 10046  df-cnp 10047  df-haus 10075  df-met 10086  df-bl 10088  df-opn 10089  df-lm 10216  df-grpo 10334  df-gid 10335  df-ginv 10336  df-gdiv 10337  df-ablo 10429  df-vc 10518  df-nv 10564  df-va 10567  df-ba 10568  df-sm 10569  df-0v 10570  df-vs 10571  df-nm 10572  df-ims 10573  df-ip 10710  df-ph 10836  df-hnorm 11465  df-hvsub 11468  df-hlim 11469  df-sh 11703  df-ch 11717  df-lnop 12394  df-hmop 12397

Copyright terms: Public domain