This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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ℎ ‘ 𝑦 ) ) ) )