Metamath Proof Explorer

Theorem hhcno

Description: The continuous operators of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses hhcn.1 ⊢D=normℎ∘-ℎ
hhcn.2 ⊢J=MetOpen⁡D
Assertion hhcno ⊢ContOp=JCnJ

Proof

Step Hyp Ref Expression
1 hhcn.1 ⊢D=normℎ∘-ℎ
2 hhcn.2 ⊢J=MetOpen⁡D
3 df-rab ⊢t∈ℋℋ|∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y=t|t∈ℋℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y
4 df-cnop ⊢ContOp=t∈ℋℋ|∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y
5 1 hilmetdval ⊢x∈ℋ∧w∈ℋ→xDw=normℎ⁡x-ℎw
6 normsub ⊢x∈ℋ∧w∈ℋ→normℎ⁡x-ℎw=normℎ⁡w-ℎx
7 5 6 eqtrd ⊢x∈ℋ∧w∈ℋ→xDw=normℎ⁡w-ℎx
8 7 adantll ⊢t:ℋ⟶ℋ∧x∈ℋ∧w∈ℋ→xDw=normℎ⁡w-ℎx
9 8 breq1d ⊢t:ℋ⟶ℋ∧x∈ℋ∧w∈ℋ→xDw<z↔normℎ⁡w-ℎx<z
10 ffvelcdm ⊢t:ℋ⟶ℋ∧x∈ℋ→t⁡x∈ℋ
11 ffvelcdm ⊢t:ℋ⟶ℋ∧w∈ℋ→t⁡w∈ℋ
12 10 11 anim12dan ⊢t:ℋ⟶ℋ∧x∈ℋ∧w∈ℋ→t⁡x∈ℋ∧t⁡w∈ℋ
13 1 hilmetdval ⊢t⁡x∈ℋ∧t⁡w∈ℋ→t⁡xDt⁡w=normℎ⁡t⁡x-ℎt⁡w
14 normsub ⊢t⁡x∈ℋ∧t⁡w∈ℋ→normℎ⁡t⁡x-ℎt⁡w=normℎ⁡t⁡w-ℎt⁡x
15 13 14 eqtrd ⊢t⁡x∈ℋ∧t⁡w∈ℋ→t⁡xDt⁡w=normℎ⁡t⁡w-ℎt⁡x
16 12 15 syl ⊢t:ℋ⟶ℋ∧x∈ℋ∧w∈ℋ→t⁡xDt⁡w=normℎ⁡t⁡w-ℎt⁡x
17 16 anassrs ⊢t:ℋ⟶ℋ∧x∈ℋ∧w∈ℋ→t⁡xDt⁡w=normℎ⁡t⁡w-ℎt⁡x
18 17 breq1d ⊢t:ℋ⟶ℋ∧x∈ℋ∧w∈ℋ→t⁡xDt⁡w<y↔normℎ⁡t⁡w-ℎt⁡x<y
19 9 18 imbi12d ⊢t:ℋ⟶ℋ∧x∈ℋ∧w∈ℋ→xDw<z→t⁡xDt⁡w<y↔normℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y
20 19 ralbidva ⊢t:ℋ⟶ℋ∧x∈ℋ→∀w∈ℋxDw<z→t⁡xDt⁡w<y↔∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y
21 20 rexbidv ⊢t:ℋ⟶ℋ∧x∈ℋ→∃z∈ℝ+∀w∈ℋxDw<z→t⁡xDt⁡w<y↔∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y
22 21 ralbidv ⊢t:ℋ⟶ℋ∧x∈ℋ→∀y∈ℝ+∃z∈ℝ+∀w∈ℋxDw<z→t⁡xDt⁡w<y↔∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y
23 22 ralbidva ⊢t:ℋ⟶ℋ→∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋxDw<z→t⁡xDt⁡w<y↔∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y
24 23 pm5.32i ⊢t:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋxDw<z→t⁡xDt⁡w<y↔t:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y
25 1 hilxmet ⊢D∈∞Met⁡ℋ
26 2 2 metcn ⊢D∈∞Met⁡ℋ∧D∈∞Met⁡ℋ→t∈JCnJ↔t:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋxDw<z→t⁡xDt⁡w<y
27 25 25 26 mp2an ⊢t∈JCnJ↔t:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋxDw<z→t⁡xDt⁡w<y
28 ax-hilex ⊢ℋ∈V
29 28 28 elmap ⊢t∈ℋℋ↔t:ℋ⟶ℋ
30 29 anbi1i ⊢t∈ℋℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y↔t:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y
31 24 27 30 3bitr4i ⊢t∈JCnJ↔t∈ℋℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y
32 31 eqabi ⊢JCnJ=t|t∈ℋℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y
33 3 4 32 3eqtr4i ⊢ContOp=JCnJ