Metamath Proof Explorer

Theorem ipasslem10

Description: Lemma for ipassi . Show the inner product associative law for the imaginary number _i . (Contributed by NM, 24-Aug-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ip1i.1 
|- X = ( BaseSet ` U )
ip1i.2 
|- G = ( +v ` U )
ip1i.4 
|- S = ( .sOLD ` U )
ip1i.7 
|- P = ( .iOLD ` U )
ip1i.9 
|- U e. CPreHilOLD
ipasslem10.a 
|- A e. X
ipasslem10.b 
|- B e. X
ipasslem10.6 
|- N = ( normCV ` U )
Assertion ipasslem10 
|- ( ( _i S A ) P B ) = ( _i x. ( A P B ) )

Proof

Step Hyp Ref Expression
1 ip1i.1 
 |-  X = ( BaseSet ` U )
2 ip1i.2 
 |-  G = ( +v ` U )
3 ip1i.4 
 |-  S = ( .sOLD ` U )
4 ip1i.7 
 |-  P = ( .iOLD ` U )
5 ip1i.9 
 |-  U e. CPreHilOLD
6 ipasslem10.a 
 |-  A e. X
7 ipasslem10.b 
 |-  B e. X
8 ipasslem10.6 
 |-  N = ( normCV ` U )
9 5 phnvi 
 |-  U e. NrmCVec
10 ax-icn 
 |-  _i e. CC
11 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ _i e. CC /\ A e. X ) -> ( _i S A ) e. X )
12 9 10 6 11 mp3an 
 |-  ( _i S A ) e. X
13 1 2 3 8 4 4ipval2 
 |-  ( ( U e. NrmCVec /\ B e. X /\ ( _i S A ) e. X ) -> ( 4 x. ( B P ( _i S A ) ) ) = ( ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( B G ( _i S ( _i S A ) ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) ^ 2 ) ) ) ) )
14 9 7 12 13 mp3an 
 |-  ( 4 x. ( B P ( _i S A ) ) ) = ( ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( B G ( _i S ( _i S A ) ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) ^ 2 ) ) ) )
15 4cn 
 |-  4 e. CC
16 negicn 
 |-  -u _i e. CC
17 1 4 dipcl 
 |-  ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( B P A ) e. CC )
18 9 7 6 17 mp3an 
 |-  ( B P A ) e. CC
19 15 16 18 mul12i 
 |-  ( 4 x. ( -u _i x. ( B P A ) ) ) = ( -u _i x. ( 4 x. ( B P A ) ) )
20 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ B e. X /\ ( _i S A ) e. X ) -> ( B G ( _i S A ) ) e. X )
21 9 7 12 20 mp3an 
 |-  ( B G ( _i S A ) ) e. X
22 1 8 9 21 nvcli 
 |-  ( N ` ( B G ( _i S A ) ) ) e. RR
23 22 recni 
 |-  ( N ` ( B G ( _i S A ) ) ) e. CC
24 23 sqcli 
 |-  ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) e. CC
25 neg1cn 
 |-  -u 1 e. CC
26 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ ( _i S A ) e. X ) -> ( -u 1 S ( _i S A ) ) e. X )
27 9 25 12 26 mp3an 
 |-  ( -u 1 S ( _i S A ) ) e. X
28 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ B e. X /\ ( -u 1 S ( _i S A ) ) e. X ) -> ( B G ( -u 1 S ( _i S A ) ) ) e. X )
29 9 7 27 28 mp3an 
 |-  ( B G ( -u 1 S ( _i S A ) ) ) e. X
30 1 8 9 29 nvcli 
 |-  ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) e. RR
31 30 recni 
 |-  ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) e. CC
32 31 sqcli 
 |-  ( ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) ^ 2 ) e. CC
33 24 32 subcli 
 |-  ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) ^ 2 ) ) e. CC
34 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ _i e. CC /\ ( _i S A ) e. X ) -> ( _i S ( _i S A ) ) e. X )
35 9 10 12 34 mp3an 
 |-  ( _i S ( _i S A ) ) e. X
