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