Metamath Proof Explorer

Theorem lnophm

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
Assertion lnophm 
|- ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) -> T e. HrmOp )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( T = if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) -> ( T e. HrmOp <-> if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) e. HrmOp ) )
2 eleq1 
 |-  ( T = if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) -> ( T e. LinOp <-> if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) e. LinOp ) )
3 id 
 |-  ( x = y -> x = y )
4 fveq2 
 |-  ( x = y -> ( T ` x ) = ( T ` y ) )
5 3 4 oveq12d 
 |-  ( x = y -> ( x .ih ( T ` x ) ) = ( y .ih ( T ` y ) ) )
6 5 eleq1d 
 |-  ( x = y -> ( ( x .ih ( T ` x ) ) e. RR <-> ( y .ih ( T ` y ) ) e. RR ) )
7 6 cbvralvw 
 |-  ( A. x e. ~H ( x .ih ( T ` x ) ) e. RR <-> A. y e. ~H ( y .ih ( T ` y ) ) e. RR )
8 fveq1 
 |-  ( T = if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) -> ( T ` y ) = ( if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) ` y ) )
9 8 oveq2d 
 |-  ( T = if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) -> ( y .ih ( T ` y ) ) = ( y .ih ( if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) ` y ) ) )
10 9 eleq1d 
 |-  ( T = if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) -> ( ( y .ih ( T ` y ) ) e. RR <-> ( y .ih ( if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) ` y ) ) e. RR ) )
11 10 ralbidv 
 |-  ( T = if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) -> ( A. y e. ~H ( y .ih ( T ` y ) ) e. RR <-> A. y e. ~H ( y .ih ( if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) ` y ) ) e. RR ) )
12 7 11 syl5bb 
 |-  ( T = if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) -> ( A. x e. ~H ( x .ih ( T ` x ) ) e. RR <-> A. y e. ~H ( y .ih ( if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) ` y ) ) e. RR ) )
13 2 12 anbi12d 
 |-  ( T = if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) -> ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) <-> ( if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) e. LinOp /\ A. y e. ~H ( y .ih ( if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) ` y ) ) e. RR ) ) )
14 eleq1 
 |-  ( ( _I |` ~H ) = if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) -> ( ( _I |` ~H ) e. LinOp <-> if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) e. LinOp ) )
15 fveq1 
 |-  ( ( _I |` ~H ) = if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) -> ( ( _I |` ~H ) ` y ) = ( if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) ` y ) )
16 15 oveq2d 
 |-  ( ( _I |` ~H ) = if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) -> ( y .ih ( ( _I |` ~H ) ` y ) ) = ( y .ih ( if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) ` y ) ) )
17 16 eleq1d 
 |-  ( ( _I |` ~H ) = if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) -> ( ( y .ih ( ( _I |` ~H ) ` y ) ) e. RR <-> ( y .ih ( if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) ` y ) ) e. RR ) )
18 17 ralbidv 
 |-  ( ( _I |` ~H ) = if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) -> ( A. y e. ~H ( y .ih ( ( _I |` ~H ) ` y ) ) e. RR <-> A. y e. ~H ( y .ih ( if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) ` y ) ) e. RR ) )
19 14 18 anbi12d 
 |-  ( ( _I |` ~H ) = if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) -> ( ( ( _I |` ~H ) e. LinOp /\ A. y e. ~H ( y .ih ( ( _I |` ~H ) ` y ) ) e. RR ) <-> ( if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) e. LinOp /\ A. y e. ~H ( y .ih ( if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) ` y ) ) e. RR ) ) )
20 idlnop 
 |-  ( _I |` ~H ) e. LinOp
21 fvresi 
 |-  ( y e. ~H -> ( ( _I |` ~H ) ` y ) = y )
22 21 oveq2d 
 |-  ( y e. ~H -> ( y .ih ( ( _I |` ~H ) ` y ) ) = ( y .ih y ) )
23 hiidrcl 
 |-  ( y e. ~H -> ( y .ih y ) e. RR )
24 22 23 eqeltrd 
 |-  ( y e. ~H -> ( y .ih ( ( _I |` ~H ) ` y ) ) e. RR )
25 24 rgen 
 |-  A. y e. ~H ( y .ih ( ( _I |` ~H ) ` y ) ) e. RR
26 20 25 pm3.2i 
 |-  ( ( _I |` ~H ) e. LinOp /\ A. y e. ~H ( y .ih ( ( _I |` ~H ) ` y ) ) e. RR )
27 13 19 26 elimhyp 
 |-  ( if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) e. LinOp /\ A. y e. ~H ( y .ih ( if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) ` y ) ) e. RR )
28 27 simpli 
 |-  if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) e. LinOp
29 27 simpri 
 |-  A. y e. ~H ( y .ih ( if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) ` y ) ) e. RR
30 28 29 lnophmi 
 |-  if ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) , T , ( _I |` ~H ) ) e. HrmOp
31 1 30 dedth 
 |-  ( ( T e. LinOp /\ A. x e. ~H ( x .ih ( T ` x ) ) e. RR ) -> T e. HrmOp )