36 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ B e. X /\ ( _i S ( _i S A ) ) e. X ) -> ( B G ( _i S ( _i S A ) ) ) e. X )
37 9 7 35 36 mp3an 
 |-  ( B G ( _i S ( _i S A ) ) ) e. X
38 1 8 9 37 nvcli 
 |-  ( N ` ( B G ( _i S ( _i S A ) ) ) ) e. RR
39 38 recni 
 |-  ( N ` ( B G ( _i S ( _i S A ) ) ) ) e. CC
40 39 sqcli 
 |-  ( ( N ` ( B G ( _i S ( _i S A ) ) ) ) ^ 2 ) e. CC
41 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ -u _i e. CC /\ ( _i S A ) e. X ) -> ( -u _i S ( _i S A ) ) e. X )
42 9 16 12 41 mp3an 
 |-  ( -u _i S ( _i S A ) ) e. X
43 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ B e. X /\ ( -u _i S ( _i S A ) ) e. X ) -> ( B G ( -u _i S ( _i S A ) ) ) e. X )
44 9 7 42 43 mp3an 
 |-  ( B G ( -u _i S ( _i S A ) ) ) e. X
45 1 8 9 44 nvcli 
 |-  ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) e. RR
46 45 recni 
 |-  ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) e. CC
47 46 sqcli 
 |-  ( ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) ^ 2 ) e. CC
48 40 47 subcli 
 |-  ( ( ( N ` ( B G ( _i S ( _i S A ) ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) ^ 2 ) ) e. CC
49 10 48 mulcli 
 |-  ( _i x. ( ( ( N ` ( B G ( _i S ( _i S A ) ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) ^ 2 ) ) ) e. CC
50 33 49 addcomi 
 |-  ( ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( B G ( _i S ( _i S A ) ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) ^ 2 ) ) ) ) = ( ( _i x. ( ( ( N ` ( B G ( _i S ( _i S A ) ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) ^ 2 ) ) ) + ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) ^ 2 ) ) )
51 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( B G A ) e. X )
52 9 7 6 51 mp3an 
 |-  ( B G A ) e. X
53 1 8 9 52 nvcli 
 |-  ( N ` ( B G A ) ) e. RR
54 53 recni 
 |-  ( N ` ( B G A ) ) e. CC
55 54 sqcli 
 |-  ( ( N ` ( B G A ) ) ^ 2 ) e. CC
56 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ A e. X ) -> ( -u 1 S A ) e. X )
57 9 25 6 56 mp3an 
 |-  ( -u 1 S A ) e. X
58 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ B e. X /\ ( -u 1 S A ) e. X ) -> ( B G ( -u 1 S A ) ) e. X )
59 9 7 57 58 mp3an 
 |-  ( B G ( -u 1 S A ) ) e. X
60 1 8 9 59 nvcli 
 |-  ( N ` ( B G ( -u 1 S A ) ) ) e. RR
61 60 recni 
 |-  ( N ` ( B G ( -u 1 S A ) ) ) e. CC
62 61 sqcli 
 |-  ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) e. CC
63 55 62 subcli 
 |-  ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) e. CC
64 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ -u _i e. CC /\ A e. X ) -> ( -u _i S A ) e. X )
65 9 16 6 64 mp3an 
 |-  ( -u _i S A ) e. X
66 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ B e. X /\ ( -u _i S A ) e. X ) -> ( B G ( -u _i S A ) ) e. X )
67 9 7 65 66 mp3an 
 |-  ( B G ( -u _i S A ) ) e. X
68 1 8 9 67 nvcli 
 |-  ( N ` ( B G ( -u _i S A ) ) ) e. RR
69 68 recni 
 |-  ( N ` ( B G ( -u _i S A ) ) ) e. CC
70 69 sqcli 
 |-  ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) e. CC
71 24 70 subcli 
 |-  ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) e. CC
72 10 71 mulcli 
 |-  ( _i x. ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) ) e. CC
73 16 63 72 adddii 
 |-  ( -u _i x. ( ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) ) ) ) = ( ( -u _i x. ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) ) + ( -u _i x. ( _i x. ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) ) ) )
74 10 10 6 3pm3.2i 
 |-  ( _i e. CC /\ _i e. CC /\ A e. X )
75 1 3 nvsass 
 |-  ( ( U e. NrmCVec /\ ( _i e. CC /\ _i e. CC /\ A e. X ) ) -> ( ( _i x. _i ) S A ) = ( _i S ( _i S A ) ) )
76 9 74 75 mp2an 
 |-  ( ( _i x. _i ) S A ) = ( _i S ( _i S A ) )
77 ixi 
 |-  ( _i x. _i ) = -u 1
78 77 oveq1i 
 |-  ( ( _i x. _i ) S A ) = ( -u 1 S A )
79 76 78 eqtr3i 
 |-  ( _i S ( _i S A ) ) = ( -u 1 S A )
80 79 oveq2i 
 |-  ( B G ( _i S ( _i S A ) ) ) = ( B G ( -u 1 S A ) )
81 80 fveq2i 
 |-  ( N ` ( B G ( _i S ( _i S A ) ) ) ) = ( N ` ( B G ( -u 1 S A ) ) )
82 81 oveq1i 
 |-  ( ( N ` ( B G ( _i S ( _i S A ) ) ) ) ^ 2 ) = ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 )
