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 ) )`