Metamath Proof Explorer

Theorem 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 ⊢ 𝑇 ∈ HrmOp
hmopidmch.2 ⊢ ( 𝑇 ∘ 𝑇 ) = 𝑇
Assertion hmopidmchi ran 𝑇 ∈ Cℋ

Proof

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