# 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 ( 𝑇 ∈ LinOp → ( 𝑇 ∈ ContOp ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( norm ‘ ( 𝑇𝑦 ) ) ≤ ( 𝑥 · ( norm𝑦 ) ) ) )

### Proof

Step Hyp Ref Expression
1 eleq1 ( 𝑇 = if ( 𝑇 ∈ LinOp , 𝑇 , ( I ↾ ℋ ) ) → ( 𝑇 ∈ ContOp ↔ if ( 𝑇 ∈ LinOp , 𝑇 , ( I ↾ ℋ ) ) ∈ ContOp ) )
2 fveq1 ( 𝑇 = if ( 𝑇 ∈ LinOp , 𝑇 , ( I ↾ ℋ ) ) → ( 𝑇𝑦 ) = ( if ( 𝑇 ∈ LinOp , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) )
3 2 fveq2d ( 𝑇 = if ( 𝑇 ∈ LinOp , 𝑇 , ( I ↾ ℋ ) ) → ( norm ‘ ( 𝑇𝑦 ) ) = ( norm ‘ ( if ( 𝑇 ∈ LinOp , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) )
4 3 breq1d ( 𝑇 = if ( 𝑇 ∈ LinOp , 𝑇 , ( I ↾ ℋ ) ) → ( ( norm ‘ ( 𝑇𝑦 ) ) ≤ ( 𝑥 · ( norm𝑦 ) ) ↔ ( norm ‘ ( if ( 𝑇 ∈ LinOp , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) ≤ ( 𝑥 · ( norm𝑦 ) ) ) )
5 4 rexralbidv ( 𝑇 = if ( 𝑇 ∈ LinOp , 𝑇 , ( I ↾ ℋ ) ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( norm ‘ ( 𝑇𝑦 ) ) ≤ ( 𝑥 · ( norm𝑦 ) ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( norm ‘ ( if ( 𝑇 ∈ LinOp , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) ≤ ( 𝑥 · ( norm𝑦 ) ) ) )
6 1 5 bibi12d ( 𝑇 = if ( 𝑇 ∈ LinOp , 𝑇 , ( I ↾ ℋ ) ) → ( ( 𝑇 ∈ ContOp ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( norm ‘ ( 𝑇𝑦 ) ) ≤ ( 𝑥 · ( norm𝑦 ) ) ) ↔ ( if ( 𝑇 ∈ LinOp , 𝑇 , ( I ↾ ℋ ) ) ∈ ContOp ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( norm ‘ ( if ( 𝑇 ∈ LinOp , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) ≤ ( 𝑥 · ( norm𝑦 ) ) ) ) )
7 idlnop ( I ↾ ℋ ) ∈ LinOp
8 7 elimel if ( 𝑇 ∈ LinOp , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp
9 8 lnopconi ( if ( 𝑇 ∈ LinOp , 𝑇 , ( I ↾ ℋ ) ) ∈ ContOp ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( norm ‘ ( if ( 𝑇 ∈ LinOp , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) ≤ ( 𝑥 · ( norm𝑦 ) ) )
10 6 9 dedth ( 𝑇 ∈ LinOp → ( 𝑇 ∈ ContOp ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( norm ‘ ( 𝑇𝑦 ) ) ≤ ( 𝑥 · ( norm𝑦 ) ) ) )