# 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 ffvelrni
` |-  ( 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 ffvelrni
` |-  ( 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 )`
` |-  ( 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 )`