Theorem ipval

Description: Value of the inner product. The definition is meaningful for normed complex vector spaces that are also inner product spaces, i.e. satisfy the parallelogram law, although for convenience we define it for any normed complex vector space. The vector (group) addition operation is G , the scalar product is S , the norm is N , and the set of vectors is X . Equation 6.45 of Ponnusamy p. 361. (Contributed by NM, 31-Jan-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	ipval	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\wedge B\in X\right)\to APB=\frac{\sum _{k=1}^4{\mathrm{i}}^k{N\left(AG\left({\mathrm{i}}^{k}SB\right)\right)}^2}{4}$$

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	1 2 3 4 5	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)$$
7	6	oveqd	$$⊢U\in \mathrm{NrmCVec}\to APB=A\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)B$$
8		fvoveq1	$$⊢x=A\to N\left(xG\left({\mathrm{i}}^{k}Sy\right)\right)=N\left(AG\left({\mathrm{i}}^{k}Sy\right)\right)$$
9	8	oveq1d	$$⊢x=A\to {N\left(xG\left({\mathrm{i}}^{k}Sy\right)\right)}^2={N\left(AG\left({\mathrm{i}}^{k}Sy\right)\right)}^2$$
10	9	oveq2d	$$⊢x=A\to {\mathrm{i}}^k{N\left(xG\left({\mathrm{i}}^{k}Sy\right)\right)}^2={\mathrm{i}}^k{N\left(AG\left({\mathrm{i}}^{k}Sy\right)\right)}^2$$
11	10	sumeq2sdv	$$⊢x=A\to \sum _{k=1}^4{\mathrm{i}}^k{N\left(xG\left({\mathrm{i}}^{k}Sy\right)\right)}^2=\sum _{k=1}^4{\mathrm{i}}^k{N\left(AG\left({\mathrm{i}}^{k}Sy\right)\right)}^2$$
12	11	oveq1d	$$⊢x=A\to \frac{\sum _{k=1}^4{\mathrm{i}}^k{N\left(xG\left({\mathrm{i}}^{k}Sy\right)\right)}^2}{4}=\frac{\sum _{k=1}^4{\mathrm{i}}^k{N\left(AG\left({\mathrm{i}}^{k}Sy\right)\right)}^2}{4}$$
13		oveq2	$$⊢y=B\to {\mathrm{i}}^{k}Sy={\mathrm{i}}^{k}SB$$
14	13	oveq2d	$$⊢y=B\to AG\left({\mathrm{i}}^{k}Sy\right)=AG\left({\mathrm{i}}^{k}SB\right)$$
15	14	fveq2d	$$⊢y=B\to N\left(AG\left({\mathrm{i}}^{k}Sy\right)\right)=N\left(AG\left({\mathrm{i}}^{k}SB\right)\right)$$
16	15	oveq1d	$$⊢y=B\to {N\left(AG\left({\mathrm{i}}^{k}Sy\right)\right)}^2={N\left(AG\left({\mathrm{i}}^{k}SB\right)\right)}^2$$
17	16	oveq2d	$$⊢y=B\to {\mathrm{i}}^k{N\left(AG\left({\mathrm{i}}^{k}Sy\right)\right)}^2={\mathrm{i}}^k{N\left(AG\left({\mathrm{i}}^{k}SB\right)\right)}^2$$
18	17	sumeq2sdv	$$⊢y=B\to \sum _{k=1}^4{\mathrm{i}}^k{N\left(AG\left({\mathrm{i}}^{k}Sy\right)\right)}^2=\sum _{k=1}^4{\mathrm{i}}^k{N\left(AG\left({\mathrm{i}}^{k}SB\right)\right)}^2$$
19	18	oveq1d	$$⊢y=B\to \frac{\sum _{k=1}^4{\mathrm{i}}^k{N\left(AG\left({\mathrm{i}}^{k}Sy\right)\right)}^2}{4}=\frac{\sum _{k=1}^4{\mathrm{i}}^k{N\left(AG\left({\mathrm{i}}^{k}SB\right)\right)}^2}{4}$$
20		eqid	$$⊢\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)=\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)$$
21		ovex	$$⊢\frac{\sum _{k=1}^4{\mathrm{i}}^k{N\left(AG\left({\mathrm{i}}^{k}SB\right)\right)}^2}{4}\in \mathrm{V}$$
22	12 19 20 21	ovmpo	$$⊢\left(A\in X\wedge B\in X\right)\to A\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)B=\frac{\sum _{k=1}^4{\mathrm{i}}^k{N\left(AG\left({\mathrm{i}}^{k}SB\right)\right)}^2}{4}$$
23	7 22	sylan9eq	$$⊢\left(U\in \mathrm{NrmCVec}\wedge \left(A\in X\wedge B\in X\right)\right)\to APB=\frac{\sum _{k=1}^4{\mathrm{i}}^k{N\left(AG\left({\mathrm{i}}^{k}SB\right)\right)}^2}{4}$$
24	23	3impb	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\wedge B\in X\right)\to APB=\frac{\sum _{k=1}^4{\mathrm{i}}^k{N\left(AG\left({\mathrm{i}}^{k}SB\right)\right)}^2}{4}$$