# Metamath Proof Explorer

## Theorem lnopeq0i

Description: A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01i for arbitrary operators, when the operator is linear we need to consider only the values of the quadratic form ( Tx ) .ih x ) . (Contributed by NM, 26-Jul-2006) (New usage is discouraged.)

Ref Expression
Hypothesis lnopeq0.1
`|- T e. LinOp`
Assertion lnopeq0i
`|- ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 <-> T = 0hop )`

### Proof

Step Hyp Ref Expression
1 lnopeq0.1
` |-  T e. LinOp`
2 1 lnopeq0lem2
` |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( T ` y ) .ih z ) = ( ( ( ( ( T ` ( y +h z ) ) .ih ( y +h z ) ) - ( ( T ` ( y -h z ) ) .ih ( y -h z ) ) ) + ( _i x. ( ( ( T ` ( y +h ( _i .h z ) ) ) .ih ( y +h ( _i .h z ) ) ) - ( ( T ` ( y -h ( _i .h z ) ) ) .ih ( y -h ( _i .h z ) ) ) ) ) ) / 4 ) )`
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( T ` y ) .ih z ) = ( ( ( ( ( T ` ( y +h z ) ) .ih ( y +h z ) ) - ( ( T ` ( y -h z ) ) .ih ( y -h z ) ) ) + ( _i x. ( ( ( T ` ( y +h ( _i .h z ) ) ) .ih ( y +h ( _i .h z ) ) ) - ( ( T ` ( y -h ( _i .h z ) ) ) .ih ( y -h ( _i .h z ) ) ) ) ) ) / 4 ) )`
` |-  ( ( y e. ~H /\ z e. ~H ) -> ( y +h z ) e. ~H )`
5 fveq2
` |-  ( x = ( y +h z ) -> ( T ` x ) = ( T ` ( y +h z ) ) )`
6 id
` |-  ( x = ( y +h z ) -> x = ( y +h z ) )`
7 5 6 oveq12d
` |-  ( x = ( y +h z ) -> ( ( T ` x ) .ih x ) = ( ( T ` ( y +h z ) ) .ih ( y +h z ) ) )`
8 7 eqeq1d
` |-  ( x = ( y +h z ) -> ( ( ( T ` x ) .ih x ) = 0 <-> ( ( T ` ( y +h z ) ) .ih ( y +h z ) ) = 0 ) )`
9 8 rspccva
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y +h z ) e. ~H ) -> ( ( T ` ( y +h z ) ) .ih ( y +h z ) ) = 0 )`
10 4 9 sylan2
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( T ` ( y +h z ) ) .ih ( y +h z ) ) = 0 )`
11 hvsubcl
` |-  ( ( y e. ~H /\ z e. ~H ) -> ( y -h z ) e. ~H )`
12 fveq2
` |-  ( x = ( y -h z ) -> ( T ` x ) = ( T ` ( y -h z ) ) )`
13 id
` |-  ( x = ( y -h z ) -> x = ( y -h z ) )`
14 12 13 oveq12d
` |-  ( x = ( y -h z ) -> ( ( T ` x ) .ih x ) = ( ( T ` ( y -h z ) ) .ih ( y -h z ) ) )`
15 14 eqeq1d
` |-  ( x = ( y -h z ) -> ( ( ( T ` x ) .ih x ) = 0 <-> ( ( T ` ( y -h z ) ) .ih ( y -h z ) ) = 0 ) )`
16 15 rspccva
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y -h z ) e. ~H ) -> ( ( T ` ( y -h z ) ) .ih ( y -h z ) ) = 0 )`
17 11 16 sylan2
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( T ` ( y -h z ) ) .ih ( y -h z ) ) = 0 )`
18 10 17 oveq12d
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( ( T ` ( y +h z ) ) .ih ( y +h z ) ) - ( ( T ` ( y -h z ) ) .ih ( y -h z ) ) ) = ( 0 - 0 ) )`
19 0m0e0
` |-  ( 0 - 0 ) = 0`
20 18 19 eqtrdi
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( ( T ` ( y +h z ) ) .ih ( y +h z ) ) - ( ( T ` ( y -h z ) ) .ih ( y -h z ) ) ) = 0 )`
21 ax-icn
` |-  _i e. CC`
22 hvmulcl
` |-  ( ( _i e. CC /\ z e. ~H ) -> ( _i .h z ) e. ~H )`
23 21 22 mpan
` |-  ( z e. ~H -> ( _i .h z ) e. ~H )`
` |-  ( ( y e. ~H /\ ( _i .h z ) e. ~H ) -> ( y +h ( _i .h z ) ) e. ~H )`
25 23 24 sylan2
` |-  ( ( y e. ~H /\ z e. ~H ) -> ( y +h ( _i .h z ) ) e. ~H )`
26 fveq2
` |-  ( x = ( y +h ( _i .h z ) ) -> ( T ` x ) = ( T ` ( y +h ( _i .h z ) ) ) )`
27 id
` |-  ( x = ( y +h ( _i .h z ) ) -> x = ( y +h ( _i .h z ) ) )`
28 26 27 oveq12d
` |-  ( x = ( y +h ( _i .h z ) ) -> ( ( T ` x ) .ih x ) = ( ( T ` ( y +h ( _i .h z ) ) ) .ih ( y +h ( _i .h z ) ) ) )`
29 28 eqeq1d
` |-  ( x = ( y +h ( _i .h z ) ) -> ( ( ( T ` x ) .ih x ) = 0 <-> ( ( T ` ( y +h ( _i .h z ) ) ) .ih ( y +h ( _i .h z ) ) ) = 0 ) )`
30 29 rspccva
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y +h ( _i .h z ) ) e. ~H ) -> ( ( T ` ( y +h ( _i .h z ) ) ) .ih ( y +h ( _i .h z ) ) ) = 0 )`
31 25 30 sylan2
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( T ` ( y +h ( _i .h z ) ) ) .ih ( y +h ( _i .h z ) ) ) = 0 )`
32 hvsubcl
` |-  ( ( y e. ~H /\ ( _i .h z ) e. ~H ) -> ( y -h ( _i .h z ) ) e. ~H )`
33 23 32 sylan2
` |-  ( ( y e. ~H /\ z e. ~H ) -> ( y -h ( _i .h z ) ) e. ~H )`
34 fveq2
` |-  ( x = ( y -h ( _i .h z ) ) -> ( T ` x ) = ( T ` ( y -h ( _i .h z ) ) ) )`
35 id
` |-  ( x = ( y -h ( _i .h z ) ) -> x = ( y -h ( _i .h z ) ) )`
36 34 35 oveq12d
` |-  ( x = ( y -h ( _i .h z ) ) -> ( ( T ` x ) .ih x ) = ( ( T ` ( y -h ( _i .h z ) ) ) .ih ( y -h ( _i .h z ) ) ) )`
37 36 eqeq1d
` |-  ( x = ( y -h ( _i .h z ) ) -> ( ( ( T ` x ) .ih x ) = 0 <-> ( ( T ` ( y -h ( _i .h z ) ) ) .ih ( y -h ( _i .h z ) ) ) = 0 ) )`
38 37 rspccva
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y -h ( _i .h z ) ) e. ~H ) -> ( ( T ` ( y -h ( _i .h z ) ) ) .ih ( y -h ( _i .h z ) ) ) = 0 )`
39 33 38 sylan2
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( T ` ( y -h ( _i .h z ) ) ) .ih ( y -h ( _i .h z ) ) ) = 0 )`
40 31 39 oveq12d
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( ( T ` ( y +h ( _i .h z ) ) ) .ih ( y +h ( _i .h z ) ) ) - ( ( T ` ( y -h ( _i .h z ) ) ) .ih ( y -h ( _i .h z ) ) ) ) = ( 0 - 0 ) )`
41 40 19 eqtrdi
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( ( T ` ( y +h ( _i .h z ) ) ) .ih ( y +h ( _i .h z ) ) ) - ( ( T ` ( y -h ( _i .h z ) ) ) .ih ( y -h ( _i .h z ) ) ) ) = 0 )`
42 41 oveq2d
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y e. ~H /\ z e. ~H ) ) -> ( _i x. ( ( ( T ` ( y +h ( _i .h z ) ) ) .ih ( y +h ( _i .h z ) ) ) - ( ( T ` ( y -h ( _i .h z ) ) ) .ih ( y -h ( _i .h z ) ) ) ) ) = ( _i x. 0 ) )`
43 it0e0
` |-  ( _i x. 0 ) = 0`
44 42 43 eqtrdi
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y e. ~H /\ z e. ~H ) ) -> ( _i x. ( ( ( T ` ( y +h ( _i .h z ) ) ) .ih ( y +h ( _i .h z ) ) ) - ( ( T ` ( y -h ( _i .h z ) ) ) .ih ( y -h ( _i .h z ) ) ) ) ) = 0 )`
45 20 44 oveq12d
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( ( ( T ` ( y +h z ) ) .ih ( y +h z ) ) - ( ( T ` ( y -h z ) ) .ih ( y -h z ) ) ) + ( _i x. ( ( ( T ` ( y +h ( _i .h z ) ) ) .ih ( y +h ( _i .h z ) ) ) - ( ( T ` ( y -h ( _i .h z ) ) ) .ih ( y -h ( _i .h z ) ) ) ) ) ) = ( 0 + 0 ) )`
46 00id
` |-  ( 0 + 0 ) = 0`
47 45 46 eqtrdi
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( ( ( T ` ( y +h z ) ) .ih ( y +h z ) ) - ( ( T ` ( y -h z ) ) .ih ( y -h z ) ) ) + ( _i x. ( ( ( T ` ( y +h ( _i .h z ) ) ) .ih ( y +h ( _i .h z ) ) ) - ( ( T ` ( y -h ( _i .h z ) ) ) .ih ( y -h ( _i .h z ) ) ) ) ) ) = 0 )`
48 47 oveq1d
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( ( ( ( T ` ( y +h z ) ) .ih ( y +h z ) ) - ( ( T ` ( y -h z ) ) .ih ( y -h z ) ) ) + ( _i x. ( ( ( T ` ( y +h ( _i .h z ) ) ) .ih ( y +h ( _i .h z ) ) ) - ( ( T ` ( y -h ( _i .h z ) ) ) .ih ( y -h ( _i .h z ) ) ) ) ) ) / 4 ) = ( 0 / 4 ) )`
49 4cn
` |-  4 e. CC`
50 4ne0
` |-  4 =/= 0`
51 49 50 div0i
` |-  ( 0 / 4 ) = 0`
52 48 51 eqtrdi
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( ( ( ( T ` ( y +h z ) ) .ih ( y +h z ) ) - ( ( T ` ( y -h z ) ) .ih ( y -h z ) ) ) + ( _i x. ( ( ( T ` ( y +h ( _i .h z ) ) ) .ih ( y +h ( _i .h z ) ) ) - ( ( T ` ( y -h ( _i .h z ) ) ) .ih ( y -h ( _i .h z ) ) ) ) ) ) / 4 ) = 0 )`
53 3 52 eqtrd
` |-  ( ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 /\ ( y e. ~H /\ z e. ~H ) ) -> ( ( T ` y ) .ih z ) = 0 )`
54 53 ralrimivva
` |-  ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 -> A. y e. ~H A. z e. ~H ( ( T ` y ) .ih z ) = 0 )`
55 1 lnopfi
` |-  T : ~H --> ~H`
56 55 ho01i
` |-  ( A. y e. ~H A. z e. ~H ( ( T ` y ) .ih z ) = 0 <-> T = 0hop )`
57 54 56 sylib
` |-  ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 -> T = 0hop )`
58 fveq1
` |-  ( T = 0hop -> ( T ` x ) = ( 0hop ` x ) )`
59 ho0val
` |-  ( x e. ~H -> ( 0hop ` x ) = 0h )`
60 58 59 sylan9eq
` |-  ( ( T = 0hop /\ x e. ~H ) -> ( T ` x ) = 0h )`
61 60 oveq1d
` |-  ( ( T = 0hop /\ x e. ~H ) -> ( ( T ` x ) .ih x ) = ( 0h .ih x ) )`
62 hi01
` |-  ( x e. ~H -> ( 0h .ih x ) = 0 )`
` |-  ( ( T = 0hop /\ x e. ~H ) -> ( 0h .ih x ) = 0 )`
` |-  ( ( T = 0hop /\ x e. ~H ) -> ( ( T ` x ) .ih x ) = 0 )`
` |-  ( T = 0hop -> A. x e. ~H ( ( T ` x ) .ih x ) = 0 )`
` |-  ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 <-> T = 0hop )`