83 10 10 mulneg1i 
 |-  ( -u _i x. _i ) = -u ( _i x. _i )
84 77 negeqi 
 |-  -u ( _i x. _i ) = -u -u 1
85 negneg1e1 
 |-  -u -u 1 = 1
86 83 84 85 3eqtri 
 |-  ( -u _i x. _i ) = 1
87 86 oveq1i 
 |-  ( ( -u _i x. _i ) S A ) = ( 1 S A )
88 16 10 6 3pm3.2i 
 |-  ( -u _i e. CC /\ _i e. CC /\ A e. X )
89 1 3 nvsass 
 |-  ( ( U e. NrmCVec /\ ( -u _i e. CC /\ _i e. CC /\ A e. X ) ) -> ( ( -u _i x. _i ) S A ) = ( -u _i S ( _i S A ) ) )
90 9 88 89 mp2an 
 |-  ( ( -u _i x. _i ) S A ) = ( -u _i S ( _i S A ) )
91 1 3 nvsid 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( 1 S A ) = A )
92 9 6 91 mp2an 
 |-  ( 1 S A ) = A
93 87 90 92 3eqtr3i 
 |-  ( -u _i S ( _i S A ) ) = A
94 93 oveq2i 
 |-  ( B G ( -u _i S ( _i S A ) ) ) = ( B G A )
95 94 fveq2i 
 |-  ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) = ( N ` ( B G A ) )
96 95 oveq1i 
 |-  ( ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) ^ 2 ) = ( ( N ` ( B G A ) ) ^ 2 )
97 82 96 oveq12i 
 |-  ( ( ( N ` ( B G ( _i S ( _i S A ) ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) ^ 2 ) ) = ( ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) - ( ( N ` ( B G A ) ) ^ 2 ) )
98 97 oveq2i 
 |-  ( _i x. ( ( ( N ` ( B G ( _i S ( _i S A ) ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) ^ 2 ) ) ) = ( _i x. ( ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) - ( ( N ` ( B G A ) ) ^ 2 ) ) )
99 63 mulm1i 
 |-  ( -u 1 x. ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) ) = -u ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) )
100 55 62 negsubdi2i 
 |-  -u ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) = ( ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) - ( ( N ` ( B G A ) ) ^ 2 ) )
101 99 100 eqtr2i 
 |-  ( ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) - ( ( N ` ( B G A ) ) ^ 2 ) ) = ( -u 1 x. ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) )
102 101 oveq2i 
 |-  ( _i x. ( ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) - ( ( N ` ( B G A ) ) ^ 2 ) ) ) = ( _i x. ( -u 1 x. ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) ) )
103 10 25 63 mulassi 
 |-  ( ( _i x. -u 1 ) x. ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) ) = ( _i x. ( -u 1 x. ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) ) )
104 102 103 eqtr4i 
 |-  ( _i x. ( ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) - ( ( N ` ( B G A ) ) ^ 2 ) ) ) = ( ( _i x. -u 1 ) x. ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) )
