Metamath Proof Explorer

Theorem lnopcnbd

Description: A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion lnopcnbd ⊢ T ∈ LinOp → T ∈ ContOp ↔ T ∈ BndLinOp

Proof

Step Hyp Ref Expression
1 nmcopex ⊢ T ∈ LinOp ∧ T ∈ ContOp → norm op ⁡ T ∈ ℝ
2 1 ex ⊢ T ∈ LinOp → T ∈ ContOp → norm op ⁡ T ∈ ℝ
3 elbdop2 ⊢ T ∈ BndLinOp ↔ T ∈ LinOp ∧ norm op ⁡ T ∈ ℝ
4 3 baibr ⊢ T ∈ LinOp → norm op ⁡ T ∈ ℝ ↔ T ∈ BndLinOp
5 2 4 sylibd ⊢ T ∈ LinOp → T ∈ ContOp → T ∈ BndLinOp
6 nmopre ⊢ T ∈ BndLinOp → norm op ⁡ T ∈ ℝ
7 nmbdoplb ⊢ T ∈ BndLinOp ∧ y ∈ ℋ → norm ℎ ⁡ T ⁡ y ≤ norm op ⁡ T ⁢ norm ℎ ⁡ y
8 7 ralrimiva ⊢ T ∈ BndLinOp → ∀ y ∈ ℋ norm ℎ ⁡ T ⁡ y ≤ norm op ⁡ T ⁢ norm ℎ ⁡ y
9 oveq1 ⊢ x = norm op ⁡ T → x ⁢ norm ℎ ⁡ y = norm op ⁡ T ⁢ norm ℎ ⁡ y
10 9 breq2d ⊢ x = norm op ⁡ T → norm ℎ ⁡ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y ↔ norm ℎ ⁡ T ⁡ y ≤ norm op ⁡ T ⁢ norm ℎ ⁡ y
11 10 ralbidv ⊢ x = norm op ⁡ T → ∀ y ∈ ℋ norm ℎ ⁡ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y ↔ ∀ y ∈ ℋ norm ℎ ⁡ T ⁡ y ≤ norm op ⁡ T ⁢ norm ℎ ⁡ y
12 11 rspcev ⊢ norm op ⁡ T ∈ ℝ ∧ ∀ y ∈ ℋ norm ℎ ⁡ T ⁡ y ≤ norm op ⁡ T ⁢ norm ℎ ⁡ y → ∃ x ∈ ℝ ∀ y ∈ ℋ norm ℎ ⁡ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y
13 6 8 12 syl2anc ⊢ T ∈ BndLinOp → ∃ x ∈ ℝ ∀ y ∈ ℋ norm ℎ ⁡ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y
14 lnopcon ⊢ T ∈ LinOp → T ∈ ContOp ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ norm ℎ ⁡ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y
15 13 14 imbitrrid ⊢ T ∈ LinOp → T ∈ BndLinOp → T ∈ ContOp
16 5 15 impbid ⊢ T ∈ LinOp → T ∈ ContOp ↔ T ∈ BndLinOp