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

Metamath Proof Explorer

Theorem elcnfn

Description: Property defining a continuous functional. (Contributed by NM, 11-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

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

Proof

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