hmopidmchi

Description: An idempotent Hermitian operator generates a closed subspace. Part of proof of Theorem of AkhiezerGlazman p. 64. (Contributed by NM, 21-Apr-2006) (Proof shortened by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hmopidmch.1	$⊢ T \in HrmOp$
	hmopidmch.2	$⊢ T \circ T = T$
Assertion	hmopidmchi	$⊢ ran T \in C_{ℋ}$

Proof

Step	Hyp	Ref	Expression
1		hmopidmch.1	$⊢ T \in HrmOp$
2		hmopidmch.2	$⊢ T \circ T = T$
3		hmoplin	$⊢ T \in HrmOp \to T \in LinOp$
4	1 3	ax-mp	$⊢ T \in LinOp$
5	4	rnelshi	$⊢ ran T \in S_{ℋ}$
6		eqid	$⊢ {norm}_{ℎ} \circ -_{ℎ} = {norm}_{ℎ} \circ -_{ℎ}$
7	6	hilxmet	$⊢ {norm}_{ℎ} \circ -_{ℎ} \in ∞Met (ℋ)$
8		eqid	$⊢ MetOpen ({norm}_{ℎ} \circ -_{ℎ}) = MetOpen ({norm}_{ℎ} \circ -_{ℎ})$
9	8	methaus	$⊢ {norm}_{ℎ} \circ -_{ℎ} \in ∞Met (ℋ) \to MetOpen ({norm}_{ℎ} \circ -_{ℎ}) \in Haus$
10	7 9	mp1i	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to MetOpen ({norm}_{ℎ} \circ -_{ℎ}) \in Haus$
11		eqid	$⊢ ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩ = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
12	11 6	hhims	$⊢ {norm}_{ℎ} \circ -_{ℎ} = IndMet (⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩)$
13	11 12 8	hhlm	$⊢ \underset{v}{⇝} = {\underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ})) ↾}_{(ℋ^{ℕ})}$
14		resss	$⊢ {\underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ})) ↾}_{(ℋ^{ℕ})} \subseteq \underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ}))$
15	13 14	eqsstri	$⊢ \underset{v}{⇝} \subseteq \underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ}))$
16	15	ssbri	$⊢ f \underset{v}{⇝} x \to f \underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ})) x$
17	16	adantl	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to f \underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ})) x$
18	8	mopntopon	$⊢ {norm}_{ℎ} \circ -_{ℎ} \in ∞Met (ℋ) \to MetOpen ({norm}_{ℎ} \circ -_{ℎ}) \in TopOn (ℋ)$
19	7 18	mp1i	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to MetOpen ({norm}_{ℎ} \circ -_{ℎ}) \in TopOn (ℋ)$
20	4	lnopfi	$⊢ T : ℋ ⟶ ℋ$
21	20	a1i	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to T : ℋ ⟶ ℋ$
22	21	feqmptd	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to T = (y \in ℋ ⟼ T (y))$
23		hmopbdoptHIL	$⊢ T \in HrmOp \to T \in BndLinOp$
24	1 23	ax-mp	$⊢ T \in BndLinOp$
25		lnopcnbd	$⊢ T \in LinOp \to (T \in ContOp \leftrightarrow T \in BndLinOp)$
26	4 25	ax-mp	$⊢ T \in ContOp \leftrightarrow T \in BndLinOp$
27	24 26	mpbir	$⊢ T \in ContOp$
28	6 8	hhcno	$⊢ ContOp = MetOpen ({norm}_{ℎ} \circ -_{ℎ}) Cn MetOpen ({norm}_{ℎ} \circ -_{ℎ})$
29	27 28	eleqtri	$⊢ T \in (MetOpen ({norm}_{ℎ} \circ -_{ℎ}) Cn MetOpen ({norm}_{ℎ} \circ -_{ℎ}))$
30	22 29	eqeltrrdi	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to (y \in ℋ ⟼ T (y)) \in (MetOpen ({norm}_{ℎ} \circ -_{ℎ}) Cn MetOpen ({norm}_{ℎ} \circ -_{ℎ}))$
31	19	cnmptid	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to (y \in ℋ ⟼ y) \in (MetOpen ({norm}_{ℎ} \circ -_{ℎ}) Cn MetOpen ({norm}_{ℎ} \circ -_{ℎ}))$
32	11	hhnv	$⊢ ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩ \in NrmCVec$
33	11	hhvs	$⊢ -_{ℎ} = -_{v} (⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩)$
34	12 8 33	vmcn	$⊢ ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩ \in NrmCVec \to -_{ℎ} \in ((MetOpen ({norm}_{ℎ} \circ -_{ℎ}) \times_{t} MetOpen ({norm}_{ℎ} \circ -_{ℎ})) Cn MetOpen ({norm}_{ℎ} \circ -_{ℎ}))$
35	32 34	mp1i	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to -_{ℎ} \in ((MetOpen ({norm}_{ℎ} \circ -_{ℎ}) \times_{t} MetOpen ({norm}_{ℎ} \circ -_{ℎ})) Cn MetOpen ({norm}_{ℎ} \circ -_{ℎ}))$
36	19 30 31 35	cnmpt12f	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to (y \in ℋ ⟼ T (y) -_{ℎ} y) \in (MetOpen ({norm}_{ℎ} \circ -_{ℎ}) Cn MetOpen ({norm}_{ℎ} \circ -_{ℎ}))$
37	17 36	lmcn	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to ((y \in ℋ ⟼ T (y) -_{ℎ} y) \circ f) \underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ})) (y \in ℋ ⟼ T (y) -_{ℎ} y) (x)$
38		simpl	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to f : ℕ ⟶ ran T$
39	5	shssii	$⊢ ran T \subseteq ℋ$
40		fss	$⊢ (f : ℕ ⟶ ran T \land ran T \subseteq ℋ) \to f : ℕ ⟶ ℋ$
41	38 39 40	sylancl	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to f : ℕ ⟶ ℋ$
42	41	ffvelcdmda	$⊢ ((f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \land k \in ℕ) \to f (k) \in ℋ$
43		fveq2	$⊢ y = f (k) \to T (y) = T (f (k))$
44		id	$⊢ y = f (k) \to y = f (k)$
45	43 44	oveq12d	$⊢ y = f (k) \to T (y) -_{ℎ} y = T (f (k)) -_{ℎ} f (k)$
46		eqid	$⊢ (y \in ℋ ⟼ T (y) -_{ℎ} y) = (y \in ℋ ⟼ T (y) -_{ℎ} y)$
47		ovex	$⊢ T (f (k)) -_{ℎ} f (k) \in V$
48	45 46 47	fvmpt	$⊢ f (k) \in ℋ \to (y \in ℋ ⟼ T (y) -_{ℎ} y) (f (k)) = T (f (k)) -_{ℎ} f (k)$
49	42 48	syl	$⊢ ((f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \land k \in ℕ) \to (y \in ℋ ⟼ T (y) -_{ℎ} y) (f (k)) = T (f (k)) -_{ℎ} f (k)$
50		ffn	$⊢ T : ℋ ⟶ ℋ \to T Fn ℋ$
51	20 50	ax-mp	$⊢ T Fn ℋ$
52		fveq2	$⊢ y = T (x) \to T (y) = T (T (x))$
53		id	$⊢ y = T (x) \to y = T (x)$
54	52 53	eqeq12d	$⊢ y = T (x) \to (T (y) = y \leftrightarrow T (T (x)) = T (x))$
55	54	ralrn	$⊢ T Fn ℋ \to (\forall y \in ran T T (y) = y \leftrightarrow \forall x \in ℋ T (T (x)) = T (x))$
56	51 55	ax-mp	$⊢ \forall y \in ran T T (y) = y \leftrightarrow \forall x \in ℋ T (T (x)) = T (x)$
57	20 20	hocoi	$⊢ x \in ℋ \to (T \circ T) (x) = T (T (x))$
58	2	fveq1i	$⊢ (T \circ T) (x) = T (x)$
59	57 58	eqtr3di	$⊢ x \in ℋ \to T (T (x)) = T (x)$
60	56 59	mprgbir	$⊢ \forall y \in ran T T (y) = y$
61		ffvelcdm	$⊢ (f : ℕ ⟶ ran T \land k \in ℕ) \to f (k) \in ran T$
62	61	adantlr	$⊢ ((f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \land k \in ℕ) \to f (k) \in ran T$
63	43 44	eqeq12d	$⊢ y = f (k) \to (T (y) = y \leftrightarrow T (f (k)) = f (k))$
64	63	rspccv	$⊢ \forall y \in ran T T (y) = y \to (f (k) \in ran T \to T (f (k)) = f (k))$
65	60 62 64	mpsyl	$⊢ ((f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \land k \in ℕ) \to T (f (k)) = f (k)$
66	65 42	eqeltrd	$⊢ ((f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \land k \in ℕ) \to T (f (k)) \in ℋ$
67		hvsubeq0	$⊢ (T (f (k)) \in ℋ \land f (k) \in ℋ) \to (T (f (k)) -_{ℎ} f (k) = 0_{ℎ} \leftrightarrow T (f (k)) = f (k))$
68	66 42 67	syl2anc	$⊢ ((f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \land k \in ℕ) \to (T (f (k)) -_{ℎ} f (k) = 0_{ℎ} \leftrightarrow T (f (k)) = f (k))$
69	65 68	mpbird	$⊢ ((f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \land k \in ℕ) \to T (f (k)) -_{ℎ} f (k) = 0_{ℎ}$
70	49 69	eqtrd	$⊢ ((f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \land k \in ℕ) \to (y \in ℋ ⟼ T (y) -_{ℎ} y) (f (k)) = 0_{ℎ}$
71		fvco3	$⊢ (f : ℕ ⟶ ran T \land k \in ℕ) \to ((y \in ℋ ⟼ T (y) -_{ℎ} y) \circ f) (k) = (y \in ℋ ⟼ T (y) -_{ℎ} y) (f (k))$
72	71	adantlr	$⊢ ((f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \land k \in ℕ) \to ((y \in ℋ ⟼ T (y) -_{ℎ} y) \circ f) (k) = (y \in ℋ ⟼ T (y) -_{ℎ} y) (f (k))$
73		ax-hv0cl	$⊢ 0_{ℎ} \in ℋ$
74	73	elexi	$⊢ 0_{ℎ} \in V$
75	74	fvconst2	$⊢ k \in ℕ \to (ℕ \times \{0_{ℎ}\}) (k) = 0_{ℎ}$
76	75	adantl	$⊢ ((f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \land k \in ℕ) \to (ℕ \times \{0_{ℎ}\}) (k) = 0_{ℎ}$
77	70 72 76	3eqtr4d	$⊢ ((f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \land k \in ℕ) \to ((y \in ℋ ⟼ T (y) -_{ℎ} y) \circ f) (k) = (ℕ \times \{0_{ℎ}\}) (k)$
78	77	ralrimiva	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to \forall k \in ℕ ((y \in ℋ ⟼ T (y) -_{ℎ} y) \circ f) (k) = (ℕ \times \{0_{ℎ}\}) (k)$
79		ovex	$⊢ T (y) -_{ℎ} y \in V$
80	79 46	fnmpti	$⊢ (y \in ℋ ⟼ T (y) -_{ℎ} y) Fn ℋ$
81		fnfco	$⊢ ((y \in ℋ ⟼ T (y) -_{ℎ} y) Fn ℋ \land f : ℕ ⟶ ℋ) \to ((y \in ℋ ⟼ T (y) -_{ℎ} y) \circ f) Fn ℕ$
82	80 41 81	sylancr	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to ((y \in ℋ ⟼ T (y) -_{ℎ} y) \circ f) Fn ℕ$
83	74	fconst	$⊢ (ℕ \times \{0_{ℎ}\}) : ℕ ⟶ \{0_{ℎ}\}$
84		ffn	$⊢ (ℕ \times \{0_{ℎ}\}) : ℕ ⟶ \{0_{ℎ}\} \to (ℕ \times \{0_{ℎ}\}) Fn ℕ$
85	83 84	ax-mp	$⊢ (ℕ \times \{0_{ℎ}\}) Fn ℕ$
86		eqfnfv	$⊢ (((y \in ℋ ⟼ T (y) -_{ℎ} y) \circ f) Fn ℕ \land (ℕ \times \{0_{ℎ}\}) Fn ℕ) \to ((y \in ℋ ⟼ T (y) -_{ℎ} y) \circ f = ℕ \times \{0_{ℎ}\} \leftrightarrow \forall k \in ℕ ((y \in ℋ ⟼ T (y) -_{ℎ} y) \circ f) (k) = (ℕ \times \{0_{ℎ}\}) (k))$
87	82 85 86	sylancl	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to ((y \in ℋ ⟼ T (y) -_{ℎ} y) \circ f = ℕ \times \{0_{ℎ}\} \leftrightarrow \forall k \in ℕ ((y \in ℋ ⟼ T (y) -_{ℎ} y) \circ f) (k) = (ℕ \times \{0_{ℎ}\}) (k))$
88	78 87	mpbird	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to (y \in ℋ ⟼ T (y) -_{ℎ} y) \circ f = ℕ \times \{0_{ℎ}\}$
89		vex	$⊢ x \in V$
90	89	hlimveci	$⊢ f \underset{v}{⇝} x \to x \in ℋ$
91	90	adantl	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to x \in ℋ$
92		fveq2	$⊢ y = x \to T (y) = T (x)$
93		id	$⊢ y = x \to y = x$
94	92 93	oveq12d	$⊢ y = x \to T (y) -_{ℎ} y = T (x) -_{ℎ} x$
95		ovex	$⊢ T (x) -_{ℎ} x \in V$
96	94 46 95	fvmpt	$⊢ x \in ℋ \to (y \in ℋ ⟼ T (y) -_{ℎ} y) (x) = T (x) -_{ℎ} x$
97	91 96	syl	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to (y \in ℋ ⟼ T (y) -_{ℎ} y) (x) = T (x) -_{ℎ} x$
98	37 88 97	3brtr3d	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to (ℕ \times \{0_{ℎ}\}) \underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ})) (T (x) -_{ℎ} x)$
99	73	a1i	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to 0_{ℎ} \in ℋ$
100		1zzd	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to 1 \in ℤ$
101		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
102	101	lmconst	$⊢ (MetOpen ({norm}_{ℎ} \circ -_{ℎ}) \in TopOn (ℋ) \land 0_{ℎ} \in ℋ \land 1 \in ℤ) \to (ℕ \times \{0_{ℎ}\}) \underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ})) 0_{ℎ}$
103	19 99 100 102	syl3anc	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to (ℕ \times \{0_{ℎ}\}) \underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ})) 0_{ℎ}$
104	10 98 103	lmmo	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to T (x) -_{ℎ} x = 0_{ℎ}$
105	20	ffvelcdmi	$⊢ x \in ℋ \to T (x) \in ℋ$
106	91 105	syl	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to T (x) \in ℋ$
107		hvsubeq0	$⊢ (T (x) \in ℋ \land x \in ℋ) \to (T (x) -_{ℎ} x = 0_{ℎ} \leftrightarrow T (x) = x)$
108	106 91 107	syl2anc	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to (T (x) -_{ℎ} x = 0_{ℎ} \leftrightarrow T (x) = x)$
109	104 108	mpbid	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to T (x) = x$
110		fnfvelrn	$⊢ (T Fn ℋ \land x \in ℋ) \to T (x) \in ran T$
111	51 91 110	sylancr	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to T (x) \in ran T$
112	109 111	eqeltrrd	$⊢ (f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to x \in ran T$
113	112	gen2	$⊢ \forall f \forall x ((f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to x \in ran T)$
114		isch2	$⊢ ran T \in C_{ℋ} \leftrightarrow (ran T \in S_{ℋ} \land \forall f \forall x ((f : ℕ ⟶ ran T \land f \underset{v}{⇝} x) \to x \in ran T))$
115	5 113 114	mpbir2an	$⊢ ran T \in C_{ℋ}$

Metamath Proof Explorer

Theorem hmopidmchi

Proof