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	eqtrid	⊢ ( ( 𝑈 ∈ 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 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) = ( 𝐵 𝑃 𝐴 ) )