Metamath Proof Explorer

Theorem nmopadjlei

Description: Property of the norm of an adjoint. Part of proof of Theorem 3.10 of Beran p. 104. (Contributed by NM, 22-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmopadjle.1 
|- T e. BndLinOp
Assertion nmopadjlei 
|- ( A e. ~H -> ( normh ` ( ( adjh ` T ) ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )

Proof

Step Hyp Ref Expression
1 nmopadjle.1 
 |-  T e. BndLinOp
2 bdopssadj 
 |-  BndLinOp C_ dom adjh
3 2 1 sselii 
 |-  T e. dom adjh
4 adjvalval 
 |-  ( ( T e. dom adjh /\ A e. ~H ) -> ( ( adjh ` T ) ` A ) = ( iota_ f e. ~H A. v e. ~H ( ( T ` v ) .ih A ) = ( v .ih f ) ) )
5 3 4 mpan 
 |-  ( A e. ~H -> ( ( adjh ` T ) ` A ) = ( iota_ f e. ~H A. v e. ~H ( ( T ` v ) .ih A ) = ( v .ih f ) ) )
6 oveq2 
 |-  ( z = A -> ( ( T ` v ) .ih z ) = ( ( T ` v ) .ih A ) )
7 6 eqeq1d 
 |-  ( z = A -> ( ( ( T ` v ) .ih z ) = ( v .ih f ) <-> ( ( T ` v ) .ih A ) = ( v .ih f ) ) )
8 7 ralbidv 
 |-  ( z = A -> ( A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih f ) <-> A. v e. ~H ( ( T ` v ) .ih A ) = ( v .ih f ) ) )
9 8 riotabidv 
 |-  ( z = A -> ( iota_ f e. ~H A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih f ) ) = ( iota_ f e. ~H A. v e. ~H ( ( T ` v ) .ih A ) = ( v .ih f ) ) )
10 eqid 
 |-  ( z e. ~H |-> ( iota_ f e. ~H A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih f ) ) ) = ( z e. ~H |-> ( iota_ f e. ~H A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih f ) ) )
11 riotaex 
 |-  ( iota_ f e. ~H A. v e. ~H ( ( T ` v ) .ih A ) = ( v .ih f ) ) e. _V
12 9 10 11 fvmpt 
 |-  ( A e. ~H -> ( ( z e. ~H |-> ( iota_ f e. ~H A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih f ) ) ) ` A ) = ( iota_ f e. ~H A. v e. ~H ( ( T ` v ) .ih A ) = ( v .ih f ) ) )
13 5 12 eqtr4d 
 |-  ( A e. ~H -> ( ( adjh ` T ) ` A ) = ( ( z e. ~H |-> ( iota_ f e. ~H A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih f ) ) ) ` A ) )
14 13 fveq2d 
 |-  ( A e. ~H -> ( normh ` ( ( adjh ` T ) ` A ) ) = ( normh ` ( ( z e. ~H |-> ( iota_ f e. ~H A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih f ) ) ) ` A ) ) )
15 inss1 
 |-  ( LinOp i^i ContOp ) C_ LinOp
16 lncnbd 
 |-  ( LinOp i^i ContOp ) = BndLinOp
17 1 16 eleqtrri 
 |-  T e. ( LinOp i^i ContOp )
18 15 17 sselii 
 |-  T e. LinOp
19 inss2 
 |-  ( LinOp i^i ContOp ) C_ ContOp
20 19 17 sselii 
 |-  T e. ContOp
21 eqid 
 |-  ( g e. ~H |-> ( ( T ` g ) .ih z ) ) = ( g e. ~H |-> ( ( T ` g ) .ih z ) )
22 oveq2 
 |-  ( f = w -> ( v .ih f ) = ( v .ih w ) )
23 22 eqeq2d 
 |-  ( f = w -> ( ( ( T ` v ) .ih z ) = ( v .ih f ) <-> ( ( T ` v ) .ih z ) = ( v .ih w ) ) )
24 23 ralbidv 
 |-  ( f = w -> ( A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih f ) <-> A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih w ) ) )
25 24 cbvriotavw 
 |-  ( iota_ f e. ~H A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih f ) ) = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih w ) )
26 18 20 21 25 10 cnlnadjlem7 
 |-  ( A e. ~H -> ( normh ` ( ( z e. ~H |-> ( iota_ f e. ~H A. v e. ~H ( ( T ` v ) .ih z ) = ( v .ih f ) ) ) ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
27 14 26 eqbrtrd 
 |-  ( A e. ~H -> ( normh ` ( ( adjh ` T ) ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )