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 ) )
3 2 adantl 
 |-  ( ( 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 ) )
4 hvaddcl 
 |-  ( ( 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 )
24 hvaddcl 
 |-  ( ( 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 )
63 62 adantl 
 |-  ( ( T = 0hop /\ x e. ~H ) -> ( 0h .ih x ) = 0 )
64 61 63 eqtrd 
 |-  ( ( T = 0hop /\ x e. ~H ) -> ( ( T ` x ) .ih x ) = 0 )
65 64 ralrimiva 
 |-  ( T = 0hop -> A. x e. ~H ( ( T ` x ) .ih x ) = 0 )
66 57 65 impbii 
 |-  ( A. x e. ~H ( ( T ` x ) .ih x ) = 0 <-> T = 0hop )