Theorem lnopconi

Description: A condition equivalent to " T is continuous" when T is linear. Theorem 3.5(iii) of Beran p. 99. (Contributed by NM, 7-Feb-2006) (Proof shortened by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	lnopcon.1	⊢ 𝑇 ∈ LinOp
Assertion	lnopconi	⊢ ( 𝑇 ∈ ContOp ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lnopcon.1	⊢ 𝑇 ∈ LinOp
2		nmcopex	⊢ ( ( 𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp ) → ( normop ‘ 𝑇 ) ∈ ℝ )
3	1 2	mpan	⊢ ( 𝑇 ∈ ContOp → ( normop ‘ 𝑇 ) ∈ ℝ )
4		nmcoplb	⊢ ( ( 𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) )
5	1 4	mp3an1	⊢ ( ( 𝑇 ∈ ContOp ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) )
6	1	lnopfi	⊢ 𝑇 : ℋ ⟶ ℋ
7		elcnop	⊢ ( 𝑇 ∈ ContOp ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 → ( normℎ ‘ ( ( 𝑇 ‘ 𝑤 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ) < 𝑧 ) ) )
8	6 7	mpbiran	⊢ ( 𝑇 ∈ ContOp ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 → ( normℎ ‘ ( ( 𝑇 ‘ 𝑤 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ) < 𝑧 ) )
9	6	ffvelrni	⊢ ( 𝑦 ∈ ℋ → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
10		normcl	⊢ ( ( 𝑇 ‘ 𝑦 ) ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ )
11	9 10	syl	⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ )
12	1	lnopsubi	⊢ ( ( 𝑤 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑤 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) )
13	3 5 8 11 12	lnconi	⊢ ( 𝑇 ∈ ContOp ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) )