Metamath Proof Explorer

Theorem dipcj

Description: The complex conjugate of an inner product reverses its arguments. Equation I1 of Ponnusamy p. 362. (Contributed by NM, 1-Feb-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ipcl.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
ipcl.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
Assertion dipcj ( ( 𝑈 ∈ 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 ipval2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) = ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) )
7 6 fveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) = ( ∗ ‘ ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) ) )
8 1 3 4 5 2 ipval2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 𝑃 𝐴 ) = ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) 𝐴 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) ) ) / 4 ) )
9 8 3com23 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝑃 𝐴 ) = ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) 𝐴 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) ) ) / 4 ) )
10 1 3 4 5 2 ipval2lem3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) ∈ ℝ )
11 10 recnd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) ∈ ℂ )
12 neg1cn ⊢ - 1 ∈ ℂ
13 1 3 4 5 2 ipval2lem4 ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ - 1 ∈ ℂ ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
14 12 13 mpan2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
15 11 14 subcld ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
16 ax-icn ⊢ i ∈ ℂ
17 1 3 4 5 2 ipval2lem4 ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ i ∈ ℂ ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
18 16 17 mpan2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
19 negicn ⊢ - i ∈ ℂ
20 1 3 4 5 2 ipval2lem4 ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ - i ∈ ℂ ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
21 19 20 mpan2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ∈ ℂ )
22 18 21 subcld ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ )
23 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ ) → ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ∈ ℂ )
24 16 22 23 sylancr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ∈ ℂ )
25 15 24 addcld ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) ∈ ℂ )
26 4cn ⊢ 4 ∈ ℂ
27 4ne0 ⊢ 4 ≠ 0
28 cjdiv ⊢ ( ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) ∈ ℂ ∧ 4 ∈ ℂ ∧ 4 ≠ 0 ) → ( ∗ ‘ ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) ) = ( ( ∗ ‘ ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) ) / ( ∗ ‘ 4 ) ) )
29 26 27 28 mp3an23 ⊢ ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) ∈ ℂ → ( ∗ ‘ ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) ) = ( ( ∗ ‘ ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) ) / ( ∗ ‘ 4 ) ) )
30 25 29 syl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∗ ‘ ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) ) = ( ( ∗ ‘ ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) ) / ( ∗ ‘ 4 ) ) )
31 4re ⊢ 4 ∈ ℝ
32 cjre ⊢ ( 4 ∈ ℝ → ( ∗ ‘ 4 ) = 4 )
33 31 32 ax-mp ⊢ ( ∗ ‘ 4 ) = 4
34 33 oveq2i ⊢ ( ( ∗ ‘ ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) ) / ( ∗ ‘ 4 ) ) = ( ( ∗ ‘ ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) ) / 4 )
35 1 3 4 5 2 ipval2lem2 ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ - 1 ∈ ℂ ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ∈ ℝ )
36 12 35 mpan2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ∈ ℝ )
37 10 36 resubcld ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ∈ ℝ )
38 1 3 4 5 2 ipval2lem2 ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ i ∈ ℂ ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ∈ ℝ )
39 16 38 mpan2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ∈ ℝ )
40 1 3 4 5 2 ipval2lem2 ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ - i ∈ ℂ ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ∈ ℝ )
41 19 40 mpan2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ∈ ℝ )
42 39 41 resubcld ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ∈ ℝ )
43 cjreim ⊢ ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ∈ ℝ ∧ ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ∈ ℝ ) → ( ∗ ‘ ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) ) = ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) − ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) )
44 37 42 43 syl2anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∗ ‘ ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) ) = ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) − ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) )
45 submul2 ⊢ ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ ∧ i ∈ ℂ ∧ ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ ) → ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) − ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) = ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · - ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) )
46 16 45 mp3an2 ⊢ ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ ∧ ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ∈ ℂ ) → ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) − ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) = ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · - ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) )
47 15 22 46 syl2anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) − ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) = ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · - ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) )
48 1 3 nvcom ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) = ( 𝐵 ( +𝑣 ‘ 𝑈 ) 𝐴 ) )
49 48 fveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) 𝐴 ) ) )
50 49 oveq1d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) = ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) 𝐴 ) ) ↑ 2 ) )
51 1 3 4 5 nvdif ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) )
52 51 oveq1d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) = ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) )
53 50 52 oveq12d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) = ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) 𝐴 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) )
54 18 21 negsubdi2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → - ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) = ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) )
55 1 3 4 5 nvpi ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) )
56 55 3com23 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) )
57 56 eqcomd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) )
58 57 oveq1d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) = ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) )
59 1 3 4 5 nvpi ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) )
60 59 oveq1d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) = ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) )
61 58 60 oveq12d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) = ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) )
62 54 61 eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → - ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) = ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) )
63 62 oveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( i · - ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) = ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) ) )
64 53 63 oveq12d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · - ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) = ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) 𝐴 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) ) ) )
65 44 47 64 3eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∗ ‘ ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) ) = ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) 𝐴 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) ) ) )
66 65 oveq1d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ∗ ‘ ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) ) / 4 ) = ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) 𝐴 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) ) ) / 4 ) )
67 34 66 syl5eq ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ∗ ‘ ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) ) / ( ∗ ‘ 4 ) ) = ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) 𝐴 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) ) ) / 4 ) )
68 30 67 eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∗ ‘ ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) ) = ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) 𝐴 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐵 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ↑ 2 ) ) ) ) / 4 ) )
69 9 68 eqtr4d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝑃 𝐴 ) = ( ∗ ‘ ( ( ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) + ( i · ( ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) − ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - i ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ↑ 2 ) ) ) ) / 4 ) ) )
70 7 69 eqtr4d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) = ( 𝐵 𝑃 𝐴 ) )