105 10 mulm1i 
 |-  ( -u 1 x. _i ) = -u _i
106 25 10 105 mulcomli 
 |-  ( _i x. -u 1 ) = -u _i
107 106 oveq1i 
 |-  ( ( _i x. -u 1 ) x. ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) ) = ( -u _i x. ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) )
108 98 104 107 3eqtri 
 |-  ( _i x. ( ( ( N ` ( B G ( _i S ( _i S A ) ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) ^ 2 ) ) ) = ( -u _i x. ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) )
109 25 10 6 3pm3.2i 
 |-  ( -u 1 e. CC /\ _i e. CC /\ A e. X )
110 1 3 nvsass 
 |-  ( ( U e. NrmCVec /\ ( -u 1 e. CC /\ _i e. CC /\ A e. X ) ) -> ( ( -u 1 x. _i ) S A ) = ( -u 1 S ( _i S A ) ) )
111 9 109 110 mp2an 
 |-  ( ( -u 1 x. _i ) S A ) = ( -u 1 S ( _i S A ) )
112 105 oveq1i 
 |-  ( ( -u 1 x. _i ) S A ) = ( -u _i S A )
113 111 112 eqtr3i 
 |-  ( -u 1 S ( _i S A ) ) = ( -u _i S A )
114 113 oveq2i 
 |-  ( B G ( -u 1 S ( _i S A ) ) ) = ( B G ( -u _i S A ) )
115 114 fveq2i 
 |-  ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) = ( N ` ( B G ( -u _i S A ) ) )
116 115 oveq1i 
 |-  ( ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) ^ 2 ) = ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 )
117 116 oveq2i 
 |-  ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) ^ 2 ) ) = ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) )
118 71 mullidi 
 |-  ( 1 x. ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) ) = ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) )
119 117 118 eqtr4i 
 |-  ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) ^ 2 ) ) = ( 1 x. ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) )
120 86 oveq1i 
 |-  ( ( -u _i x. _i ) x. ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) ) = ( 1 x. ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) )
121 119 120 eqtr4i 
 |-  ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) ^ 2 ) ) = ( ( -u _i x. _i ) x. ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) )
122 16 10 71 mulassi 
 |-  ( ( -u _i x. _i ) x. ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) ) = ( -u _i x. ( _i x. ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) ) )
123 121 122 eqtri 
 |-  ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) ^ 2 ) ) = ( -u _i x. ( _i x. ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) ) )
124 108 123 oveq12i 
 |-  ( ( _i x. ( ( ( N ` ( B G ( _i S ( _i S A ) ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) ^ 2 ) ) ) + ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) ^ 2 ) ) ) = ( ( -u _i x. ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) ) + ( -u _i x. ( _i x. ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) ) ) )
125 73 124 eqtr4i 
 |-  ( -u _i x. ( ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) ) ) ) = ( ( _i x. ( ( ( N ` ( B G ( _i S ( _i S A ) ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) ^ 2 ) ) ) + ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) ^ 2 ) ) )
126 50 125 eqtr4i 
 |-  ( ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( B G ( _i S ( _i S A ) ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) ^ 2 ) ) ) ) = ( -u _i x. ( ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) ) ) )
127 1 2 3 8 4 4ipval2 
 |-  ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( 4 x. ( B P A ) ) = ( ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) ) ) )
128 9 7 6 127 mp3an 
 |-  ( 4 x. ( B P A ) ) = ( ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) ) )
