This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )