Theorem dipcl

Description: An inner product is a complex number. (Contributed by NM, 1-Feb-2007) (Revised by Mario Carneiro, 5-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ipcl.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	ipcl.7	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
Assertion	dipcl	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\wedge B\in X\right)\to APB\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		ipcl.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		ipcl.7	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
3		eqid	$$⊢{+}_v\left(U\right)={+}_v\left(U\right)$$
4		eqid	$$⊢{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
5		eqid	$$⊢{norm}_{CV}\left(U\right)={norm}_{CV}\left(U\right)$$
6	1 3 4 5 2	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{{norm}_{CV}\left(U\right)\left(A{+}_v\left(U\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)B\right)\right)}^2}{4}$$
7		fzfid	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\wedge B\in X\right)\to \left(1\dots 4\right)\in \mathrm{Fin}$$
8		ax-icn	$$⊢\mathrm{i}\in ℂ$$
9		elfznn	$$⊢k\in \left(1\dots 4\right)\to k\in \mathbb{N}$$
10	9	nnnn0d	$$⊢k\in \left(1\dots 4\right)\to k\in {\mathbb{N}}_0$$
11		expcl	$$⊢\left(\mathrm{i}\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{i}}^k\in ℂ$$
12	8 10 11	sylancr	$$⊢k\in \left(1\dots 4\right)\to {\mathrm{i}}^k\in ℂ$$
13	12	adantl	$$⊢\left(\left(U\in \mathrm{NrmCVec}\wedge A\in X\wedge B\in X\right)\wedge k\in \left(1\dots 4\right)\right)\to {\mathrm{i}}^k\in ℂ$$
14	1 3 4 5 2	ipval2lem4	$$⊢\left(\left(U\in \mathrm{NrmCVec}\wedge A\in X\wedge B\in X\right)\wedge {\mathrm{i}}^k\in ℂ\right)\to {{norm}_{CV}\left(U\right)\left(A{+}_v\left(U\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)B\right)\right)}^2\in ℂ$$
15	12 14	sylan2	$$⊢\left(\left(U\in \mathrm{NrmCVec}\wedge A\in X\wedge B\in X\right)\wedge k\in \left(1\dots 4\right)\right)\to {{norm}_{CV}\left(U\right)\left(A{+}_v\left(U\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)B\right)\right)}^2\in ℂ$$
16	13 15	mulcld	$$⊢\left(\left(U\in \mathrm{NrmCVec}\wedge A\in X\wedge B\in X\right)\wedge k\in \left(1\dots 4\right)\right)\to {\mathrm{i}}^k{{norm}_{CV}\left(U\right)\left(A{+}_v\left(U\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)B\right)\right)}^2\in ℂ$$
17	7 16	fsumcl	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\wedge B\in X\right)\to \sum _{k=1}^4{\mathrm{i}}^k{{norm}_{CV}\left(U\right)\left(A{+}_v\left(U\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)B\right)\right)}^2\in ℂ$$
18		4cn	$$⊢4\in ℂ$$
19		4ne0	$$⊢4\ne 0$$
20		divcl	$$⊢\left(\sum _{k=1}^4{\mathrm{i}}^k{{norm}_{CV}\left(U\right)\left(A{+}_v\left(U\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)B\right)\right)}^2\in ℂ\wedge 4\in ℂ\wedge 4\ne 0\right)\to \frac{\sum _{k=1}^4{\mathrm{i}}^k{{norm}_{CV}\left(U\right)\left(A{+}_v\left(U\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)B\right)\right)}^2}{4}\in ℂ$$
21	18 19 20	mp3an23	$$⊢\sum _{k=1}^4{\mathrm{i}}^k{{norm}_{CV}\left(U\right)\left(A{+}_v\left(U\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)B\right)\right)}^2\in ℂ\to \frac{\sum _{k=1}^4{\mathrm{i}}^k{{norm}_{CV}\left(U\right)\left(A{+}_v\left(U\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)B\right)\right)}^2}{4}\in ℂ$$
22	17 21	syl	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\wedge B\in X\right)\to \frac{\sum _{k=1}^4{\mathrm{i}}^k{{norm}_{CV}\left(U\right)\left(A{+}_v\left(U\right)\left({\mathrm{i}}^k{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)B\right)\right)}^2}{4}\in ℂ$$
23	6 22	eqeltrd	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\wedge B\in X\right)\to APB\in ℂ$$