129 128 oveq2i 
 |-  ( -u _i x. ( 4 x. ( B P A ) ) ) = ( -u _i x. ( ( ( ( N ` ( B G A ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S A ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S A ) ) ) ^ 2 ) ) ) ) )
130 126 129 eqtr4i 
 |-  ( ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( B G ( _i S ( _i S A ) ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) ^ 2 ) ) ) ) = ( -u _i x. ( 4 x. ( B P A ) ) )
131 19 130 eqtr4i 
 |-  ( 4 x. ( -u _i x. ( B P A ) ) ) = ( ( ( ( N ` ( B G ( _i S A ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u 1 S ( _i S A ) ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( B G ( _i S ( _i S A ) ) ) ) ^ 2 ) - ( ( N ` ( B G ( -u _i S ( _i S A ) ) ) ) ^ 2 ) ) ) )
132 14 131 eqtr4i 
 |-  ( 4 x. ( B P ( _i S A ) ) ) = ( 4 x. ( -u _i x. ( B P A ) ) )
133 1 4 dipcl 
 |-  ( ( U e. NrmCVec /\ B e. X /\ ( _i S A ) e. X ) -> ( B P ( _i S A ) ) e. CC )
134 9 7 12 133 mp3an 
 |-  ( B P ( _i S A ) ) e. CC
135 16 18 mulcli 
 |-  ( -u _i x. ( B P A ) ) e. CC
136 4ne0 
 |-  4 =/= 0
137 134 135 15 136 mulcani 
 |-  ( ( 4 x. ( B P ( _i S A ) ) ) = ( 4 x. ( -u _i x. ( B P A ) ) ) <-> ( B P ( _i S A ) ) = ( -u _i x. ( B P A ) ) )
138 132 137 mpbi 
 |-  ( B P ( _i S A ) ) = ( -u _i x. ( B P A ) )
139 138 fveq2i 
 |-  ( * ` ( B P ( _i S A ) ) ) = ( * ` ( -u _i x. ( B P A ) ) )
140 1 4 dipcj 
 |-  ( ( U e. NrmCVec /\ B e. X /\ ( _i S A ) e. X ) -> ( * ` ( B P ( _i S A ) ) ) = ( ( _i S A ) P B ) )
141 9 7 12 140 mp3an 
 |-  ( * ` ( B P ( _i S A ) ) ) = ( ( _i S A ) P B )
142 16 18 cjmuli 
 |-  ( * ` ( -u _i x. ( B P A ) ) ) = ( ( * ` -u _i ) x. ( * ` ( B P A ) ) )
143 25 10 cjmuli 
 |-  ( * ` ( -u 1 x. _i ) ) = ( ( * ` -u 1 ) x. ( * ` _i ) )
144 105 fveq2i 
 |-  ( * ` ( -u 1 x. _i ) ) = ( * ` -u _i )
145 neg1rr 
 |-  -u 1 e. RR
146 25 cjrebi 
 |-  ( -u 1 e. RR <-> ( * ` -u 1 ) = -u 1 )
147 145 146 mpbi 
 |-  ( * ` -u 1 ) = -u 1
148 cji 
 |-  ( * ` _i ) = -u _i
149 147 148 oveq12i 
 |-  ( ( * ` -u 1 ) x. ( * ` _i ) ) = ( -u 1 x. -u _i )
150 ax-1cn 
 |-  1 e. CC
151 150 10 mul2negi 
 |-  ( -u 1 x. -u _i ) = ( 1 x. _i )
152 10 mullidi 
 |-  ( 1 x. _i ) = _i
153 149 151 152 3eqtri 
 |-  ( ( * ` -u 1 ) x. ( * ` _i ) ) = _i
154 143 144 153 3eqtr3i 
 |-  ( * ` -u _i ) = _i
155 1 4 dipcj 
 |-  ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( * ` ( B P A ) ) = ( A P B ) )
156 9 7 6 155 mp3an 
 |-  ( * ` ( B P A ) ) = ( A P B )
157 154 156 oveq12i 
 |-  ( ( * ` -u _i ) x. ( * ` ( B P A ) ) ) = ( _i x. ( A P B ) )
158 142 157 eqtri 
 |-  ( * ` ( -u _i x. ( B P A ) ) ) = ( _i x. ( A P B ) )
159 139 141 158 3eqtr3i 
 |-  ( ( _i S A ) P B ) = ( _i x. ( A P B ) )