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 LinOp
Assertion lnopeq0i x T x ih x = 0 T = 0 hop

Proof

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