This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lnopeq

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
Assertion lnopeq 
|- ( ( T e. LinOp /\ U e. LinOp ) -> ( A. x e. ~H ( ( T ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> T = U ) )

Proof

Step Hyp Ref Expression
1 fveq1 
 |-  ( T = if ( T e. LinOp , T , 0hop ) -> ( T ` x ) = ( if ( T e. LinOp , T , 0hop ) ` x ) )
2 1 oveq1d 
 |-  ( T = if ( T e. LinOp , T , 0hop ) -> ( ( T ` x ) .ih x ) = ( ( if ( T e. LinOp , T , 0hop ) ` x ) .ih x ) )
3 2 eqeq1d 
 |-  ( T = if ( T e. LinOp , T , 0hop ) -> ( ( ( T ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> ( ( if ( T e. LinOp , T , 0hop ) ` x ) .ih x ) = ( ( U ` x ) .ih x ) ) )
4 3 ralbidv 
 |-  ( T = if ( T e. LinOp , T , 0hop ) -> ( A. x e. ~H ( ( T ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> A. x e. ~H ( ( if ( T e. LinOp , T , 0hop ) ` x ) .ih x ) = ( ( U ` x ) .ih x ) ) )
5 eqeq1 
 |-  ( T = if ( T e. LinOp , T , 0hop ) -> ( T = U <-> if ( T e. LinOp , T , 0hop ) = U ) )
6 4 5 bibi12d 
 |-  ( T = if ( T e. LinOp , T , 0hop ) -> ( ( A. x e. ~H ( ( T ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> T = U ) <-> ( A. x e. ~H ( ( if ( T e. LinOp , T , 0hop ) ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> if ( T e. LinOp , T , 0hop ) = U ) ) )
7 fveq1 
 |-  ( U = if ( U e. LinOp , U , 0hop ) -> ( U ` x ) = ( if ( U e. LinOp , U , 0hop ) ` x ) )
8 7 oveq1d 
 |-  ( U = if ( U e. LinOp , U , 0hop ) -> ( ( U ` x ) .ih x ) = ( ( if ( U e. LinOp , U , 0hop ) ` x ) .ih x ) )
9 8 eqeq2d 
 |-  ( U = if ( U e. LinOp , U , 0hop ) -> ( ( ( if ( T e. LinOp , T , 0hop ) ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> ( ( if ( T e. LinOp , T , 0hop ) ` x ) .ih x ) = ( ( if ( U e. LinOp , U , 0hop ) ` x ) .ih x ) ) )
10 9 ralbidv 
 |-  ( U = if ( U e. LinOp , U , 0hop ) -> ( A. x e. ~H ( ( if ( T e. LinOp , T , 0hop ) ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> A. x e. ~H ( ( if ( T e. LinOp , T , 0hop ) ` x ) .ih x ) = ( ( if ( U e. LinOp , U , 0hop ) ` x ) .ih x ) ) )
11 eqeq2 
 |-  ( U = if ( U e. LinOp , U , 0hop ) -> ( if ( T e. LinOp , T , 0hop ) = U <-> if ( T e. LinOp , T , 0hop ) = if ( U e. LinOp , U , 0hop ) ) )
12 10 11 bibi12d 
 |-  ( U = if ( U e. LinOp , U , 0hop ) -> ( ( A. x e. ~H ( ( if ( T e. LinOp , T , 0hop ) ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> if ( T e. LinOp , T , 0hop ) = U ) <-> ( A. x e. ~H ( ( if ( T e. LinOp , T , 0hop ) ` x ) .ih x ) = ( ( if ( U e. LinOp , U , 0hop ) ` x ) .ih x ) <-> if ( T e. LinOp , T , 0hop ) = if ( U e. LinOp , U , 0hop ) ) ) )
13 0lnop 
 |-  0hop e. LinOp
14 13 elimel 
 |-  if ( T e. LinOp , T , 0hop ) e. LinOp
15 13 elimel 
 |-  if ( U e. LinOp , U , 0hop ) e. LinOp
16 14 15 lnopeqi 
 |-  ( A. x e. ~H ( ( if ( T e. LinOp , T , 0hop ) ` x ) .ih x ) = ( ( if ( U e. LinOp , U , 0hop ) ` x ) .ih x ) <-> if ( T e. LinOp , T , 0hop ) = if ( U e. LinOp , U , 0hop ) )
17 6 12 16 dedth2h 
 |-  ( ( T e. LinOp /\ U e. LinOp ) -> ( A. x e. ~H ( ( T ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> T = U ) )