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	|- T e. LinOp
Assertion	lnopconi	|- ( T e. ContOp <-> E. x e. RR A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )

Proof

Step	Hyp	Ref	Expression
1		lnopcon.1	|- T e. LinOp
2		nmcopex	|- ( ( T e. LinOp /\ T e. ContOp ) -> ( normop ` T ) e. RR )
3	1 2	mpan	|- ( T e. ContOp -> ( normop ` T ) e. RR )
4		nmcoplb	|- ( ( T e. LinOp /\ T e. ContOp /\ y e. ~H ) -> ( normh ` ( T ` y ) ) <_ ( ( normop ` T ) x. ( normh ` y ) ) )
5	1 4	mp3an1	|- ( ( T e. ContOp /\ y e. ~H ) -> ( normh ` ( T ` y ) ) <_ ( ( normop ` T ) x. ( normh ` y ) ) )
6	1	lnopfi	|- T : ~H --> ~H
7		elcnop	|- ( T e. ContOp <-> ( T : ~H --> ~H /\ A. x e. ~H A. z e. RR+ E. y e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < y -> ( normh ` ( ( T ` w ) -h ( T ` x ) ) ) < z ) ) )
8	6 7	mpbiran	|- ( T e. ContOp <-> A. x e. ~H A. z e. RR+ E. y e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < y -> ( normh ` ( ( T ` w ) -h ( T ` x ) ) ) < z ) )
9	6	ffvelrni	|- ( y e. ~H -> ( T ` y ) e. ~H )
10		normcl	|- ( ( T ` y ) e. ~H -> ( normh ` ( T ` y ) ) e. RR )
11	9 10	syl	|- ( y e. ~H -> ( normh ` ( T ` y ) ) e. RR )
12	1	lnopsubi	|- ( ( w e. ~H /\ x e. ~H ) -> ( T ` ( w -h x ) ) = ( ( T ` w ) -h ( T ` x ) ) )
13	3 5 8 11 12	lnconi	|- ( T e. ContOp <-> E. x e. RR A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )