Metamath Proof Explorer

Theorem cnlnadjlem8

Description: Lemma for cnlnadji . F is continuous. (Contributed by NM, 17-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses cnlnadjlem.1 
|- T e. LinOp
cnlnadjlem.2 
|- T e. ContOp
cnlnadjlem.3 
|- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )
cnlnadjlem.4 
|- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
cnlnadjlem.5 
|- F = ( y e. ~H |-> B )
Assertion cnlnadjlem8 
|- F e. ContOp

Proof

Step Hyp Ref Expression
1 cnlnadjlem.1 
 |-  T e. LinOp
2 cnlnadjlem.2 
 |-  T e. ContOp
3 cnlnadjlem.3 
 |-  G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )
4 cnlnadjlem.4 
 |-  B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
5 cnlnadjlem.5 
 |-  F = ( y e. ~H |-> B )
6 1 2 nmcopexi 
 |-  ( normop ` T ) e. RR
7 1 2 3 4 5 cnlnadjlem7 
 |-  ( z e. ~H -> ( normh ` ( F ` z ) ) <_ ( ( normop ` T ) x. ( normh ` z ) ) )
8 7 rgen 
 |-  A. z e. ~H ( normh ` ( F ` z ) ) <_ ( ( normop ` T ) x. ( normh ` z ) )
9 oveq1 
 |-  ( x = ( normop ` T ) -> ( x x. ( normh ` z ) ) = ( ( normop ` T ) x. ( normh ` z ) ) )
10 9 breq2d 
 |-  ( x = ( normop ` T ) -> ( ( normh ` ( F ` z ) ) <_ ( x x. ( normh ` z ) ) <-> ( normh ` ( F ` z ) ) <_ ( ( normop ` T ) x. ( normh ` z ) ) ) )
11 10 ralbidv 
 |-  ( x = ( normop ` T ) -> ( A. z e. ~H ( normh ` ( F ` z ) ) <_ ( x x. ( normh ` z ) ) <-> A. z e. ~H ( normh ` ( F ` z ) ) <_ ( ( normop ` T ) x. ( normh ` z ) ) ) )
12 11 rspcev 
 |-  ( ( ( normop ` T ) e. RR /\ A. z e. ~H ( normh ` ( F ` z ) ) <_ ( ( normop ` T ) x. ( normh ` z ) ) ) -> E. x e. RR A. z e. ~H ( normh ` ( F ` z ) ) <_ ( x x. ( normh ` z ) ) )
13 6 8 12 mp2an 
 |-  E. x e. RR A. z e. ~H ( normh ` ( F ` z ) ) <_ ( x x. ( normh ` z ) )
14 1 2 3 4 5 cnlnadjlem6 
 |-  F e. LinOp
15 14 lnopconi 
 |-  ( F e. ContOp <-> E. x e. RR A. z e. ~H ( normh ` ( F ` z ) ) <_ ( x x. ( normh ` z ) ) )
16 13 15 mpbir 
 |-  F e. ContOp