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 𝐷 = ( norm ∘ − )
hhcn.2 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion hhcno ContOp = ( 𝐽 Cn 𝐽 )

Proof

Step Hyp Ref Expression
1 hhcn.1 𝐷 = ( norm ∘ − )
2 hhcn.2 𝐽 = ( MetOpen ‘ 𝐷 )
3 df-rab { 𝑡 ∈ ( ℋ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ( ( norm ‘ ( 𝑤 𝑥 ) ) < 𝑧 → ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) < 𝑦 ) } = { 𝑡 ∣ ( 𝑡 ∈ ( ℋ ↑m ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ( ( norm ‘ ( 𝑤 𝑥 ) ) < 𝑧 → ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) < 𝑦 ) ) }
4 df-cnop ContOp = { 𝑡 ∈ ( ℋ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ( ( norm ‘ ( 𝑤 𝑥 ) ) < 𝑧 → ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) < 𝑦 ) }
5 1 hilmetdval ( ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( 𝑥 𝐷 𝑤 ) = ( norm ‘ ( 𝑥 𝑤 ) ) )
6 normsub ( ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( norm ‘ ( 𝑥 𝑤 ) ) = ( norm ‘ ( 𝑤 𝑥 ) ) )
7 5 6 eqtrd ( ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( 𝑥 𝐷 𝑤 ) = ( norm ‘ ( 𝑤 𝑥 ) ) )
8 7 adantll ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( 𝑥 𝐷 𝑤 ) = ( norm ‘ ( 𝑤 𝑥 ) ) )
9 8 breq1d ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( 𝑥 𝐷 𝑤 ) < 𝑧 ↔ ( norm ‘ ( 𝑤 𝑥 ) ) < 𝑧 ) )
10 ffvelrn ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑡𝑥 ) ∈ ℋ )
11 ffvelrn ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) → ( 𝑡𝑤 ) ∈ ℋ )
12 10 11 anim12dan ( ( 𝑡 : ℋ ⟶ ℋ ∧ ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑡𝑥 ) ∈ ℋ ∧ ( 𝑡𝑤 ) ∈ ℋ ) )
13 1 hilmetdval ( ( ( 𝑡𝑥 ) ∈ ℋ ∧ ( 𝑡𝑤 ) ∈ ℋ ) → ( ( 𝑡𝑥 ) 𝐷 ( 𝑡𝑤 ) ) = ( norm ‘ ( ( 𝑡𝑥 ) − ( 𝑡𝑤 ) ) ) )
14 normsub ( ( ( 𝑡𝑥 ) ∈ ℋ ∧ ( 𝑡𝑤 ) ∈ ℋ ) → ( norm ‘ ( ( 𝑡𝑥 ) − ( 𝑡𝑤 ) ) ) = ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) )
15 13 14 eqtrd ( ( ( 𝑡𝑥 ) ∈ ℋ ∧ ( 𝑡𝑤 ) ∈ ℋ ) → ( ( 𝑡𝑥 ) 𝐷 ( 𝑡𝑤 ) ) = ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) )
16 12 15 syl ( ( 𝑡 : ℋ ⟶ ℋ ∧ ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑡𝑥 ) 𝐷 ( 𝑡𝑤 ) ) = ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) )
17 16 anassrs ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( 𝑡𝑥 ) 𝐷 ( 𝑡𝑤 ) ) = ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) )
18 17 breq1d ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( ( 𝑡𝑥 ) 𝐷 ( 𝑡𝑤 ) ) < 𝑦 ↔ ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) < 𝑦 ) )
19 9 18 imbi12d ( ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( ( 𝑥 𝐷 𝑤 ) < 𝑧 → ( ( 𝑡𝑥 ) 𝐷 ( 𝑡𝑤 ) ) < 𝑦 ) ↔ ( ( norm ‘ ( 𝑤 𝑥 ) ) < 𝑧 → ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) < 𝑦 ) ) )
20 19 ralbidva ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ∀ 𝑤 ∈ ℋ ( ( 𝑥 𝐷 𝑤 ) < 𝑧 → ( ( 𝑡𝑥 ) 𝐷 ( 𝑡𝑤 ) ) < 𝑦 ) ↔ ∀ 𝑤 ∈ ℋ ( ( norm ‘ ( 𝑤 𝑥 ) ) < 𝑧 → ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) < 𝑦 ) ) )
21 20 rexbidv ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ∃ 𝑧 ∈ ℝ+𝑤 ∈ ℋ ( ( 𝑥 𝐷 𝑤 ) < 𝑧 → ( ( 𝑡𝑥 ) 𝐷 ( 𝑡𝑤 ) ) < 𝑦 ) ↔ ∃ 𝑧 ∈ ℝ+𝑤 ∈ ℋ ( ( norm ‘ ( 𝑤 𝑥 ) ) < 𝑧 → ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) < 𝑦 ) ) )
22 21 ralbidv ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ( ( 𝑥 𝐷 𝑤 ) < 𝑧 → ( ( 𝑡𝑥 ) 𝐷 ( 𝑡𝑤 ) ) < 𝑦 ) ↔ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ( ( norm ‘ ( 𝑤 𝑥 ) ) < 𝑧 → ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) < 𝑦 ) ) )
23 22 ralbidva ( 𝑡 : ℋ ⟶ ℋ → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ( ( 𝑥 𝐷 𝑤 ) < 𝑧 → ( ( 𝑡𝑥 ) 𝐷 ( 𝑡𝑤 ) ) < 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ( ( norm ‘ ( 𝑤 𝑥 ) ) < 𝑧 → ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) < 𝑦 ) ) )
24 23 pm5.32i ( ( 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ( ( 𝑥 𝐷 𝑤 ) < 𝑧 → ( ( 𝑡𝑥 ) 𝐷 ( 𝑡𝑤 ) ) < 𝑦 ) ) ↔ ( 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ( ( norm ‘ ( 𝑤 𝑥 ) ) < 𝑧 → ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) < 𝑦 ) ) )
25 1 hilxmet 𝐷 ∈ ( ∞Met ‘ ℋ )
26 2 2 metcn ( ( 𝐷 ∈ ( ∞Met ‘ ℋ ) ∧ 𝐷 ∈ ( ∞Met ‘ ℋ ) ) → ( 𝑡 ∈ ( 𝐽 Cn 𝐽 ) ↔ ( 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ( ( 𝑥 𝐷 𝑤 ) < 𝑧 → ( ( 𝑡𝑥 ) 𝐷 ( 𝑡𝑤 ) ) < 𝑦 ) ) ) )
27 25 25 26 mp2an ( 𝑡 ∈ ( 𝐽 Cn 𝐽 ) ↔ ( 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ( ( 𝑥 𝐷 𝑤 ) < 𝑧 → ( ( 𝑡𝑥 ) 𝐷 ( 𝑡𝑤 ) ) < 𝑦 ) ) )
28 ax-hilex ℋ ∈ V
29 28 28 elmap ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↔ 𝑡 : ℋ ⟶ ℋ )
30 29 anbi1i ( ( 𝑡 ∈ ( ℋ ↑m ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ( ( norm ‘ ( 𝑤 𝑥 ) ) < 𝑧 → ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) < 𝑦 ) ) ↔ ( 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ( ( norm ‘ ( 𝑤 𝑥 ) ) < 𝑧 → ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) < 𝑦 ) ) )
31 24 27 30 3bitr4i ( 𝑡 ∈ ( 𝐽 Cn 𝐽 ) ↔ ( 𝑡 ∈ ( ℋ ↑m ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ( ( norm ‘ ( 𝑤 𝑥 ) ) < 𝑧 → ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) < 𝑦 ) ) )
32 31 abbi2i ( 𝐽 Cn 𝐽 ) = { 𝑡 ∣ ( 𝑡 ∈ ( ℋ ↑m ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ( ( norm ‘ ( 𝑤 𝑥 ) ) < 𝑧 → ( norm ‘ ( ( 𝑡𝑤 ) − ( 𝑡𝑥 ) ) ) < 𝑦 ) ) }
33 3 4 32 3eqtr4i ContOp = ( 𝐽 Cn 𝐽 )