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 
|- X = ( BaseSet ` U )
ipcl.7 
|- P = ( .iOLD ` U )
Assertion dipcj 
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( * ` ( A P B ) ) = ( B P A ) )

Proof

Step Hyp Ref Expression
1 ipcl.1 
 |-  X = ( BaseSet ` U )
2 ipcl.7 
 |-  P = ( .iOLD ` U )
3 eqid 
 |-  ( +v ` U ) = ( +v ` U )
4 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
5 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
6 1 3 4 5 2 ipval2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) = ( ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) / 4 ) )
7 6 fveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( * ` ( A P B ) ) = ( * ` ( ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) / 4 ) ) )
8 1 3 4 5 2 ipval2 
 |-  ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( B P A ) = ( ( ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) A ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( _i ( .sOLD ` U ) A ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u _i ( .sOLD ` U ) A ) ) ) ^ 2 ) ) ) ) / 4 ) )
9 8 3com23 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( B P A ) = ( ( ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) A ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( _i ( .sOLD ` U ) A ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u _i ( .sOLD ` U ) A ) ) ) ^ 2 ) ) ) ) / 4 ) )
10 1 3 4 5 2 ipval2lem3 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) e. RR )
11 10 recnd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) e. CC )
12 neg1cn 
 |-  -u 1 e. CC
13 1 3 4 5 2 ipval2lem4 
 |-  ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ -u 1 e. CC ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) e. CC )
14 12 13 mpan2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) e. CC )
15 11 14 subcld 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) e. CC )
16 ax-icn 
 |-  _i e. CC
17 1 3 4 5 2 ipval2lem4 
 |-  ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ _i e. CC ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) e. CC )
18 16 17 mpan2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) e. CC )
19 negicn 
 |-  -u _i e. CC
20 1 3 4 5 2 ipval2lem4 
 |-  ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ -u _i e. CC ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) e. CC )
21 19 20 mpan2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) e. CC )
22 18 21 subcld 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) e. CC )
23 mulcl 
 |-  ( ( _i e. CC /\ ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) e. CC ) -> ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) e. CC )
24 16 22 23 sylancr 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) e. CC )
25 15 24 addcld 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) e. CC )
26 4cn 
 |-  4 e. CC
27 4ne0 
 |-  4 =/= 0
28 cjdiv 
 |-  ( ( ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) e. CC /\ 4 e. CC /\ 4 =/= 0 ) -> ( * ` ( ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) / 4 ) ) = ( ( * ` ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) ) / ( * ` 4 ) ) )
29 26 27 28 mp3an23 
 |-  ( ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) e. CC -> ( * ` ( ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) / 4 ) ) = ( ( * ` ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) ) / ( * ` 4 ) ) )
30 25 29 syl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( * ` ( ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) / 4 ) ) = ( ( * ` ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) ) / ( * ` 4 ) ) )
31 4re 
 |-  4 e. RR
32 cjre 
 |-  ( 4 e. RR -> ( * ` 4 ) = 4 )
33 31 32 ax-mp 
 |-  ( * ` 4 ) = 4
34 33 oveq2i 
 |-  ( ( * ` ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) ) / ( * ` 4 ) ) = ( ( * ` ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) ) / 4 )
35 1 3 4 5 2 ipval2lem2 
 |-  ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ -u 1 e. CC ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) e. RR )
36 12 35 mpan2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) e. RR )
37 10 36 resubcld 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) e. RR )
38 1 3 4 5 2 ipval2lem2 
 |-  ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ _i e. CC ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) e. RR )
39 16 38 mpan2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) e. RR )
40 1 3 4 5 2 ipval2lem2 
 |-  ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ -u _i e. CC ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) e. RR )
41 19 40 mpan2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) e. RR )
42 39 41 resubcld 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) e. RR )
43 cjreim 
 |-  ( ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) e. RR /\ ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) e. RR ) -> ( * ` ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) ) = ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) - ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) )
44 37 42 43 syl2anc 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( * ` ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) ) = ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) - ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) )
45 submul2 
 |-  ( ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) e. CC /\ _i e. CC /\ ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) e. CC ) -> ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) - ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) = ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. -u ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) )
46 16 45 mp3an2 
 |-  ( ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) e. CC /\ ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) e. CC ) -> ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) - ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) = ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. -u ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) )
47 15 22 46 syl2anc 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) - ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) = ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. -u ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) )
48 1 3 nvcom 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A ( +v ` U ) B ) = ( B ( +v ` U ) A ) )
49 48 fveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) = ( ( normCV ` U ) ` ( B ( +v ` U ) A ) ) )
50 49 oveq1d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) = ( ( ( normCV ` U ) ` ( B ( +v ` U ) A ) ) ^ 2 ) )
51 1 3 4 5 nvdif 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) = ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) ) )
52 51 oveq1d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) = ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) ) ^ 2 ) )
53 50 52 oveq12d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) = ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) A ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) ) ^ 2 ) ) )
54 18 21 negsubdi2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> -u ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) = ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) )
55 1 3 4 5 nvpi 
 |-  ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( ( normCV ` U ) ` ( B ( +v ` U ) ( _i ( .sOLD ` U ) A ) ) ) = ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) )
56 55 3com23 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( normCV ` U ) ` ( B ( +v ` U ) ( _i ( .sOLD ` U ) A ) ) ) = ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) )
57 56 eqcomd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) = ( ( normCV ` U ) ` ( B ( +v ` U ) ( _i ( .sOLD ` U ) A ) ) ) )
58 57 oveq1d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) = ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( _i ( .sOLD ` U ) A ) ) ) ^ 2 ) )
59 1 3 4 5 nvpi 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) = ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u _i ( .sOLD ` U ) A ) ) ) )
60 59 oveq1d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) = ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u _i ( .sOLD ` U ) A ) ) ) ^ 2 ) )
61 58 60 oveq12d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) = ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( _i ( .sOLD ` U ) A ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u _i ( .sOLD ` U ) A ) ) ) ^ 2 ) ) )
62 54 61 eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> -u ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) = ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( _i ( .sOLD ` U ) A ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u _i ( .sOLD ` U ) A ) ) ) ^ 2 ) ) )
63 62 oveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( _i x. -u ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) = ( _i x. ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( _i ( .sOLD ` U ) A ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u _i ( .sOLD ` U ) A ) ) ) ^ 2 ) ) ) )
64 53 63 oveq12d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. -u ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) = ( ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) A ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( _i ( .sOLD ` U ) A ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u _i ( .sOLD ` U ) A ) ) ) ^ 2 ) ) ) ) )
65 44 47 64 3eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( * ` ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) ) = ( ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) A ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( _i ( .sOLD ` U ) A ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u _i ( .sOLD ` U ) A ) ) ) ^ 2 ) ) ) ) )
66 65 oveq1d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( * ` ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) ) / 4 ) = ( ( ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) A ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( _i ( .sOLD ` U ) A ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u _i ( .sOLD ` U ) A ) ) ) ^ 2 ) ) ) ) / 4 ) )
67 34 66 syl5eq 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( * ` ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) ) / ( * ` 4 ) ) = ( ( ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) A ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( _i ( .sOLD ` U ) A ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u _i ( .sOLD ` U ) A ) ) ) ^ 2 ) ) ) ) / 4 ) )
68 30 67 eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( * ` ( ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) / 4 ) ) = ( ( ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) A ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( _i ( .sOLD ` U ) A ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( B ( +v ` U ) ( -u _i ( .sOLD ` U ) A ) ) ) ^ 2 ) ) ) ) / 4 ) )
69 9 68 eqtr4d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( B P A ) = ( * ` ( ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) B ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) B ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) B ) ) ) ^ 2 ) ) ) ) / 4 ) ) )
70 7 69 eqtr4d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( * ` ( A P B ) ) = ( B P A ) )