Theorem polidi

Description: Polarization identity. Recovers inner product from norm. Exercise 4(a) of ReedSimon p. 63. The outermost operation is + instead of - due to our mathematicians' (rather than physicists') version of Axiom ax-his3 . (Contributed by NM, 30-Jun-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	polid.1	$$⊢A\in \mathscr{H}$$
	polid.2	$$⊢B\in \mathscr{H}$$
Assertion	polidi	$$⊢A{\cdot }_{\mathrm{ih}}B=\frac{{{norm}_{ℎ}\left(A{+}_{ℎ}B\right)}^2-{{norm}_{ℎ}\left(A{-}_{ℎ}B\right)}^2+\mathrm{i}\left({{norm}_{ℎ}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)}^2-{{norm}_{ℎ}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)}^2\right)}{4}$$

Proof

Step	Hyp	Ref	Expression
1		polid.1	$$⊢A\in \mathscr{H}$$
2		polid.2	$$⊢B\in \mathscr{H}$$
3	1 2 2 1	polid2i	$$⊢A{\cdot }_{\mathrm{ih}}B=\frac{\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)}{4}$$
4	1 2	hvaddcli	$$⊢A{+}_{ℎ}B\in \mathscr{H}$$
5	4	normsqi	$$⊢{{norm}_{ℎ}\left(A{+}_{ℎ}B\right)}^2=\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)$$
6	1 2	hvsubcli	$$⊢A{-}_{ℎ}B\in \mathscr{H}$$
7	6	normsqi	$$⊢{{norm}_{ℎ}\left(A{-}_{ℎ}B\right)}^2=\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{-}_{ℎ}B\right)$$
8	5 7	oveq12i	$$⊢{{norm}_{ℎ}\left(A{+}_{ℎ}B\right)}^2-{{norm}_{ℎ}\left(A{-}_{ℎ}B\right)}^2=\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{-}_{ℎ}B\right)\right)$$
9		ax-icn	$$⊢\mathrm{i}\in ℂ$$
10	9 2	hvmulcli	$$⊢\mathrm{i}{\cdot }_{ℎ}B\in \mathscr{H}$$
11	1 10	hvaddcli	$$⊢A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\in \mathscr{H}$$
12	11	normsqi	$$⊢{{norm}_{ℎ}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)}^2=\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)$$
13	1 10	hvsubcli	$$⊢A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\in \mathscr{H}$$
14	13	normsqi	$$⊢{{norm}_{ℎ}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)}^2=\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)$$
15	12 14	oveq12i	$$⊢{{norm}_{ℎ}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)}^2-{{norm}_{ℎ}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)}^2=\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)$$
16	15	oveq2i	$$⊢\mathrm{i}\left({{norm}_{ℎ}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)}^2-{{norm}_{ℎ}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)}^2\right)=\mathrm{i}\left(\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)$$
17	8 16	oveq12i	$$⊢{{norm}_{ℎ}\left(A{+}_{ℎ}B\right)}^2-{{norm}_{ℎ}\left(A{-}_{ℎ}B\right)}^2+\mathrm{i}\left({{norm}_{ℎ}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)}^2-{{norm}_{ℎ}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)}^2\right)=\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)$$
18	17	oveq1i	$$⊢\frac{{{norm}_{ℎ}\left(A{+}_{ℎ}B\right)}^2-{{norm}_{ℎ}\left(A{-}_{ℎ}B\right)}^2+\mathrm{i}\left({{norm}_{ℎ}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)}^2-{{norm}_{ℎ}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)}^2\right)}{4}=\frac{\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)}{4}$$
19	3 18	eqtr4i	$$⊢A{\cdot }_{\mathrm{ih}}B=\frac{{{norm}_{ℎ}\left(A{+}_{ℎ}B\right)}^2-{{norm}_{ℎ}\left(A{-}_{ℎ}B\right)}^2+\mathrm{i}\left({{norm}_{ℎ}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)}^2-{{norm}_{ℎ}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)}^2\right)}{4}$$