Theorem hhip

Description: The inner product operation of Hilbert space. (Contributed by NM, 17-Nov-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hhnv.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
Assertion	hhip	$$⊢{\cdot }_{\mathrm{ih}}={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2		polid	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to x{\cdot }_{\mathrm{ih}}y=\frac{{{norm}_{ℎ}\left(x{+}_{ℎ}y\right)}^2-{{norm}_{ℎ}\left(x{-}_{ℎ}y\right)}^2+\mathrm{i}\left({{norm}_{ℎ}\left(x{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}y\right)\right)}^2-{{norm}_{ℎ}\left(x{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}y\right)\right)}^2\right)}{4}$$
3	1	hhnv	$$⊢U\in \mathrm{NrmCVec}$$
4	1	hhba	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
5	1	hhva	$$⊢{+}_{ℎ}={+}_v\left(U\right)$$
6	1	hhsm	$$⊢{\cdot }_{ℎ}={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
7	1	hhnm	$$⊢{norm}_{ℎ}={norm}_{CV}\left(U\right)$$
8		eqid	$$⊢{\cdot }_{\mathrm{𝑖OLD}}\left(U\right)={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
9	1	hhvs	$$⊢{-}_{ℎ}={-}_v\left(U\right)$$
10	4 5 6 7 8 9	ipval3	$$⊢\left(U\in \mathrm{NrmCVec}\wedge x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to x{\cdot }_{\mathrm{𝑖OLD}}\left(U\right)y=\frac{{{norm}_{ℎ}\left(x{+}_{ℎ}y\right)}^2-{{norm}_{ℎ}\left(x{-}_{ℎ}y\right)}^2+\mathrm{i}\left({{norm}_{ℎ}\left(x{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}y\right)\right)}^2-{{norm}_{ℎ}\left(x{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}y\right)\right)}^2\right)}{4}$$
11	3 10	mp3an1	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to x{\cdot }_{\mathrm{𝑖OLD}}\left(U\right)y=\frac{{{norm}_{ℎ}\left(x{+}_{ℎ}y\right)}^2-{{norm}_{ℎ}\left(x{-}_{ℎ}y\right)}^2+\mathrm{i}\left({{norm}_{ℎ}\left(x{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}y\right)\right)}^2-{{norm}_{ℎ}\left(x{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}y\right)\right)}^2\right)}{4}$$
12	2 11	eqtr4d	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to x{\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{𝑖OLD}}\left(U\right)y$$
13	12	rgen2	$$⊢\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{𝑖OLD}}\left(U\right)y$$
14		ax-hfi	$$⊢{\cdot }_{\mathrm{ih}}:\mathscr{H}\times \mathscr{H}⟶ℂ$$
15	4 8	ipf	$$⊢U\in \mathrm{NrmCVec}\to {\cdot }_{\mathrm{𝑖OLD}}\left(U\right):\mathscr{H}\times \mathscr{H}⟶ℂ$$
16	3 15	ax-mp	$$⊢{\cdot }_{\mathrm{𝑖OLD}}\left(U\right):\mathscr{H}\times \mathscr{H}⟶ℂ$$
17		ffn	$$⊢{\cdot }_{\mathrm{ih}}:\mathscr{H}\times \mathscr{H}⟶ℂ\to {\cdot }_{\mathrm{ih}}Fn\left(\mathscr{H}\times \mathscr{H}\right)$$
18		ffn	$$⊢{\cdot }_{\mathrm{𝑖OLD}}\left(U\right):\mathscr{H}\times \mathscr{H}⟶ℂ\to {\cdot }_{\mathrm{𝑖OLD}}\left(U\right)Fn\left(\mathscr{H}\times \mathscr{H}\right)$$
19		eqfnov2	$$⊢\left({\cdot }_{\mathrm{ih}}Fn\left(\mathscr{H}\times \mathscr{H}\right)\wedge {\cdot }_{\mathrm{𝑖OLD}}\left(U\right)Fn\left(\mathscr{H}\times \mathscr{H}\right)\right)\to \left({\cdot }_{\mathrm{ih}}={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)\leftrightarrow \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{𝑖OLD}}\left(U\right)y\right)$$
20	17 18 19	syl2an	$$⊢\left({\cdot }_{\mathrm{ih}}:\mathscr{H}\times \mathscr{H}⟶ℂ\wedge {\cdot }_{\mathrm{𝑖OLD}}\left(U\right):\mathscr{H}\times \mathscr{H}⟶ℂ\right)\to \left({\cdot }_{\mathrm{ih}}={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)\leftrightarrow \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{𝑖OLD}}\left(U\right)y\right)$$
21	14 16 20	mp2an	$$⊢{\cdot }_{\mathrm{ih}}={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)\leftrightarrow \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{𝑖OLD}}\left(U\right)y$$
22	13 21	mpbir	$$⊢{\cdot }_{\mathrm{ih}}={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$