Theorem lnopeq0lem1

Description: Lemma for lnopeq0i . Apply the generalized polarization identity polid2i to the quadratic form ( ( Tx ) , x ) . (Contributed by NM, 26-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lnopeq0.1	|- T e. LinOp
	lnopeq0lem1.2	|- A e. ~H
	lnopeq0lem1.3	|- B e. ~H
Assertion	lnopeq0lem1	|- ( ( 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

Step	Hyp	Ref	Expression
1		lnopeq0.1	|- T e. LinOp
2		lnopeq0lem1.2	|- A e. ~H
3		lnopeq0lem1.3	|- B e. ~H
4	1	lnopfi	|- T : ~H --> ~H
5	4	ffvelrni	|- ( A e. ~H -> ( T ` A ) e. ~H )
6	2 5	ax-mp	|- ( T ` A ) e. ~H
7	4	ffvelrni	|- ( B e. ~H -> ( T ` B ) e. ~H )
8	3 7	ax-mp	|- ( T ` B ) e. ~H
9	6 3 8 2	polid2i	|- ( ( T ` A ) .ih B ) = ( ( ( ( ( ( T ` A ) +h ( T ` B ) ) .ih ( A +h B ) ) - ( ( ( T ` A ) -h ( T ` B ) ) .ih ( A -h B ) ) ) + ( _i x. ( ( ( ( T ` A ) +h ( _i .h ( T ` B ) ) ) .ih ( A +h ( _i .h B ) ) ) - ( ( ( T ` A ) -h ( _i .h ( T ` B ) ) ) .ih ( A -h ( _i .h B ) ) ) ) ) ) / 4 )
10	1	lnopaddi	|- ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A +h B ) ) = ( ( T ` A ) +h ( T ` B ) ) )
11	2 3 10	mp2an	|- ( T ` ( A +h B ) ) = ( ( T ` A ) +h ( T ` B ) )
12	11	oveq1i	|- ( ( T ` ( A +h B ) ) .ih ( A +h B ) ) = ( ( ( T ` A ) +h ( T ` B ) ) .ih ( A +h B ) )
13	1	lnopsubi	|- ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A -h B ) ) = ( ( T ` A ) -h ( T ` B ) ) )
14	2 3 13	mp2an	|- ( T ` ( A -h B ) ) = ( ( T ` A ) -h ( T ` B ) )
15	14	oveq1i	|- ( ( T ` ( A -h B ) ) .ih ( A -h B ) ) = ( ( ( T ` A ) -h ( T ` B ) ) .ih ( A -h B ) )
16	12 15	oveq12i	|- ( ( ( T ` ( A +h B ) ) .ih ( A +h B ) ) - ( ( T ` ( A -h B ) ) .ih ( A -h B ) ) ) = ( ( ( ( T ` A ) +h ( T ` B ) ) .ih ( A +h B ) ) - ( ( ( T ` A ) -h ( T ` B ) ) .ih ( A -h B ) ) )
17		ax-icn	|- _i e. CC
18	1	lnopaddmuli	|- ( ( _i e. CC /\ A e. ~H /\ B e. ~H ) -> ( T ` ( A +h ( _i .h B ) ) ) = ( ( T ` A ) +h ( _i .h ( T ` B ) ) ) )
19	17 2 3 18	mp3an	|- ( T ` ( A +h ( _i .h B ) ) ) = ( ( T ` A ) +h ( _i .h ( T ` B ) ) )
20	19	oveq1i	|- ( ( T ` ( A +h ( _i .h B ) ) ) .ih ( A +h ( _i .h B ) ) ) = ( ( ( T ` A ) +h ( _i .h ( T ` B ) ) ) .ih ( A +h ( _i .h B ) ) )
21	1	lnopsubmuli	|- ( ( _i e. CC /\ A e. ~H /\ B e. ~H ) -> ( T ` ( A -h ( _i .h B ) ) ) = ( ( T ` A ) -h ( _i .h ( T ` B ) ) ) )
22	17 2 3 21	mp3an	|- ( T ` ( A -h ( _i .h B ) ) ) = ( ( T ` A ) -h ( _i .h ( T ` B ) ) )
23	22	oveq1i	|- ( ( T ` ( A -h ( _i .h B ) ) ) .ih ( A -h ( _i .h B ) ) ) = ( ( ( T ` A ) -h ( _i .h ( T ` B ) ) ) .ih ( A -h ( _i .h B ) ) )
24	20 23	oveq12i	|- ( ( ( 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 ` A ) +h ( _i .h ( T ` B ) ) ) .ih ( A +h ( _i .h B ) ) ) - ( ( ( T ` A ) -h ( _i .h ( T ` B ) ) ) .ih ( A -h ( _i .h B ) ) ) )
25	24	oveq2i	|- ( _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 ` A ) +h ( _i .h ( T ` B ) ) ) .ih ( A +h ( _i .h B ) ) ) - ( ( ( T ` A ) -h ( _i .h ( T ` B ) ) ) .ih ( A -h ( _i .h B ) ) ) ) )
26	16 25	oveq12i	|- ( ( ( ( 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 ` A ) +h ( T ` B ) ) .ih ( A +h B ) ) - ( ( ( T ` A ) -h ( T ` B ) ) .ih ( A -h B ) ) ) + ( _i x. ( ( ( ( T ` A ) +h ( _i .h ( T ` B ) ) ) .ih ( A +h ( _i .h B ) ) ) - ( ( ( T ` A ) -h ( _i .h ( T ` B ) ) ) .ih ( A -h ( _i .h B ) ) ) ) ) )
27	26	oveq1i	|- ( ( ( ( ( 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 ` A ) +h ( T ` B ) ) .ih ( A +h B ) ) - ( ( ( T ` A ) -h ( T ` B ) ) .ih ( A -h B ) ) ) + ( _i x. ( ( ( ( T ` A ) +h ( _i .h ( T ` B ) ) ) .ih ( A +h ( _i .h B ) ) ) - ( ( ( T ` A ) -h ( _i .h ( T ` B ) ) ) .ih ( A -h ( _i .h B ) ) ) ) ) ) / 4 )
28	9 27	eqtr4i	|- ( ( 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 )