df-cnop

Description: Define the set of continuous operators on Hilbert space. For every "epsilon" ( y ) there is a "delta" ( z ) such that... (Contributed by NM, 28-Jan-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-cnop	⊢ ContOp = { 𝑡 ∈ ( ℋ ↑_m ℋ ) ∣ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccop	⊢ ContOp
1		vt	⊢ 𝑡
2		chba	⊢ ℋ
3		cmap	⊢ ↑_m
4	2 2 3	co	⊢ ( ℋ ↑_m ℋ )
5		vx	⊢ 𝑥
6		vy	⊢ 𝑦
7		crp	⊢ ℝ⁺
8		vz	⊢ 𝑧
9		vw	⊢ 𝑤
10		cno	⊢ norm_ℎ
11	9	cv	⊢ 𝑤
12		cmv	⊢ −_ℎ
13	5	cv	⊢ 𝑥
14	11 13 12	co	⊢ ( 𝑤 −_ℎ 𝑥 )
15	14 10	cfv	⊢ ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) )
16		clt	⊢ <
17	8	cv	⊢ 𝑧
18	15 17 16	wbr	⊢ ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧
19	1	cv	⊢ 𝑡
20	11 19	cfv	⊢ ( 𝑡 ‘ 𝑤 )
21	13 19	cfv	⊢ ( 𝑡 ‘ 𝑥 )
22	20 21 12	co	⊢ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) )
23	22 10	cfv	⊢ ( norm_ℎ ‘ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) )
24	6	cv	⊢ 𝑦
25	23 24 16	wbr	⊢ ( norm_ℎ ‘ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦
26	18 25	wi	⊢ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 )
27	26 9 2	wral	⊢ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 )
28	27 8 7	wrex	⊢ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 )
29	28 6 7	wral	⊢ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 )
30	29 5 2	wral	⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 )
31	30 1 4	crab	⊢ { 𝑡 ∈ ( ℋ ↑_m ℋ ) ∣ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) }
32	0 31	wceq	⊢ ContOp = { 𝑡 ∈ ( ℋ ↑_m ℋ ) ∣ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( norm_ℎ ‘ ( ( 𝑡 ‘ 𝑤 ) −_ℎ ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) }

Metamath Proof Explorer

Definition df-cnop

Detailed syntax breakdown