Metamath Proof Explorer

Theorem lnopcon

Description: A condition equivalent to " T is continuous" when T is linear. Theorem 3.5(iii) of Beran p. 99. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion lnopcon ⊢ T ∈ LinOp → T ∈ ContOp ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ norm ℎ ⁡ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ T = if T ∈ LinOp T I ↾ ℋ → T ∈ ContOp ↔ if T ∈ LinOp T I ↾ ℋ ∈ ContOp
2 fveq1 ⊢ T = if T ∈ LinOp T I ↾ ℋ → T ⁡ y = if T ∈ LinOp T I ↾ ℋ ⁡ y
3 2 fveq2d ⊢ T = if T ∈ LinOp T I ↾ ℋ → norm ℎ ⁡ T ⁡ y = norm ℎ ⁡ if T ∈ LinOp T I ↾ ℋ ⁡ y
4 3 breq1d ⊢ T = if T ∈ LinOp T I ↾ ℋ → norm ℎ ⁡ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y ↔ norm ℎ ⁡ if T ∈ LinOp T I ↾ ℋ ⁡ y ≤ x ⁢ norm ℎ ⁡ y
5 4 rexralbidv ⊢ T = if T ∈ LinOp T I ↾ ℋ → ∃ x ∈ ℝ ∀ y ∈ ℋ norm ℎ ⁡ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ norm ℎ ⁡ if T ∈ LinOp T I ↾ ℋ ⁡ y ≤ x ⁢ norm ℎ ⁡ y
6 1 5 bibi12d ⊢ T = if T ∈ LinOp T I ↾ ℋ → T ∈ ContOp ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ norm ℎ ⁡ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y ↔ if T ∈ LinOp T I ↾ ℋ ∈ ContOp ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ norm ℎ ⁡ if T ∈ LinOp T I ↾ ℋ ⁡ y ≤ x ⁢ norm ℎ ⁡ y
7 idlnop ⊢ I ↾ ℋ ∈ LinOp
8 7 elimel ⊢ if T ∈ LinOp T I ↾ ℋ ∈ LinOp
9 8 lnopconi ⊢ if T ∈ LinOp T I ↾ ℋ ∈ ContOp ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ norm ℎ ⁡ if T ∈ LinOp T I ↾ ℋ ⁡ y ≤ x ⁢ norm ℎ ⁡ y
10 6 9 dedth ⊢ T ∈ LinOp → T ∈ ContOp ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ norm ℎ ⁡ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y