Theorem lnopeq0 9870

Description: A condition implying that a linear Hilbert space operator is identically zero. Unlike ho01 9694 for arbitrary operators, when the operator is linear we need to consider only the values of the quadratic form (T` x) .ih x).

Hypothesis

Ref	Expression
lnopeq0.1	|- T e. LinOp

Assertion

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

Distinct variable group:   x,T

Proof of Theorem lnopeq0

Step	Hyp	Ref	Expression
1		lnopeq0.1	. . . . . . . 8 |- T e. LinOp
2	1	lnopeq0lem2 9869	. . . . . . 7 |- ((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 388	. . . . . 6 |- ((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		fveq2 3715	. . . . . . . . . . . . . . . 16 |- (x = (y +h z) -> (T` x) = (T` (y +h z)))
5		id 59	. . . . . . . . . . . . . . . 16 |- (x = (y +h z) -> x = (y +h z))
6	4, 5	opreq12d 3969	. . . . . . . . . . . . . . 15 |- (x = (y +h z) -> ((T` x) .ih x) = ((T` (y +h z)) .ih (y +h z)))
7	6	eqeq1d 1480	. . . . . . . . . . . . . 14 |- (x = (y +h z) -> (((T` x) .ih x) = 0 <-> ((T` (y +h z)) .ih (y +h z)) = 0))
8	7	rcla4cva 1872	. . . . . . . . . . . . 13 |- ((A.x e. H~ ((T` x) .ih x) = 0 /\ (y +h z) e. H~) -> ((T` (y +h z)) .ih (y +h z)) = 0)
9		hvaddclt 8821	. . . . . . . . . . . . 13 |- ((y e. H~ /\ z e. H~) -> (y +h z) e. H~)
10	8, 9	sylan2 451	. . . . . . . . . . . 12 |- ((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		fveq2 3715	. . . . . . . . . . . . . . . 16 |- (x = (y -h z) -> (T` x) = (T` (y -h z)))
12		id 59	. . . . . . . . . . . . . . . 16 |- (x = (y -h z) -> x = (y -h z))
13	11, 12	opreq12d 3969	. . . . . . . . . . . . . . 15 |- (x = (y -h z) -> ((T` x) .ih x) = ((T` (y -h z)) .ih (y -h z)))
14	13	eqeq1d 1480	. . . . . . . . . . . . . 14 |- (x = (y -h z) -> (((T` x) .ih x) = 0 <-> ((T` (y -h z)) .ih (y -h z)) = 0))
15	14	rcla4cva 1872	. . . . . . . . . . . . 13 |- ((A.x e. H~ ((T` x) .ih x) = 0 /\ (y -h z) e. H~) -> ((T` (y -h z)) .ih (y -h z)) = 0)
16		hvsubclt 8826	. . . . . . . . . . . . 13 |- ((y e. H~ /\ z e. H~) -> (y -h z) e. H~)
17	15, 16	sylan2 451	. . . . . . . . . . . 12 |- ((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	opreq12d 3969	. . . . . . . . . . 11 |- ((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		0cn 5308	. . . . . . . . . . . 12 |- 0 e. CC
20	19	subid 5371	. . . . . . . . . . 11 |- (0 - 0) = 0
21	18, 20	syl6eq 1520	. . . . . . . . . 10 |- ((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)
22		fveq2 3715	. . . . . . . . . . . . . . . . . 18 |- (x = (y +h (i .h z)) -> (T` x) = (T` (y +h (i .h z))))
23		id 59	. . . . . . . . . . . . . . . . . 18 |- (x = (y +h (i .h z)) -> x = (y +h (i .h z)))
24	22, 23	opreq12d 3969	. . . . . . . . . . . . . . . . 17 |- (x = (y +h (i .h z)) -> ((T` x) .ih x) = ((T` (y +h (i .h z))) .ih (y +h (i .h z))))
25	24	eqeq1d 1480	. . . . . . . . . . . . . . . 16 |- (x = (y +h (i .h z)) -> (((T` x) .ih x) = 0 <-> ((T` (y +h (i .h z))) .ih (y +h (i .h z))) = 0))
26	25	rcla4cva 1872	. . . . . . . . . . . . . . 15 |- ((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)
27		hvaddclt 8821	. . . . . . . . . . . . . . . 16 |- ((y e. H~ /\ (i .h z) e. H~) -> (y +h (i .h z)) e. H~)
28		axicn 5250	. . . . . . . . . . . . . . . . 17 |- i e. CC
29		hvmulclt 8822	. . . . . . . . . . . . . . . . 17 |- ((i e. CC /\ z e. H~) -> (i .h z) e. H~)
30	28, 29	mpan 694	. . . . . . . . . . . . . . . 16 |- (z e. H~ -> (i .h z) e. H~)
31	27, 30	sylan2 451	. . . . . . . . . . . . . . 15 |- ((y e. H~ /\ z e. H~) -> (y +h (i .h z)) e. H~)
32	26, 31	sylan2 451	. . . . . . . . . . . . . 14 |- ((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)
33		fveq2 3715	. . . . . . . . . . . . . . . . . 18 |- (x = (y -h (i .h z)) -> (T` x) = (T` (y -h (i .h z))))
34		id 59	. . . . . . . . . . . . . . . . . 18 |- (x = (y -h (i .h z)) -> x = (y -h (i .h z)))
35	33, 34	opreq12d 3969	. . . . . . . . . . . . . . . . 17 |- (x = (y -h (i .h z)) -> ((T` x) .ih x) = ((T` (y -h (i .h z))) .ih (y -h (i .h z))))
36	35	eqeq1d 1480	. . . . . . . . . . . . . . . 16 |- (x = (y -h (i .h z)) -> (((T` x) .ih x) = 0 <-> ((T` (y -h (i .h z))) .ih (y -h (i .h z))) = 0))
37	36	rcla4cva 1872	. . . . . . . . . . . . . . 15 |- ((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)
38		hvsubclt 8826	. . . . . . . . . . . . . . . 16 |- ((y e. H~ /\ (i .h z) e. H~) -> (y -h (i .h z)) e. H~)
39	38, 30	sylan2 451	. . . . . . . . . . . . . . 15 |- ((y e. H~ /\ z e. H~) -> (y -h (i .h z)) e. H~)
40	37, 39	sylan2 451	. . . . . . . . . . . . . 14 |- ((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)
41	32, 40	opreq12d 3969	. . . . . . . . . . . . 13 |- ((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))
42	41, 20	syl6eq 1520	. . . . . . . . . . . 12 |- ((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)
43	42	opreq2d 3967	. . . . . . . . . . 11 |- ((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))
44	28	mul01 5411	. . . . . . . . . . 11 |- (i x. 0) = 0
45	43, 44	syl6eq 1520	. . . . . . . . . 10 |- ((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)
46	21, 45	opreq12d 3969	. . . . . . . . 9 |- ((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))