Metamath Proof Explorer

Theorem ip0i

Description: A slight variant of Equation 6.46 of Ponnusamy p. 362, where J is either 1 or -1 to represent +-1. (Contributed by NM, 23-Apr-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
ip1i.a 
|- A e. X
ip1i.b 
|- B e. X
ip1i.c 
|- C e. X
ip1i.6 
|- N = ( normCV ` U )
ip0i.j 
|- J e. CC
Assertion ip0i 
|- ( ( ( ( N ` ( ( A G B ) G ( J S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u J S C ) ) ) ^ 2 ) ) + ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( J S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u J S C ) ) ) ^ 2 ) ) ) = ( 2 x. ( ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) ) )

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 ip1i.a 
 |-  A e. X
7 ip1i.b 
 |-  B e. X
8 ip1i.c 
 |-  C e. X
9 ip1i.6 
 |-  N = ( normCV ` U )
10 ip0i.j 
 |-  J e. CC
11 2cn 
 |-  2 e. CC
12 5 phnvi 
 |-  U e. NrmCVec
13 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ J e. CC /\ C e. X ) -> ( J S C ) e. X )
14 12 10 8 13 mp3an 
 |-  ( J S C ) e. X
15 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ ( J S C ) e. X ) -> ( A G ( J S C ) ) e. X )
16 12 6 14 15 mp3an 
 |-  ( A G ( J S C ) ) e. X
17 1 9 12 16 nvcli 
 |-  ( N ` ( A G ( J S C ) ) ) e. RR
18 17 recni 
 |-  ( N ` ( A G ( J S C ) ) ) e. CC
19 18 sqcli 
 |-  ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) e. CC
20 10 negcli 
 |-  -u J e. CC
21 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ -u J e. CC /\ C e. X ) -> ( -u J S C ) e. X )
22 12 20 8 21 mp3an 
 |-  ( -u J S C ) e. X
23 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ ( -u J S C ) e. X ) -> ( A G ( -u J S C ) ) e. X )
24 12 6 22 23 mp3an 
 |-  ( A G ( -u J S C ) ) e. X
25 1 9 12 24 nvcli 
 |-  ( N ` ( A G ( -u J S C ) ) ) e. RR
26 25 recni 
 |-  ( N ` ( A G ( -u J S C ) ) ) e. CC
27 26 sqcli 
 |-  ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) e. CC
28 11 19 27 subdii 
 |-  ( 2 x. ( ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) ) ) = ( ( 2 x. ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) ) - ( 2 x. ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) ) )
29 11 19 mulcli 
 |-  ( 2 x. ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) ) e. CC
30 11 27 mulcli 
 |-  ( 2 x. ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) ) e. CC
31 1 9 12 7 nvcli 
 |-  ( N ` B ) e. RR
32 31 recni 
 |-  ( N ` B ) e. CC
33 32 sqcli 
 |-  ( ( N ` B ) ^ 2 ) e. CC
34 11 33 mulcli 
 |-  ( 2 x. ( ( N ` B ) ^ 2 ) ) e. CC
35 pnpcan2 
 |-  ( ( ( 2 x. ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) ) e. CC /\ ( 2 x. ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) ) e. CC /\ ( 2 x. ( ( N ` B ) ^ 2 ) ) e. CC ) -> ( ( ( 2 x. ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) ) + ( 2 x. ( ( N ` B ) ^ 2 ) ) ) - ( ( 2 x. ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) ) + ( 2 x. ( ( N ` B ) ^ 2 ) ) ) ) = ( ( 2 x. ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) ) - ( 2 x. ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) ) ) )
36 29 30 34 35 mp3an 
 |-  ( ( ( 2 x. ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) ) + ( 2 x. ( ( N ` B ) ^ 2 ) ) ) - ( ( 2 x. ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) ) + ( 2 x. ( ( N ` B ) ^ 2 ) ) ) ) = ( ( 2 x. ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) ) - ( 2 x. ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) ) )
37 28 36 eqtr4i 
 |-  ( 2 x. ( ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) ) ) = ( ( ( 2 x. ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) ) + ( 2 x. ( ( N ` B ) ^ 2 ) ) ) - ( ( 2 x. ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) ) + ( 2 x. ( ( N ` B ) ^ 2 ) ) ) )
38 eqid 
 |-  ( 1st ` U ) = ( 1st ` U )
39 38 nvvc 
 |-  ( U e. NrmCVec -> ( 1st ` U ) e. CVecOLD )
40 2 vafval 
 |-  G = ( 1st ` ( 1st ` U ) )
41 40 vcablo 
 |-  ( ( 1st ` U ) e. CVecOLD -> G e. AbelOp )
42 12 39 41 mp2b 
 |-  G e. AbelOp
43 6 7 14 3pm3.2i 
 |-  ( A e. X /\ B e. X /\ ( J S C ) e. X )
44 1 2 bafval 
 |-  X = ran G
45 44 ablo32 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ ( J S C ) e. X ) ) -> ( ( A G B ) G ( J S C ) ) = ( ( A G ( J S C ) ) G B ) )
46 42 43 45 mp2an 
 |-  ( ( A G B ) G ( J S C ) ) = ( ( A G ( J S C ) ) G B )
47 46 fveq2i 
 |-  ( N ` ( ( A G B ) G ( J S C ) ) ) = ( N ` ( ( A G ( J S C ) ) G B ) )
48 47 oveq1i 
 |-  ( ( N ` ( ( A G B ) G ( J S C ) ) ) ^ 2 ) = ( ( N ` ( ( A G ( J S C ) ) G B ) ) ^ 2 )
49 neg1cn 
 |-  -u 1 e. CC
50 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ B e. X ) -> ( -u 1 S B ) e. X )
51 12 49 7 50 mp3an 
 |-  ( -u 1 S B ) e. X
52 6 51 14 3pm3.2i 
 |-  ( A e. X /\ ( -u 1 S B ) e. X /\ ( J S C ) e. X )
53 44 ablo32 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ ( -u 1 S B ) e. X /\ ( J S C ) e. X ) ) -> ( ( A G ( -u 1 S B ) ) G ( J S C ) ) = ( ( A G ( J S C ) ) G ( -u 1 S B ) ) )
54 42 52 53 mp2an 
 |-  ( ( A G ( -u 1 S B ) ) G ( J S C ) ) = ( ( A G ( J S C ) ) G ( -u 1 S B ) )
55 54 fveq2i 
 |-  ( N ` ( ( A G ( -u 1 S B ) ) G ( J S C ) ) ) = ( N ` ( ( A G ( J S C ) ) G ( -u 1 S B ) ) )
56 55 oveq1i 
 |-  ( ( N ` ( ( A G ( -u 1 S B ) ) G ( J S C ) ) ) ^ 2 ) = ( ( N ` ( ( A G ( J S C ) ) G ( -u 1 S B ) ) ) ^ 2 )
57 48 56 oveq12i 
 |-  ( ( ( N ` ( ( A G B ) G ( J S C ) ) ) ^ 2 ) + ( ( N ` ( ( A G ( -u 1 S B ) ) G ( J S C ) ) ) ^ 2 ) ) = ( ( ( N ` ( ( A G ( J S C ) ) G B ) ) ^ 2 ) + ( ( N ` ( ( A G ( J S C ) ) G ( -u 1 S B ) ) ) ^ 2 ) )
