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	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	ipcl.7	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
Assertion	dipcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		ipcl.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		ipcl.7	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
3		eqid	⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
4		eqid	⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
5		eqid	⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
6	1 3 4 5 2	ipval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) = ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) / 4 ) )
7		fzfid	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 1 ... 4 ) ∈ Fin )
8		ax-icn	⊢ i ∈ ℂ
9		elfznn	⊢ ( 𝑘 ∈ ( 1 ... 4 ) → 𝑘 ∈ ℕ )
10	9	nnnn0d	⊢ ( 𝑘 ∈ ( 1 ... 4 ) → 𝑘 ∈ ℕ0 )
11		expcl	⊢ ( ( i ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( i ↑ 𝑘 ) ∈ ℂ )
12	8 10 11	sylancr	⊢ ( 𝑘 ∈ ( 1 ... 4 ) → ( i ↑ 𝑘 ) ∈ ℂ )
13	12	adantl	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ( 1 ... 4 ) ) → ( i ↑ 𝑘 ) ∈ ℂ )
14	1 3 4 5 2	ipval2lem4	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( i ↑ 𝑘 ) ∈ ℂ ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
15	12 14	sylan2	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ( 1 ... 4 ) ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
16	13 15	mulcld	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑘 ∈ ( 1 ... 4 ) ) → ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
17	7 16	fsumcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
18		4cn	⊢ 4 ∈ ℂ
19		4ne0	⊢ 4 ≠ 0
20		divcl	⊢ ( ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ ∧ 4 ∈ ℂ ∧ 4 ≠ 0 ) → ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) / 4 ) ∈ ℂ )
21	18 19 20	mp3an23	⊢ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ → ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) / 4 ) ∈ ℂ )
22	17 21	syl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) / 4 ) ∈ ℂ )
23	6 22	eqeltrd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )