Theorem dipfval

Description: The inner product function on a normed complex vector space. The definition is meaningful for vector spaces that are also inner product spaces, i.e. satisfy the parallelogram law. (Contributed by NM, 10-Apr-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dipfval.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	dipfval.2	$$⊢G={+}_v\left(U\right)$$
	dipfval.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
	dipfval.6	$$⊢N={norm}_{CV}\left(U\right)$$
	dipfval.7	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
Assertion	dipfval	$$⊢U\in \mathrm{NrmCVec}\to P=\left(x\in X,y\in X⟼\frac{\sum _{k=1}^4{\mathrm{i}}^k{N\left(xG\left({\mathrm{i}}^{k}Sy\right)\right)}^2}{4}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dipfval.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		dipfval.2	$$⊢G={+}_v\left(U\right)$$
3		dipfval.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
4		dipfval.6	$$⊢N={norm}_{CV}\left(U\right)$$
5		dipfval.7	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
6		fveq2	$$⊢u=U\to \mathrm{BaseSet}\left(u\right)=\mathrm{BaseSet}\left(U\right)$$
7	6 1	eqtr4di	$$⊢u=U\to \mathrm{BaseSet}\left(u\right)=X$$
8		fveq2	$$⊢u=U\to {norm}_{CV}\left(u\right)={norm}_{CV}\left(U\right)$$
9	8 4	eqtr4di	$$⊢u=U\to {norm}_{CV}\left(u\right)=N$$
10		fveq2	$$⊢u=U\to {+}_v\left(u\right)={+}_v\left(U\right)$$
11	10 2	eqtr4di	$$⊢u=U\to {+}_v\left(u\right)=G$$
12		eqidd	$$⊢u=U\to x=x$$
13		fveq2	$$⊢u=U\to {\cdot }_{\mathrm{𝑠OLD}}\left(u\right)={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
14	13 3	eqtr4di	$$⊢u=U\to {\cdot }_{\mathrm{𝑠OLD}}\left(u\right)=S$$
15	14	oveqd	$$⊢u=U\to {\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(u\right)y={\mathrm{i}}^{k}Sy$$
16	11 12 15	oveq123d	$$⊢u=U\to x{+}_v\left(u\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(u\right)y\right)=xG\left({\mathrm{i}}^{k}Sy\right)$$
17	9 16	fveq12d	$$⊢u=U\to {norm}_{CV}\left(u\right)\left(x{+}_v\left(u\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(u\right)y\right)\right)=N\left(xG\left({\mathrm{i}}^{k}Sy\right)\right)$$
18	17	oveq1d	$$⊢u=U\to {{norm}_{CV}\left(u\right)\left(x{+}_v\left(u\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(u\right)y\right)\right)}^2={N\left(xG\left({\mathrm{i}}^{k}Sy\right)\right)}^2$$
19	18	oveq2d	$$⊢u=U\to {\mathrm{i}}^k{{norm}_{CV}\left(u\right)\left(x{+}_v\left(u\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(u\right)y\right)\right)}^2={\mathrm{i}}^k{N\left(xG\left({\mathrm{i}}^{k}Sy\right)\right)}^2$$
20	19	sumeq2sdv	$$⊢u=U\to \sum _{k=1}^4{\mathrm{i}}^k{{norm}_{CV}\left(u\right)\left(x{+}_v\left(u\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(u\right)y\right)\right)}^2=\sum _{k=1}^4{\mathrm{i}}^k{N\left(xG\left({\mathrm{i}}^{k}Sy\right)\right)}^2$$
21	20	oveq1d	$$⊢u=U\to \frac{\sum _{k=1}^4{\mathrm{i}}^k{{norm}_{CV}\left(u\right)\left(x{+}_v\left(u\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(u\right)y\right)\right)}^2}{4}=\frac{\sum _{k=1}^4{\mathrm{i}}^k{N\left(xG\left({\mathrm{i}}^{k}Sy\right)\right)}^2}{4}$$
22	7 7 21	mpoeq123dv	$$⊢u=U\to \left(x\in \mathrm{BaseSet}\left(u\right),y\in \mathrm{BaseSet}\left(u\right)⟼\frac{\sum _{k=1}^4{\mathrm{i}}^k{{norm}_{CV}\left(u\right)\left(x{+}_v\left(u\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(u\right)y\right)\right)}^2}{4}\right)=\left(x\in X,y\in X⟼\frac{\sum _{k=1}^4{\mathrm{i}}^k{N\left(xG\left({\mathrm{i}}^{k}Sy\right)\right)}^2}{4}\right)$$
23		df-dip	$$⊢{\cdot }_{\mathrm{𝑖OLD}}=\left(u\in \mathrm{NrmCVec}⟼\left(x\in \mathrm{BaseSet}\left(u\right),y\in \mathrm{BaseSet}\left(u\right)⟼\frac{\sum _{k=1}^4{\mathrm{i}}^k{{norm}_{CV}\left(u\right)\left(x{+}_v\left(u\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(u\right)y\right)\right)}^2}{4}\right)\right)$$
24	1	fvexi	$$⊢X\in \mathrm{V}$$
25	24 24	mpoex	$$⊢\left(x\in X,y\in X⟼\frac{\sum _{k=1}^4{\mathrm{i}}^k{N\left(xG\left({\mathrm{i}}^{k}Sy\right)\right)}^2}{4}\right)\in \mathrm{V}$$
26	22 23 25	fvmpt	$$⊢U\in \mathrm{NrmCVec}\to {\cdot }_{\mathrm{𝑖OLD}}\left(U\right)=\left(x\in X,y\in X⟼\frac{\sum _{k=1}^4{\mathrm{i}}^k{N\left(xG\left({\mathrm{i}}^{k}Sy\right)\right)}^2}{4}\right)$$
27	5 26	syl5eq	$$⊢U\in \mathrm{NrmCVec}\to P=\left(x\in X,y\in X⟼\frac{\sum _{k=1}^4{\mathrm{i}}^k{N\left(xG\left({\mathrm{i}}^{k}Sy\right)\right)}^2}{4}\right)$$