58 1 2 3 9 phpar 
 |-  ( ( U e. CPreHilOLD /\ ( A G ( J S C ) ) e. X /\ B e. X ) -> ( ( ( N ` ( ( A G ( J S C ) ) G B ) ) ^ 2 ) + ( ( N ` ( ( A G ( J S C ) ) G ( -u 1 S B ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) )
59 5 16 7 58 mp3an 
 |-  ( ( ( N ` ( ( A G ( J S C ) ) G B ) ) ^ 2 ) + ( ( N ` ( ( A G ( J S C ) ) G ( -u 1 S B ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) )
60 11 19 33 adddii 
 |-  ( 2 x. ( ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) = ( ( 2 x. ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) ) + ( 2 x. ( ( N ` B ) ^ 2 ) ) )
61 57 59 60 3eqtri 
 |-  ( ( ( N ` ( ( A G B ) G ( J S C ) ) ) ^ 2 ) + ( ( N ` ( ( A G ( -u 1 S B ) ) G ( J S C ) ) ) ^ 2 ) ) = ( ( 2 x. ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) ) + ( 2 x. ( ( N ` B ) ^ 2 ) ) )
62 6 7 22 3pm3.2i 
 |-  ( A e. X /\ B e. X /\ ( -u J S C ) e. X )
63 44 ablo32 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ ( -u J S C ) e. X ) ) -> ( ( A G B ) G ( -u J S C ) ) = ( ( A G ( -u J S C ) ) G B ) )
64 42 62 63 mp2an 
 |-  ( ( A G B ) G ( -u J S C ) ) = ( ( A G ( -u J S C ) ) G B )
65 64 fveq2i 
 |-  ( N ` ( ( A G B ) G ( -u J S C ) ) ) = ( N ` ( ( A G ( -u J S C ) ) G B ) )
66 65 oveq1i 
 |-  ( ( N ` ( ( A G B ) G ( -u J S C ) ) ) ^ 2 ) = ( ( N ` ( ( A G ( -u J S C ) ) G B ) ) ^ 2 )
67 6 51 22 3pm3.2i 
 |-  ( A e. X /\ ( -u 1 S B ) e. X /\ ( -u J S C ) e. X )
68 44 ablo32 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ ( -u 1 S B ) e. X /\ ( -u J S C ) e. X ) ) -> ( ( A G ( -u 1 S B ) ) G ( -u J S C ) ) = ( ( A G ( -u J S C ) ) G ( -u 1 S B ) ) )
69 42 67 68 mp2an 
 |-  ( ( A G ( -u 1 S B ) ) G ( -u J S C ) ) = ( ( A G ( -u J S C ) ) G ( -u 1 S B ) )
70 69 fveq2i 
 |-  ( N ` ( ( A G ( -u 1 S B ) ) G ( -u J S C ) ) ) = ( N ` ( ( A G ( -u J S C ) ) G ( -u 1 S B ) ) )
71 70 oveq1i 
 |-  ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u J S C ) ) ) ^ 2 ) = ( ( N ` ( ( A G ( -u J S C ) ) G ( -u 1 S B ) ) ) ^ 2 )
72 66 71 oveq12i 
 |-  ( ( ( N ` ( ( A G B ) G ( -u J S C ) ) ) ^ 2 ) + ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u J S C ) ) ) ^ 2 ) ) = ( ( ( N ` ( ( A G ( -u J S C ) ) G B ) ) ^ 2 ) + ( ( N ` ( ( A G ( -u J S C ) ) G ( -u 1 S B ) ) ) ^ 2 ) )
73 1 2 3 9 phpar 
 |-  ( ( U e. CPreHilOLD /\ ( A G ( -u J S C ) ) e. X /\ B e. X ) -> ( ( ( N ` ( ( A G ( -u J S C ) ) G B ) ) ^ 2 ) + ( ( N ` ( ( A G ( -u J S C ) ) G ( -u 1 S B ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) )
74 5 24 7 73 mp3an 
 |-  ( ( ( N ` ( ( A G ( -u J S C ) ) G B ) ) ^ 2 ) + ( ( N ` ( ( A G ( -u J S C ) ) G ( -u 1 S B ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) )
75 11 27 33 adddii 
 |-  ( 2 x. ( ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) = ( ( 2 x. ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) ) + ( 2 x. ( ( N ` B ) ^ 2 ) ) )
76 72 74 75 3eqtri 
 |-  ( ( ( N ` ( ( A G B ) G ( -u J S C ) ) ) ^ 2 ) + ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u J S C ) ) ) ^ 2 ) ) = ( ( 2 x. ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) ) + ( 2 x. ( ( N ` B ) ^ 2 ) ) )
77 61 76 oveq12i 
 |-  ( ( ( ( N ` ( ( A G B ) G ( J S C ) ) ) ^ 2 ) + ( ( N ` ( ( A G ( -u 1 S B ) ) G ( J S C ) ) ) ^ 2 ) ) - ( ( ( N ` ( ( A G B ) G ( -u J S C ) ) ) ^ 2 ) + ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u J S C ) ) ) ^ 2 ) ) ) = ( ( ( 2 x. ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) ) + ( 2 x. ( ( N ` B ) ^ 2 ) ) ) - ( ( 2 x. ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) ) + ( 2 x. ( ( N ` B ) ^ 2 ) ) ) )
78 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G B ) e. X )
79 12 6 7 78 mp3an 
 |-  ( A G B ) e. X
80 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ ( A G B ) e. X /\ ( J S C ) e. X ) -> ( ( A G B ) G ( J S C ) ) e. X )
81 12 79 14 80 mp3an 
 |-  ( ( A G B ) G ( J S C ) ) e. X
82 1 9 12 81 nvcli 
 |-  ( N ` ( ( A G B ) G ( J S C ) ) ) e. RR
83 82 recni 
 |-  ( N ` ( ( A G B ) G ( J S C ) ) ) e. CC
84 83 sqcli 
 |-  ( ( N ` ( ( A G B ) G ( J S C ) ) ) ^ 2 ) e. CC
85 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ ( -u 1 S B ) e. X ) -> ( A G ( -u 1 S B ) ) e. X )
86 12 6 51 85 mp3an 
 |-  ( A G ( -u 1 S B ) ) e. X
87 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ ( A G ( -u 1 S B ) ) e. X /\ ( J S C ) e. X ) -> ( ( A G ( -u 1 S B ) ) G ( J S C ) ) e. X )
88 12 86 14 87 mp3an 
 |-  ( ( A G ( -u 1 S B ) ) G ( J S C ) ) e. X
89 1 9 12 88 nvcli 
 |-  ( N ` ( ( A G ( -u 1 S B ) ) G ( J S C ) ) ) e. RR
90 89 recni 
 |-  ( N ` ( ( A G ( -u 1 S B ) ) G ( J S C ) ) ) e. CC
91 90 sqcli 
 |-  ( ( N ` ( ( A G ( -u 1 S B ) ) G ( J S C ) ) ) ^ 2 ) e. CC
92 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ ( A G B ) e. X /\ ( -u J S C ) e. X ) -> ( ( A G B ) G ( -u J S C ) ) e. X )
93 12 79 22 92 mp3an 
 |-  ( ( A G B ) G ( -u J S C ) ) e. X
94 1 9 12 93 nvcli 
 |-  ( N ` ( ( A G B ) G ( -u J S C ) ) ) e. RR
95 94 recni 
 |-  ( N ` ( ( A G B ) G ( -u J S C ) ) ) e. CC
96 95 sqcli 
 |-  ( ( N ` ( ( A G B ) G ( -u J S C ) ) ) ^ 2 ) e. CC
97 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ ( A G ( -u 1 S B ) ) e. X /\ ( -u J S C ) e. X ) -> ( ( A G ( -u 1 S B ) ) G ( -u J S C ) ) e. X )
98 12 86 22 97 mp3an 
 |-  ( ( A G ( -u 1 S B ) ) G ( -u J S C ) ) e. X
99 1 9 12 98 nvcli 
 |-  ( N ` ( ( A G ( -u 1 S B ) ) G ( -u J S C ) ) ) e. RR
100 99 recni 
 |-  ( N ` ( ( A G ( -u 1 S B ) ) G ( -u J S C ) ) ) e. CC
101 100 sqcli 
 |-  ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u J S C ) ) ) ^ 2 ) e. CC
102 84 91 96 101 addsub4i 
 |-  ( ( ( ( N ` ( ( A G B ) G ( J S C ) ) ) ^ 2 ) + ( ( N ` ( ( A G ( -u 1 S B ) ) G ( J S C ) ) ) ^ 2 ) ) - ( ( ( N ` ( ( A G B ) G ( -u J S C ) ) ) ^ 2 ) + ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u J S C ) ) ) ^ 2 ) ) ) = ( ( ( ( N ` ( ( A G B ) G ( J S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u J S C ) ) ) ^ 2 ) ) + ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( J S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u J S C ) ) ) ^ 2 ) ) )
103 37 77 102 3eqtr2ri 
 |-  ( ( ( ( N ` ( ( A G B ) G ( J S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G B ) G ( -u J S C ) ) ) ^ 2 ) ) + ( ( ( N ` ( ( A G ( -u 1 S B ) ) G ( J S C ) ) ) ^ 2 ) - ( ( N ` ( ( A G ( -u 1 S B ) ) G ( -u J S C ) ) ) ^ 2 ) ) ) = ( 2 x. ( ( ( N ` ( A G ( J S C ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u J S C ) ) ) ^ 2 ) ) )