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=ifT∈LinOpTI↾ℋ→T∈ContOp↔ifT∈LinOpTI↾ℋ∈ContOp
2 fveq1 ⊢T=ifT∈LinOpTI↾ℋ→T⁡y=ifT∈LinOpTI↾ℋ⁡y
3 2 fveq2d ⊢T=ifT∈LinOpTI↾ℋ→normℎ⁡T⁡y=normℎ⁡ifT∈LinOpTI↾ℋ⁡y
4 3 breq1d ⊢T=ifT∈LinOpTI↾ℋ→normℎ⁡T⁡y≤x⁢normℎ⁡y↔normℎ⁡ifT∈LinOpTI↾ℋ⁡y≤x⁢normℎ⁡y
5 4 rexralbidv ⊢T=ifT∈LinOpTI↾ℋ→∃x∈ℝ∀y∈ℋnormℎ⁡T⁡y≤x⁢normℎ⁡y↔∃x∈ℝ∀y∈ℋnormℎ⁡ifT∈LinOpTI↾ℋ⁡y≤x⁢normℎ⁡y
6 1 5 bibi12d ⊢T=ifT∈LinOpTI↾ℋ→T∈ContOp↔∃x∈ℝ∀y∈ℋnormℎ⁡T⁡y≤x⁢normℎ⁡y↔ifT∈LinOpTI↾ℋ∈ContOp↔∃x∈ℝ∀y∈ℋnormℎ⁡ifT∈LinOpTI↾ℋ⁡y≤x⁢normℎ⁡y
7 idlnop ⊢I↾ℋ∈LinOp
8 7 elimel ⊢ifT∈LinOpTI↾ℋ∈LinOp
9 8 lnopconi ⊢ifT∈LinOpTI↾ℋ∈ContOp↔∃x∈ℝ∀y∈ℋnormℎ⁡ifT∈LinOpTI↾ℋ⁡y≤x⁢normℎ⁡y
10 6 9 dedth ⊢T∈LinOp→T∈ContOp↔∃x∈ℝ∀y∈ℋnormℎ⁡T⁡y≤x⁢normℎ⁡y