This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmi 
 |-  ( A e. ~H -> ( T ` A ) e. ~H )
6 2 5 ax-mp 
 |-  ( T ` A ) e. ~H
7 4 ffvelcdmi 
 |-  ( 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 )