# Metamath Proof Explorer

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

Ref Expression
`|- T e. LinOp`
`|- T e. ContOp`
`|- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )`
`|- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )`
`|- F = ( y e. ~H |-> B )`
`|- F e. ContOp`

### Proof

Step Hyp Ref Expression
` |-  T e. LinOp`
` |-  T e. ContOp`
` |-  G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )`
` |-  B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )`
` |-  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`