Metamath Proof Explorer

Theorem lnophmi

Description: A linear operator is Hermitian if x .ih ( Tx ) takes only real values. Remark in ReedSimon p. 195. (Contributed by NM, 24-Jan-2006) (New usage is discouraged.)

Ref Expression
Hypotheses lnophm.1 
|- T e. LinOp
lnophm.2 
|- A. x e. ~H ( x .ih ( T ` x ) ) e. RR
Assertion lnophmi 
|- T e. HrmOp

Proof

Step Hyp Ref Expression
1 lnophm.1 
 |-  T e. LinOp
2 lnophm.2 
 |-  A. x e. ~H ( x .ih ( T ` x ) ) e. RR
3 1 lnopfi 
 |-  T : ~H --> ~H
4 oveq1 
 |-  ( y = if ( y e. ~H , y , 0h ) -> ( y .ih ( T ` z ) ) = ( if ( y e. ~H , y , 0h ) .ih ( T ` z ) ) )
5 fveq2 
 |-  ( y = if ( y e. ~H , y , 0h ) -> ( T ` y ) = ( T ` if ( y e. ~H , y , 0h ) ) )
6 5 oveq1d 
 |-  ( y = if ( y e. ~H , y , 0h ) -> ( ( T ` y ) .ih z ) = ( ( T ` if ( y e. ~H , y , 0h ) ) .ih z ) )
7 4 6 eqeq12d 
 |-  ( y = if ( y e. ~H , y , 0h ) -> ( ( y .ih ( T ` z ) ) = ( ( T ` y ) .ih z ) <-> ( if ( y e. ~H , y , 0h ) .ih ( T ` z ) ) = ( ( T ` if ( y e. ~H , y , 0h ) ) .ih z ) ) )
8 fveq2 
 |-  ( z = if ( z e. ~H , z , 0h ) -> ( T ` z ) = ( T ` if ( z e. ~H , z , 0h ) ) )
9 8 oveq2d 
 |-  ( z = if ( z e. ~H , z , 0h ) -> ( if ( y e. ~H , y , 0h ) .ih ( T ` z ) ) = ( if ( y e. ~H , y , 0h ) .ih ( T ` if ( z e. ~H , z , 0h ) ) ) )
10 oveq2 
 |-  ( z = if ( z e. ~H , z , 0h ) -> ( ( T ` if ( y e. ~H , y , 0h ) ) .ih z ) = ( ( T ` if ( y e. ~H , y , 0h ) ) .ih if ( z e. ~H , z , 0h ) ) )
11 9 10 eqeq12d 
 |-  ( z = if ( z e. ~H , z , 0h ) -> ( ( if ( y e. ~H , y , 0h ) .ih ( T ` z ) ) = ( ( T ` if ( y e. ~H , y , 0h ) ) .ih z ) <-> ( if ( y e. ~H , y , 0h ) .ih ( T ` if ( z e. ~H , z , 0h ) ) ) = ( ( T ` if ( y e. ~H , y , 0h ) ) .ih if ( z e. ~H , z , 0h ) ) ) )
12 ifhvhv0 
 |-  if ( y e. ~H , y , 0h ) e. ~H
13 ifhvhv0 
 |-  if ( z e. ~H , z , 0h ) e. ~H
14 12 13 1 2 lnophmlem2 
 |-  ( if ( y e. ~H , y , 0h ) .ih ( T ` if ( z e. ~H , z , 0h ) ) ) = ( ( T ` if ( y e. ~H , y , 0h ) ) .ih if ( z e. ~H , z , 0h ) )
15 7 11 14 dedth2h 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( y .ih ( T ` z ) ) = ( ( T ` y ) .ih z ) )
16 15 rgen2 
 |-  A. y e. ~H A. z e. ~H ( y .ih ( T ` z ) ) = ( ( T ` y ) .ih z )
17 elhmop 
 |-  ( T e. HrmOp <-> ( T : ~H --> ~H /\ A. y e. ~H A. z e. ~H ( y .ih ( T ` z ) ) = ( ( T ` y ) .ih z ) ) )
18 3 16 17 mpbir2an 
 |-  T e. HrmOp