Theorem hmopidmchi 31391

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.)

Hypotheses

Ref	Expression
hmopidmch.1	⊢ 𝑇 ∈ HrmOp
hmopidmch.2	⊢ (𝑇 ∘ 𝑇) = 𝑇

Assertion

Ref	Expression
hmopidmchi	⊢ ran 𝑇 ∈ Cℋ

Proof of Theorem hmopidmchi

Dummy variables 𝑓 𝑘 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hmopidmch.1	. . . 4 ⊢ 𝑇 ∈ HrmOp
2		hmoplin 31182	. . . 4 ⊢ (𝑇 ∈ HrmOp → 𝑇 ∈ LinOp)
3	1, 2	ax-mp 5	. . 3 ⊢ 𝑇 ∈ LinOp
4	3	rnelshi 31299	. 2 ⊢ ran 𝑇 ∈ Sℋ
5		eqid 2732	. . . . . . . 8 ⊢ (normℎ ∘ −ℎ ) = (normℎ ∘ −ℎ )
6	5	hilxmet 30435	. . . . . . 7 ⊢ (normℎ ∘ −ℎ ) ∈ (∞Met‘ ℋ)
7		eqid 2732	. . . . . . . 8 ⊢ (MetOpen‘(normℎ ∘ −ℎ )) = (MetOpen‘(normℎ ∘ −ℎ ))
8	7	methaus 24020	. . . . . . 7 ⊢ ((normℎ ∘ −ℎ ) ∈ (∞Met‘ ℋ) → (MetOpen‘(normℎ ∘ −ℎ )) ∈ Haus)
9	6, 8	mp1i 13	. . . . . 6 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → (MetOpen‘(normℎ ∘ −ℎ )) ∈ Haus)
10		eqid 2732	. . . . . . . . . . . 12 ⊢ ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
11	10, 5	hhims 30412	. . . . . . . . . . . 12 ⊢ (normℎ ∘ −ℎ ) = (IndMet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
12	10, 11, 7	hhlm 30439	. . . . . . . . . . 11 ⊢ ⇝𝑣 = ((⇝𝑡‘(MetOpen‘(normℎ ∘ −ℎ ))) ↾ ( ℋ ↑m ℕ))
13		resss 6004	. . . . . . . . . . 11 ⊢ ((⇝𝑡‘(MetOpen‘(normℎ ∘ −ℎ ))) ↾ ( ℋ ↑m ℕ)) ⊆ (⇝𝑡‘(MetOpen‘(normℎ ∘ −ℎ )))
14	12, 13	eqsstri 4015	. . . . . . . . . 10 ⊢ ⇝𝑣 ⊆ (⇝𝑡‘(MetOpen‘(normℎ ∘ −ℎ )))
15	14	ssbri 5192	. . . . . . . . 9 ⊢ (𝑓 ⇝𝑣 𝑥 → 𝑓(⇝𝑡‘(MetOpen‘(normℎ ∘ −ℎ )))𝑥)
16	15	adantl 482	. . . . . . . 8 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑓(⇝𝑡‘(MetOpen‘(normℎ ∘ −ℎ )))𝑥)
17	7	mopntopon 23936	. . . . . . . . . 10 ⊢ ((normℎ ∘ −ℎ ) ∈ (∞Met‘ ℋ) → (MetOpen‘(normℎ ∘ −ℎ )) ∈ (TopOn‘ ℋ))
18	6, 17	mp1i 13	. . . . . . . . 9 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → (MetOpen‘(normℎ ∘ −ℎ )) ∈ (TopOn‘ ℋ))
19	3	lnopfi 31209	. . . . . . . . . . . 12 ⊢ 𝑇: ℋ⟶ ℋ
20	19	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑇: ℋ⟶ ℋ)
21	20	feqmptd 6957	. . . . . . . . . 10 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑇 = (𝑦 ∈ ℋ ↦ (𝑇‘𝑦)))
22		hmopbdoptHIL 31228	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ HrmOp → 𝑇 ∈ BndLinOp)
23	1, 22	ax-mp 5	. . . . . . . . . . . 12 ⊢ 𝑇 ∈ BndLinOp
24		lnopcnbd 31276	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ LinOp → (𝑇 ∈ ContOp ↔ 𝑇 ∈ BndLinOp))
25	3, 24	ax-mp 5	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ContOp ↔ 𝑇 ∈ BndLinOp)
26	23, 25	mpbir 230	. . . . . . . . . . 11 ⊢ 𝑇 ∈ ContOp
27	5, 7	hhcno 31144	. . . . . . . . . . 11 ⊢ ContOp = ((MetOpen‘(normℎ ∘ −ℎ )) Cn (MetOpen‘(normℎ ∘ −ℎ )))
28	26, 27	eleqtri 2831	. . . . . . . . . 10 ⊢ 𝑇 ∈ ((MetOpen‘(normℎ ∘ −ℎ )) Cn (MetOpen‘(normℎ ∘ −ℎ )))
29	21, 28	eqeltrrdi 2842	. . . . . . . . 9 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → (𝑦 ∈ ℋ ↦ (𝑇‘𝑦)) ∈ ((MetOpen‘(normℎ ∘ −ℎ )) Cn (MetOpen‘(normℎ ∘ −ℎ ))))
30	18	cnmptid 23156	. . . . . . . . 9 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → (𝑦 ∈ ℋ ↦ 𝑦) ∈ ((MetOpen‘(normℎ ∘ −ℎ )) Cn (MetOpen‘(normℎ ∘ −ℎ ))))
31	10	hhnv 30405	. . . . . . . . . 10 ⊢ ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ ∈ NrmCVec
32	10	hhvs 30410	. . . . . . . . . . 11 ⊢ −ℎ = ( −𝑣 ‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
33	11, 7, 32	vmcn 29939	. . . . . . . . . 10 ⊢ (⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ ∈ NrmCVec → −ℎ ∈ (((MetOpen‘(normℎ ∘ −ℎ )) ×t (MetOpen‘(normℎ ∘ −ℎ ))) Cn (MetOpen‘(normℎ ∘ −ℎ ))))
34	31, 33	mp1i 13	. . . . . . . . 9 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → −ℎ ∈ (((MetOpen‘(normℎ ∘ −ℎ )) ×t (MetOpen‘(normℎ ∘ −ℎ ))) Cn (MetOpen‘(normℎ ∘ −ℎ ))))
35	18, 29, 30, 34	cnmpt12f 23161	. . . . . . . 8 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → (𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦)) ∈ ((MetOpen‘(normℎ ∘ −ℎ )) Cn (MetOpen‘(normℎ ∘ −ℎ ))))
36	16, 35	lmcn 22800	. . . . . . 7 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → ((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦)) ∘ 𝑓)(⇝𝑡‘(MetOpen‘(normℎ ∘ −ℎ )))((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦))‘𝑥))
37		simpl 483	. . . . . . . . . . . . . 14 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑓:ℕ⟶ran 𝑇)
38	4	shssii 30453	. . . . . . . . . . . . . 14 ⊢ ran 𝑇 ⊆ ℋ
39		fss 6731	. . . . . . . . . . . . . 14 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ ran 𝑇 ⊆ ℋ) → 𝑓:ℕ⟶ ℋ)
40	37, 38, 39	sylancl 586	. . . . . . . . . . . . 13 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑓:ℕ⟶ ℋ)
41	40	ffvelcdmda 7083	. . . . . . . . . . . 12 ⊢ (((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ ℋ)
42		fveq2 6888	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑓‘𝑘) → (𝑇‘𝑦) = (𝑇‘(𝑓‘𝑘)))
43		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑓‘𝑘) → 𝑦 = (𝑓‘𝑘))
44	42, 43	oveq12d 7423	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑓‘𝑘) → ((𝑇‘𝑦) −ℎ 𝑦) = ((𝑇‘(𝑓‘𝑘)) −ℎ (𝑓‘𝑘)))
45		eqid 2732	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦)) = (𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦))
46		ovex 7438	. . . . . . . . . . . . 13 ⊢ ((𝑇‘(𝑓‘𝑘)) −ℎ (𝑓‘𝑘)) ∈ V
47	44, 45, 46	fvmpt 6995	. . . . . . . . . . . 12 ⊢ ((𝑓‘𝑘) ∈ ℋ → ((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦))‘(𝑓‘𝑘)) = ((𝑇‘(𝑓‘𝑘)) −ℎ (𝑓‘𝑘)))
48	41, 47	syl 17	. . . . . . . . . . 11 ⊢ (((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑘 ∈ ℕ) → ((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦))‘(𝑓‘𝑘)) = ((𝑇‘(𝑓‘𝑘)) −ℎ (𝑓‘𝑘)))
49		ffn 6714	. . . . . . . . . . . . . . . 16 ⊢ (𝑇: ℋ⟶ ℋ → 𝑇 Fn ℋ)
50	19, 49	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 𝑇 Fn ℋ
51		fveq2 6888	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑇‘𝑥) → (𝑇‘𝑦) = (𝑇‘(𝑇‘𝑥)))
52		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑇‘𝑥) → 𝑦 = (𝑇‘𝑥))
53	51, 52	eqeq12d 2748	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑇‘𝑥) → ((𝑇‘𝑦) = 𝑦 ↔ (𝑇‘(𝑇‘𝑥)) = (𝑇‘𝑥)))
54	53	ralrn 7086	. . . . . . . . . . . . . . 15 ⊢ (𝑇 Fn ℋ → (∀𝑦 ∈ ran 𝑇(𝑇‘𝑦) = 𝑦 ↔ ∀𝑥 ∈ ℋ (𝑇‘(𝑇‘𝑥)) = (𝑇‘𝑥)))
55	50, 54	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (∀𝑦 ∈ ran 𝑇(𝑇‘𝑦) = 𝑦 ↔ ∀𝑥 ∈ ℋ (𝑇‘(𝑇‘𝑥)) = (𝑇‘𝑥))
56	19, 19	hocoi 31004	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℋ → ((𝑇 ∘ 𝑇)‘𝑥) = (𝑇‘(𝑇‘𝑥)))
57		hmopidmch.2	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∘ 𝑇) = 𝑇
58	57	fveq1i 6889	. . . . . . . . . . . . . . 15 ⊢ ((𝑇 ∘ 𝑇)‘𝑥) = (𝑇‘𝑥)
59	56, 58	eqtr3di 2787	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℋ → (𝑇‘(𝑇‘𝑥)) = (𝑇‘𝑥))
60	55, 59	mprgbir 3068	. . . . . . . . . . . . 13 ⊢ ∀𝑦 ∈ ran 𝑇(𝑇‘𝑦) = 𝑦
61		ffvelcdm 7080	. . . . . . . . . . . . . 14 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ ran 𝑇)
62	61	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ ran 𝑇)
63	42, 43	eqeq12d 2748	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑓‘𝑘) → ((𝑇‘𝑦) = 𝑦 ↔ (𝑇‘(𝑓‘𝑘)) = (𝑓‘𝑘)))
64	63	rspccv 3609	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ ran 𝑇(𝑇‘𝑦) = 𝑦 → ((𝑓‘𝑘) ∈ ran 𝑇 → (𝑇‘(𝑓‘𝑘)) = (𝑓‘𝑘)))
65	60, 62, 64	mpsyl 68	. . . . . . . . . . . 12 ⊢ (((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑘 ∈ ℕ) → (𝑇‘(𝑓‘𝑘)) = (𝑓‘𝑘))
66	65, 41	eqeltrd 2833	. . . . . . . . . . . . 13 ⊢ (((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑘 ∈ ℕ) → (𝑇‘(𝑓‘𝑘)) ∈ ℋ)
67		hvsubeq0 30308	. . . . . . . . . . . . 13 ⊢ (((𝑇‘(𝑓‘𝑘)) ∈ ℋ ∧ (𝑓‘𝑘) ∈ ℋ) → (((𝑇‘(𝑓‘𝑘)) −ℎ (𝑓‘𝑘)) = 0ℎ ↔ (𝑇‘(𝑓‘𝑘)) = (𝑓‘𝑘)))
68	66, 41, 67	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑘 ∈ ℕ) → (((𝑇‘(𝑓‘𝑘)) −ℎ (𝑓‘𝑘)) = 0ℎ ↔ (𝑇‘(𝑓‘𝑘)) = (𝑓‘𝑘)))
69	65, 68	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑘 ∈ ℕ) → ((𝑇‘(𝑓‘𝑘)) −ℎ (𝑓‘𝑘)) = 0ℎ)
70	48, 69	eqtrd 2772	. . . . . . . . . 10 ⊢ (((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑘 ∈ ℕ) → ((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦))‘(𝑓‘𝑘)) = 0ℎ)
71		fvco3 6987	. . . . . . . . . . 11 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑘 ∈ ℕ) → (((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦)) ∘ 𝑓)‘𝑘) = ((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦))‘(𝑓‘𝑘)))
72	71	adantlr 713	. . . . . . . . . 10 ⊢ (((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑘 ∈ ℕ) → (((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦)) ∘ 𝑓)‘𝑘) = ((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦))‘(𝑓‘𝑘)))
73		ax-hv0cl 30243	. . . . . . . . . . . . 13 ⊢ 0ℎ ∈ ℋ
74	73	elexi 3493	. . . . . . . . . . . 12 ⊢ 0ℎ ∈ V
75	74	fvconst2 7201	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((ℕ × {0ℎ})‘𝑘) = 0ℎ)
76	75	adantl 482	. . . . . . . . . 10 ⊢ (((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑘 ∈ ℕ) → ((ℕ × {0ℎ})‘𝑘) = 0ℎ)
77	70, 72, 76	3eqtr4d 2782	. . . . . . . . 9 ⊢ (((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) ∧ 𝑘 ∈ ℕ) → (((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦)) ∘ 𝑓)‘𝑘) = ((ℕ × {0ℎ})‘𝑘))
78	77	ralrimiva 3146	. . . . . . . 8 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → ∀𝑘 ∈ ℕ (((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦)) ∘ 𝑓)‘𝑘) = ((ℕ × {0ℎ})‘𝑘))
79		ovex 7438	. . . . . . . . . . 11 ⊢ ((𝑇‘𝑦) −ℎ 𝑦) ∈ V
80	79, 45	fnmpti 6690	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦)) Fn ℋ
81		fnfco 6753	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦)) Fn ℋ ∧ 𝑓:ℕ⟶ ℋ) → ((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦)) ∘ 𝑓) Fn ℕ)
82	80, 40, 81	sylancr 587	. . . . . . . . 9 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → ((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦)) ∘ 𝑓) Fn ℕ)
83	74	fconst 6774	. . . . . . . . . 10 ⊢ (ℕ × {0ℎ}):ℕ⟶{0ℎ}
84		ffn 6714	. . . . . . . . . 10 ⊢ ((ℕ × {0ℎ}):ℕ⟶{0ℎ} → (ℕ × {0ℎ}) Fn ℕ)
85	83, 84	ax-mp 5	. . . . . . . . 9 ⊢ (ℕ × {0ℎ}) Fn ℕ
86		eqfnfv 7029	. . . . . . . . 9 ⊢ ((((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦)) ∘ 𝑓) Fn ℕ ∧ (ℕ × {0ℎ}) Fn ℕ) → (((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦)) ∘ 𝑓) = (ℕ × {0ℎ}) ↔ ∀𝑘 ∈ ℕ (((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦)) ∘ 𝑓)‘𝑘) = ((ℕ × {0ℎ})‘𝑘)))
87	82, 85, 86	sylancl 586	. . . . . . . 8 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → (((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦)) ∘ 𝑓) = (ℕ × {0ℎ}) ↔ ∀𝑘 ∈ ℕ (((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦)) ∘ 𝑓)‘𝑘) = ((ℕ × {0ℎ})‘𝑘)))
88	78, 87	mpbird 256	. . . . . . 7 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → ((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦)) ∘ 𝑓) = (ℕ × {0ℎ}))
89		vex 3478	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
90	89	hlimveci 30430	. . . . . . . . 9 ⊢ (𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ ℋ)
91	90	adantl 482	. . . . . . . 8 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ ℋ)
92		fveq2 6888	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (𝑇‘𝑦) = (𝑇‘𝑥))
93		id 22	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → 𝑦 = 𝑥)
94	92, 93	oveq12d 7423	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → ((𝑇‘𝑦) −ℎ 𝑦) = ((𝑇‘𝑥) −ℎ 𝑥))
95		ovex 7438	. . . . . . . . 9 ⊢ ((𝑇‘𝑥) −ℎ 𝑥) ∈ V
96	94, 45, 95	fvmpt 6995	. . . . . . . 8 ⊢ (𝑥 ∈ ℋ → ((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦))‘𝑥) = ((𝑇‘𝑥) −ℎ 𝑥))
97	91, 96	syl 17	. . . . . . 7 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → ((𝑦 ∈ ℋ ↦ ((𝑇‘𝑦) −ℎ 𝑦))‘𝑥) = ((𝑇‘𝑥) −ℎ 𝑥))
98	36, 88, 97	3brtr3d 5178	. . . . . 6 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → (ℕ × {0ℎ})(⇝𝑡‘(MetOpen‘(normℎ ∘ −ℎ )))((𝑇‘𝑥) −ℎ 𝑥))
99	73	a1i 11	. . . . . . 7 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → 0ℎ ∈ ℋ)
100		1zzd 12589	. . . . . . 7 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → 1 ∈ ℤ)
101		nnuz 12861	. . . . . . . 8 ⊢ ℕ = (ℤ≥‘1)
102	101	lmconst 22756	. . . . . . 7 ⊢ (((MetOpen‘(normℎ ∘ −ℎ )) ∈ (TopOn‘ ℋ) ∧ 0ℎ ∈ ℋ ∧ 1 ∈ ℤ) → (ℕ × {0ℎ})(⇝𝑡‘(MetOpen‘(normℎ ∘ −ℎ )))0ℎ)
103	18, 99, 100, 102	syl3anc 1371	. . . . . 6 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → (ℕ × {0ℎ})(⇝𝑡‘(MetOpen‘(normℎ ∘ −ℎ )))0ℎ)
104	9, 98, 103	lmmo 22875	. . . . 5 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → ((𝑇‘𝑥) −ℎ 𝑥) = 0ℎ)
105	19	ffvelcdmi 7082	. . . . . . 7 ⊢ (𝑥 ∈ ℋ → (𝑇‘𝑥) ∈ ℋ)
106	91, 105	syl 17	. . . . . 6 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → (𝑇‘𝑥) ∈ ℋ)
107		hvsubeq0 30308	. . . . . 6 ⊢ (((𝑇‘𝑥) ∈ ℋ ∧ 𝑥 ∈ ℋ) → (((𝑇‘𝑥) −ℎ 𝑥) = 0ℎ ↔ (𝑇‘𝑥) = 𝑥))
108	106, 91, 107	syl2anc 584	. . . . 5 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → (((𝑇‘𝑥) −ℎ 𝑥) = 0ℎ ↔ (𝑇‘𝑥) = 𝑥))
109	104, 108	mpbid 231	. . . 4 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → (𝑇‘𝑥) = 𝑥)
110		fnfvelrn 7079	. . . . 5 ⊢ ((𝑇 Fn ℋ ∧ 𝑥 ∈ ℋ) → (𝑇‘𝑥) ∈ ran 𝑇)
111	50, 91, 110	sylancr 587	. . . 4 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → (𝑇‘𝑥) ∈ ran 𝑇)
112	109, 111	eqeltrrd 2834	. . 3 ⊢ ((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ ran 𝑇)
113	112	gen2 1798	. 2 ⊢ ∀𝑓∀𝑥((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ ran 𝑇)
114		isch2 30463	. 2 ⊢ (ran 𝑇 ∈ Cℋ ↔ (ran 𝑇 ∈ Sℋ ∧ ∀𝑓∀𝑥((𝑓:ℕ⟶ran 𝑇 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ ran 𝑇)))
115	4, 113, 114	mpbir2an 709	1 ⊢ ran 𝑇 ∈ Cℋ

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1539   = wceq 1541   ∈ wcel 2106  ∀wral 3061   ⊆ wss 3947  {csn 4627  ⟨cop 4633   class class class wbr 5147   ↦ cmpt 5230   × cxp 5673  ran crn 5676   ↾ cres 5677   ∘ ccom 5679   Fn wfn 6535  ⟶wf 6536  ‘cfv 6540  (class class class)co 7405   ↑_m cmap 8816  1c1 11107  ℕcn 12208  ℤcz 12554  ∞Metcxmet 20921  MetOpencmopn 20926  TopOnctopon 22403   Cn ccn 22719  ⇝_𝑡clm 22721  Hauscha 22803   ×_t ctx 23055  NrmCVeccnv 29824   ℋchba 30159   +_ℎ cva 30160   ·_ℎ csm 30161  norm_ℎcno 30163  0_ℎc0v 30164   −_ℎ cmv 30165   ⇝_𝑣 chli 30167   S_ℋ csh 30168   C_ℋ cch 30169  ContOpccop 30186  LinOpclo 30187  BndLinOpcbo 30188  HrmOpcho 30190

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-cc 10426  ax-dc 10437  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186  ax-hilex 30239  ax-hfvadd 30240  ax-hvcom 30241  ax-hvass 30242  ax-hv0cl 30243  ax-hvaddid 30244  ax-hfvmul 30245  ax-hvmulid 30246  ax-hvmulass 30247  ax-hvdistr1 30248  ax-hvdistr2 30249  ax-hvmul0 30250  ax-hfi 30319  ax-his1 30322  ax-his2 30323  ax-his3 30324  ax-his4 30325  ax-hcompl 30442

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666  df-om 7852  df-1st 7971  df-2nd 7972  df-supp 8143  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-oadd 8466  df-omul 8467  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  df-acn 9933  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-ioo 13324  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-seq 13963  df-exp 14024  df-hash 14287  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-clim 15428  df-rlim 15429  df-sum 15629  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-rest 17364  df-topn 17365  df-0g 17383  df-gsum 17384  df-topgen 17385  df-pt 17386  df-prds 17389  df-xrs 17444  df-qtop 17449  df-imas 17450  df-xps 17452  df-mre 17526  df-mrc 17527  df-acs 17529  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-submnd 18668  df-mulg 18945  df-cntz 19175  df-cmn 19644  df-psmet 20928  df-xmet 20929  df-met 20930  df-bl 20931  df-mopn 20932  df-fbas 20933  df-fg 20934  df-cnfld 20937  df-top 22387  df-topon 22404  df-topsp 22426  df-bases 22440  df-cld 22514  df-ntr 22515  df-cls 22516  df-nei 22593  df-cn 22722  df-cnp 22723  df-lm 22724  df-t1 22809  df-haus 22810  df-cmp 22882  df-tx 23057  df-hmeo 23250  df-fil 23341  df-fm 23433  df-flim 23434  df-flf 23435  df-fcls 23436  df-xms 23817  df-ms 23818  df-tms 23819  df-cncf 24385  df-cfil 24763  df-cau 24764  df-cmet 24765  df-grpo 29733  df-gid 29734  df-ginv 29735  df-gdiv 29736  df-ablo 29785  df-vc 29799  df-nv 29832  df-va 29835  df-ba 29836  df-sm 29837  df-0v 29838  df-vs 29839  df-nmcv 29840  df-ims 29841  df-dip 29941  df-ssp 29962  df-lno 29984  df-nmoo 29985  df-blo 29986  df-0o 29987  df-ph 30053  df-cbn 30103  df-hlo 30126  df-hnorm 30208  df-hba 30209  df-hvsub 30211  df-hlim 30212  df-hcau 30213  df-sh 30447  df-ch 30461  df-oc 30492  df-ch0 30493  df-shs 30548  df-pjh 30635  df-h0op 30988  df-nmop 31079  df-cnop 31080  df-lnop 31081  df-bdop 31082  df-unop 31083  df-hmop 31084

This theorem is referenced by:  hmopidmpji  31392  hmopidmch  31393