Metamath Proof Explorer

Theorem lnopeqi

Description: Two linear Hilbert space operators are equal iff their quadratic forms are equal. (Contributed by NM, 27-Jul-2006) (New usage is discouraged.)

Ref Expression
Hypotheses lnopeq.1 
|- T e. LinOp
lnopeq.2 
|- U e. LinOp
Assertion lnopeqi 
|- ( A. x e. ~H ( ( T ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> T = U )

Proof

Step Hyp Ref Expression
1 lnopeq.1 
 |-  T e. LinOp
2 lnopeq.2 
 |-  U e. LinOp
3 1 lnopfi 
 |-  T : ~H --> ~H
4 3 ffvelcdmi 
 |-  ( x e. ~H -> ( T ` x ) e. ~H )
5 hicl 
 |-  ( ( ( T ` x ) e. ~H /\ x e. ~H ) -> ( ( T ` x ) .ih x ) e. CC )
6 4 5 mpancom 
 |-  ( x e. ~H -> ( ( T ` x ) .ih x ) e. CC )
7 2 lnopfi 
 |-  U : ~H --> ~H
8 7 ffvelcdmi 
 |-  ( x e. ~H -> ( U ` x ) e. ~H )
9 hicl 
 |-  ( ( ( U ` x ) e. ~H /\ x e. ~H ) -> ( ( U ` x ) .ih x ) e. CC )
10 8 9 mpancom 
 |-  ( x e. ~H -> ( ( U ` x ) .ih x ) e. CC )
11 6 10 subeq0ad 
 |-  ( x e. ~H -> ( ( ( ( T ` x ) .ih x ) - ( ( U ` x ) .ih x ) ) = 0 <-> ( ( T ` x ) .ih x ) = ( ( U ` x ) .ih x ) ) )
12 hodval 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H /\ x e. ~H ) -> ( ( T -op U ) ` x ) = ( ( T ` x ) -h ( U ` x ) ) )
13 3 7 12 mp3an12 
 |-  ( x e. ~H -> ( ( T -op U ) ` x ) = ( ( T ` x ) -h ( U ` x ) ) )
14 13 oveq1d 
 |-  ( x e. ~H -> ( ( ( T -op U ) ` x ) .ih x ) = ( ( ( T ` x ) -h ( U ` x ) ) .ih x ) )
15 id 
 |-  ( x e. ~H -> x e. ~H )
16 his2sub 
 |-  ( ( ( T ` x ) e. ~H /\ ( U ` x ) e. ~H /\ x e. ~H ) -> ( ( ( T ` x ) -h ( U ` x ) ) .ih x ) = ( ( ( T ` x ) .ih x ) - ( ( U ` x ) .ih x ) ) )
17 4 8 15 16 syl3anc 
 |-  ( x e. ~H -> ( ( ( T ` x ) -h ( U ` x ) ) .ih x ) = ( ( ( T ` x ) .ih x ) - ( ( U ` x ) .ih x ) ) )
18 14 17 eqtr2d 
 |-  ( x e. ~H -> ( ( ( T ` x ) .ih x ) - ( ( U ` x ) .ih x ) ) = ( ( ( T -op U ) ` x ) .ih x ) )
19 18 eqeq1d 
 |-  ( x e. ~H -> ( ( ( ( T ` x ) .ih x ) - ( ( U ` x ) .ih x ) ) = 0 <-> ( ( ( T -op U ) ` x ) .ih x ) = 0 ) )
20 11 19 bitr3d 
 |-  ( x e. ~H -> ( ( ( T ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> ( ( ( T -op U ) ` x ) .ih x ) = 0 ) )
21 20 ralbiia 
 |-  ( A. x e. ~H ( ( T ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> A. x e. ~H ( ( ( T -op U ) ` x ) .ih x ) = 0 )
22 1 2 lnophdi 
 |-  ( T -op U ) e. LinOp
23 22 lnopeq0i 
 |-  ( A. x e. ~H ( ( ( T -op U ) ` x ) .ih x ) = 0 <-> ( T -op U ) = 0hop )
24 3 7 hosubeq0i 
 |-  ( ( T -op U ) = 0hop <-> T = U )
25 21 23 24 3bitri 
 |-  ( A. x e. ~H ( ( T ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> T = U )