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 ⊢T∈ContOp↔T:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡T⁡w-ℎT⁡x<y

Proof

Step Hyp Ref Expression
1 fveq1 ⊢t=T→t⁡w=T⁡w
2 fveq1 ⊢t=T→t⁡x=T⁡x
3 1 2 oveq12d ⊢t=T→t⁡w-ℎt⁡x=T⁡w-ℎT⁡x
4 3 fveq2d ⊢t=T→normℎ⁡t⁡w-ℎt⁡x=normℎ⁡T⁡w-ℎT⁡x
5 4 breq1d ⊢t=T→normℎ⁡t⁡w-ℎt⁡x<y↔normℎ⁡T⁡w-ℎT⁡x<y
6 5 imbi2d ⊢t=T→normℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y↔normℎ⁡w-ℎx<z→normℎ⁡T⁡w-ℎT⁡x<y
7 6 rexralbidv ⊢t=T→∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y↔∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡T⁡w-ℎT⁡x<y
8 7 2ralbidv ⊢t=T→∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y↔∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡T⁡w-ℎT⁡x<y
9 df-cnop ⊢ContOp=t∈ℋℋ|∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y
10 8 9 elrab2 ⊢T∈ContOp↔T∈ℋℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡T⁡w-ℎT⁡x<y
11 ax-hilex ⊢ℋ∈V
12 11 11 elmap ⊢T∈ℋℋ↔T:ℋ⟶ℋ
13 12 anbi1i ⊢T∈ℋℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡T⁡w-ℎT⁡x<y↔T:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡T⁡w-ℎT⁡x<y
14 10 13 bitri ⊢T∈ContOp↔T:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡T⁡w-ℎT⁡x<y