# 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 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 )`
` |-  ( ( 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`
` |-  ( ( _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 )`