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		ffvelcdm	⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑡 ‘ 𝑥 ) ∈ ℋ )
11		ffvelcdm	⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) → ( 𝑡 ‘ 𝑤 ) ∈ ℋ )
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	eqabi	⊢ ( 𝐽 Cn 𝐽 ) = { 𝑡 ∣ ( 𝑡 ∈ ( ℋ ↑_m ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) ) }
33	3 4 32	3eqtr4i	⊢ ContOp = ( 𝐽 Cn 𝐽 )

Metamath Proof Explorer

Theorem hhcno

Proof