This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elcnop

Description: Property defining a continuous Hilbert space operator. (Contributed by NM, 28-Jan-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	elcnop	⊢ ( 𝑇 ∈ ContOp ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑇 ‘ 𝑤 ) −_ℎ ( 𝑇 ‘ 𝑥 ) ) ) < 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq1	⊢ ( 𝑡 = 𝑇 → ( 𝑡 ‘ 𝑤 ) = ( 𝑇 ‘ 𝑤 ) )
2		fveq1	⊢ ( 𝑡 = 𝑇 → ( 𝑡 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
3	1 2	oveq12d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑤 ) −_ℎ ( 𝑇 ‘ 𝑥 ) ) )
4	3	fveq2d	⊢ ( 𝑡 = 𝑇 → ( norm_ℎ ‘ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) ) = ( norm_ℎ ‘ ( ( 𝑇 ‘ 𝑤 ) −_ℎ ( 𝑇 ‘ 𝑥 ) ) ) )
5	4	breq1d	⊢ ( 𝑡 = 𝑇 → ( ( norm_ℎ ‘ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ↔ ( norm_ℎ ‘ ( ( 𝑇 ‘ 𝑤 ) −_ℎ ( 𝑇 ‘ 𝑥 ) ) ) < 𝑦 ) )
6	5	imbi2d	⊢ ( 𝑡 = 𝑇 → ( ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) ↔ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑇 ‘ 𝑤 ) −_ℎ ( 𝑇 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
7	6	rexralbidv	⊢ ( 𝑡 = 𝑇 → ( ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) ↔ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑇 ‘ 𝑤 ) −_ℎ ( 𝑇 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
8	7	2ralbidv	⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑇 ‘ 𝑤 ) −_ℎ ( 𝑇 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
9		df-cnop	⊢ ContOp = { 𝑡 ∈ ( ℋ ↑_m ℋ ) ∣ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) }
10	8 9	elrab2	⊢ ( 𝑇 ∈ ContOp ↔ ( 𝑇 ∈ ( ℋ ↑_m ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑇 ‘ 𝑤 ) −_ℎ ( 𝑇 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
11		ax-hilex	⊢ ℋ ∈ V
12	11 11	elmap	⊢ ( 𝑇 ∈ ( ℋ ↑_m ℋ ) ↔ 𝑇 : ℋ ⟶ ℋ )
13	12	anbi1i	⊢ ( ( 𝑇 ∈ ( ℋ ↑_m ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑇 ‘ 𝑤 ) −_ℎ ( 𝑇 ‘ 𝑥 ) ) ) < 𝑦 ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑇 ‘ 𝑤 ) −_ℎ ( 𝑇 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
14	10 13	bitri	⊢ ( 𝑇 ∈ ContOp ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑇 ‘ 𝑤 ) −_ℎ ( 𝑇 ‘ 𝑥 ) ) ) < 𝑦 ) ) )