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

Metamath Proof Explorer

Theorem lnfncon

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

Ref Expression
Assertion lnfncon ( 𝑇 ∈ LinFn → ( 𝑇 ∈ ContFn ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( 𝑇 ∈ ContFn ↔ if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ∈ ContFn ) )
2 fveq1 ⊢ ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( 𝑇 ‘ 𝑦 ) = ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑦 ) )
3 2 fveq2d ⊢ ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) = ( abs ‘ ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑦 ) ) )
4 3 breq1d ⊢ ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ↔ ( abs ‘ ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ) )
5 4 rexralbidv ⊢ ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( abs ‘ ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ) )
6 1 5 bibi12d ⊢ ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( ( 𝑇 ∈ ContFn ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ) ↔ ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ∈ ContFn ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( abs ‘ ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ) ) )
7 0lnfn ⊢ ( ℋ × { 0 } ) ∈ LinFn
8 7 elimel ⊢ if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn
9 8 lnfnconi ⊢ ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ∈ ContFn ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( abs ‘ ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) )
10 6 9 dedth ⊢ ( 𝑇 ∈ LinFn → ( 𝑇 ∈ ContFn ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ) )