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