Theorem lnopeq0lem2 9931

Description: Lemma for lnopeq0 9932.

Hypothesis

Ref	Expression
lnopeq0.1	|- T e. LinOp

Assertion

Ref	Expression
lnopeq0lem2	|- ((A e. H~ /\ B e. H~) -> ((T` A) .ih B) = (((((T` (A +h B)) .ih (A +h B)) - ((T` (A -h B)) .ih (A -h B))) + (i x. (((T` (A +h (i .h B))) .ih (A +h (i .h B))) - ((T` (A -h (i .h B))) .ih (A -h (i .h B)))))) / 4))

Proof of Theorem lnopeq0lem2

Step	Hyp	Ref	Expression
1		fveq2 3724	. . . 4 |- (A = if(A e. H~, A, 0h) -> (T` A) = (T` if(A e. H~, A, 0h)))
2	1	opreq1d 3975	. . 3 |- (A = if(A e. H~, A, 0h) -> ((T` A) .ih B) = ((T` if(A e. H~, A, 0h)) .ih B))
3		opreq1 3968	. . . . . . . 8 |- (A = if(A e. H~, A, 0h) -> (A +h B) = (if(A e. H~, A, 0h) +h B))
4	3	fveq2d 3728	. . . . . . 7 |- (A = if(A e. H~, A, 0h) -> (T` (A +h B)) = (T` (if(A e. H~, A, 0h) +h B)))
5	4, 3	opreq12d 3978	. . . . . 6 |- (A = if(A e. H~, A, 0h) -> ((T` (A +h B)) .ih (A +h B)) = ((T` (if(A e. H~, A, 0h) +h B)) .ih (if(A e. H~, A, 0h) +h B)))
6		opreq1 3968	. . . . . . . 8 |- (A = if(A e. H~, A, 0h) -> (A -h B) = (if(A e. H~, A, 0h) -h B))
7	6	fveq2d 3728	. . . . . . 7 |- (A = if(A e. H~, A, 0h) -> (T` (A -h B)) = (T` (if(A e. H~, A, 0h) -h B)))
8	7, 6	opreq12d 3978	. . . . . 6 |- (A = if(A e. H~, A, 0h) -> ((T` (A -h B)) .ih (A -h B)) = ((T` (if(A e. H~, A, 0h) -h B)) .ih (if(A e. H~, A, 0h) -h B)))
9	5, 8	opreq12d 3978	. . . . 5 |- (A = if(A e. H~, A, 0h) -> (((T` (A +h B)) .ih (A +h B)) - ((T` (A -h B)) .ih (A -h B))) = (((T` (if(A e. H~, A, 0h) +h B)) .ih (if(A e. H~, A, 0h) +h B)) - ((T` (if(A e. H~, A, 0h) -h B)) .ih (if(A e. H~, A, 0h) -h B))))
10		opreq1 3968	. . . . . . . . 9 |- (A = if(A e. H~, A, 0h) -> (A +h (i .h B)) = (if(A e. H~, A, 0h) +h (i .h B)))
11	10	fveq2d 3728	. . . . . . . 8 |- (A = if(A e. H~, A, 0h) -> (T` (A +h (i .h B))) = (T` (if(A e. H~, A, 0h) +h (i .h B))))
12	11, 10	opreq12d 3978	. . . . . . 7 |- (A = if(A e. H~, A, 0h) -> ((T` (A +h (i .h B))) .ih (A +h (i .h B))) = ((T` (if(A e. H~, A, 0h) +h (i .h B))) .ih (if(A e. H~, A, 0h) +h (i .h B))))
13		opreq1 3968	. . . . . . . . 9 |- (A = if(A e. H~, A, 0h) -> (A -h (i .h B)) = (if(A e. H~, A, 0h) -h (i .h B)))
14	13	fveq2d 3728	. . . . . . . 8 |- (A = if(A e. H~, A, 0h) -> (T` (A -h (i .h B))) = (T` (if(A e. H~, A, 0h) -h (i .h B))))
15	14, 13	opreq12d 3978	. . . . . . 7 |- (A = if(A e. H~, A, 0h) -> ((T` (A -h (i .h B))) .ih (A -h (i .h B))) = ((T` (if(A e. H~, A, 0h) -h (i .h B))) .ih (if(A e. H~, A, 0h) -h (i .h B))))
16	12, 15	opreq12d 3978	. . . . . 6 |- (A = if(A e. H~, A, 0h) -> (((T` (A +h (i .h B))) .ih (A +h (i .h B))) - ((T` (A -h (i .h B))) .ih (A -h (i .h B)))) = (((T` (if(A e. H~, A, 0h) +h (i .h B))) .ih (if(A e. H~, A, 0h) +h (i .h B))) - ((T` (if(A e. H~, A, 0h) -h (i .h B))) .ih (if(A e. H~, A, 0h) -h (i .h B)))))
17	16	opreq2d 3976	. . . . 5 |- (A = if(A e. H~, A, 0h) -> (i x. (((T` (A +h (i .h B))) .ih (A +h (i .h B))) - ((T` (A -h (i .h B))) .ih (A -h (i .h B))))) = (i x. (((T` (if(A e. H~, A, 0h) +h (i .h B))) .ih (if(A e. H~, A, 0h) +h (i .h B))) - ((T` (if(A e. H~, A, 0h) -h (i .h B))) .ih (if(A e. H~, A, 0h) -h (i .h B))))))
18	9, 17	opreq12d 3978	. . . 4 |- (A = if(A e. H~, A, 0h) -> ((((T` (A +h B)) .ih (A +h B)) - ((T` (A -h B)) .ih (A -h B))) + (i x. (((T` (A +h (i .h B))) .ih (A +h (i .h B))) - ((T` (A -h (i .h B))) .ih (A -h (i .h B)))))) = ((((T` (if(A e. H~, A, 0h) +h B)) .ih (if(A e. H~, A, 0h) +h B)) - ((T` (if(A e. H~, A, 0h) -h B)) .ih (if(A e. H~, A, 0h) -h B))) + (i x. (((T` (if(A e. H~, A, 0h) +h (i .h B))) .ih (if(A e. H~, A, 0h) +h (i .h B))) - ((T` (if(A e. H~, A, 0h) -h (i .h B))) .ih (if(A e. H~, A, 0h) -h (i .h B)))))))
19	18	opreq1d 3975	. . 3 |- (A = if(A e. H~, A, 0h) -> (((((T` (A +h B)) .ih (A +h B)) - ((T` (A -h B)) .ih (A -h B))) + (i x. (((T` (A +h (i .h B))) .ih (A +h (i .h B))) - ((T` (A -h (i .h B))) .ih (A -h (i .h B)))))) / 4) = (((((T` (if(A e. H~, A, 0h) +h B)) .ih (if(A e. H~, A, 0h) +h B)) - ((T` (if(A e. H~, A, 0h) -h B)) .ih (if(A e. H~, A, 0h) -h B))) + (i x. (((T` (if(A e. H~, A, 0h) +h (i .h B))) .ih (if(A e. H~, A, 0h) +h (i .h B))) - ((T` (if(A e. H~, A, 0h) -h (i .h B))) .ih (if(A e. H~, A, 0h) -h (i .h B)))))) / 4))
20	2, 19	eqeq12d 1489	. 2 |- (A = if(A e. H~, A, 0h) -> (((T` A) .ih B) = (((((T` (A +h B)) .ih (A +h B)) - ((T` (A -h B)) .ih (A -h B))) + (i x. (((T` (A +h (i .h B))) .ih (A +h (i .h B))) - ((T` (A -h (i .h B))) .ih (A -h (i .h B)))))) / 4) <-> ((T` if(A e. H~, A, 0h)) .ih B) = (((((T` (if(A e. H~, A, 0h) +h B)) .ih (if(A e. H~, A, 0h) +h B)) - ((T` (if(A e. H~, A, 0h) -h B)) .ih (if(A e. H~, A, 0h) -h B))) + (i x. (((T` (if(A e. H~, A, 0h) +h (i .h B))) .ih (if(A e. H~, A, 0h) +h (i .h B))) - ((T` (if(A e. H~, A, 0h) -h (i .h B))) .ih (if(A e. H~, A,