# 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}\in \mathrm{LinOp}$
lnopeq0lem1.2 ${⊢}{A}\in ℋ$
lnopeq0lem1.3 ${⊢}{B}\in ℋ$
Assertion lnopeq0lem1 ${⊢}{T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}=\frac{\left({T}\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)\right)-\left({T}\left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left({T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)}{4}$

### Proof

Step Hyp Ref Expression
1 lnopeq0.1 ${⊢}{T}\in \mathrm{LinOp}$
2 lnopeq0lem1.2 ${⊢}{A}\in ℋ$
3 lnopeq0lem1.3 ${⊢}{B}\in ℋ$
4 1 lnopfi ${⊢}{T}:ℋ⟶ℋ$
5 4 ffvelrni ${⊢}{A}\in ℋ\to {T}\left({A}\right)\in ℋ$
6 2 5 ax-mp ${⊢}{T}\left({A}\right)\in ℋ$
7 4 ffvelrni ${⊢}{B}\in ℋ\to {T}\left({B}\right)\in ℋ$
8 3 7 ax-mp ${⊢}{T}\left({B}\right)\in ℋ$
9 6 3 8 2 polid2i ${⊢}{T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}=\frac{\left(\left({T}\left({A}\right){+}_{ℎ}{T}\left({B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)\right)-\left(\left({T}\left({A}\right){-}_{ℎ}{T}\left({B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left(\left({T}\left({A}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{T}\left({B}\right)\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left(\left({T}\left({A}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{T}\left({B}\right)\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)}{4}$
10 1 lnopaddi ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}{+}_{ℎ}{B}\right)={T}\left({A}\right){+}_{ℎ}{T}\left({B}\right)$
11 2 3 10 mp2an ${⊢}{T}\left({A}{+}_{ℎ}{B}\right)={T}\left({A}\right){+}_{ℎ}{T}\left({B}\right)$
12 11 oveq1i ${⊢}{T}\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)=\left({T}\left({A}\right){+}_{ℎ}{T}\left({B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)$
13 1 lnopsubi ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}{-}_{ℎ}{B}\right)={T}\left({A}\right){-}_{ℎ}{T}\left({B}\right)$
14 2 3 13 mp2an ${⊢}{T}\left({A}{-}_{ℎ}{B}\right)={T}\left({A}\right){-}_{ℎ}{T}\left({B}\right)$
15 14 oveq1i ${⊢}{T}\left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)=\left({T}\left({A}\right){-}_{ℎ}{T}\left({B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)$
16 12 15 oveq12i ${⊢}\left({T}\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)\right)-\left({T}\left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)=\left(\left({T}\left({A}\right){+}_{ℎ}{T}\left({B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)\right)-\left(\left({T}\left({A}\right){-}_{ℎ}{T}\left({B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)$
17 ax-icn ${⊢}\mathrm{i}\in ℂ$
18 1 lnopaddmuli ${⊢}\left(\mathrm{i}\in ℂ\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)={T}\left({A}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{T}\left({B}\right)\right)$
19 17 2 3 18 mp3an ${⊢}{T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)={T}\left({A}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{T}\left({B}\right)\right)$
20 19 oveq1i ${⊢}{T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)=\left({T}\left({A}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{T}\left({B}\right)\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)$
21 1 lnopsubmuli ${⊢}\left(\mathrm{i}\in ℂ\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)={T}\left({A}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{T}\left({B}\right)\right)$
22 17 2 3 21 mp3an ${⊢}{T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)={T}\left({A}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{T}\left({B}\right)\right)$
23 22 oveq1i ${⊢}{T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)=\left({T}\left({A}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{T}\left({B}\right)\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)$
24 20 23 oveq12i ${⊢}\left({T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)=\left(\left({T}\left({A}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{T}\left({B}\right)\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left(\left({T}\left({A}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{T}\left({B}\right)\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)$
25 24 oveq2i ${⊢}\mathrm{i}\left(\left({T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)=\mathrm{i}\left(\left(\left({T}\left({A}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{T}\left({B}\right)\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left(\left({T}\left({A}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{T}\left({B}\right)\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)$
26 16 25 oveq12i ${⊢}\left({T}\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)\right)-\left({T}\left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left({T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)=\left(\left({T}\left({A}\right){+}_{ℎ}{T}\left({B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)\right)-\left(\left({T}\left({A}\right){-}_{ℎ}{T}\left({B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left(\left({T}\left({A}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{T}\left({B}\right)\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left(\left({T}\left({A}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{T}\left({B}\right)\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)$
27 26 oveq1i ${⊢}\frac{\left({T}\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)\right)-\left({T}\left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left({T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)}{4}=\frac{\left(\left({T}\left({A}\right){+}_{ℎ}{T}\left({B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)\right)-\left(\left({T}\left({A}\right){-}_{ℎ}{T}\left({B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left(\left({T}\left({A}\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{T}\left({B}\right)\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left(\left({T}\left({A}\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{T}\left({B}\right)\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)}{4}$
28 9 27 eqtr4i ${⊢}{T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}=\frac{\left({T}\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}{B}\right)\right)-\left({T}\left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)+\mathrm{i}\left(\left({T}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)-\left({T}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}{B}\right)\right)\right)\right)}{4}$