Metamath Proof Explorer


Theorem nvpi

Description: The norm of a vector plus the imaginary scalar product of another. (Contributed by NM, 2-Feb-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvdif.1 X = BaseSet U
nvdif.2 G = + v U
nvdif.4 S = 𝑠OLD U
nvdif.6 N = norm CV U
Assertion nvpi U NrmCVec A X B X N A G i S B = N B G i S A

Proof

Step Hyp Ref Expression
1 nvdif.1 X = BaseSet U
2 nvdif.2 G = + v U
3 nvdif.4 S = 𝑠OLD U
4 nvdif.6 N = norm CV U
5 simp1 U NrmCVec A X B X U NrmCVec
6 ax-icn i
7 1 3 nvscl U NrmCVec i B X i S B X
8 6 7 mp3an2 U NrmCVec B X i S B X
9 8 3adant2 U NrmCVec A X B X i S B X
10 1 2 nvgcl U NrmCVec A X i S B X A G i S B X
11 9 10 syld3an3 U NrmCVec A X B X A G i S B X
12 1 4 nvcl U NrmCVec A G i S B X N A G i S B
13 5 11 12 syl2anc U NrmCVec A X B X N A G i S B
14 13 recnd U NrmCVec A X B X N A G i S B
15 14 mulid2d U NrmCVec A X B X 1 N A G i S B = N A G i S B
16 6 absnegi i = i
17 absi i = 1
18 16 17 eqtri i = 1
19 18 oveq1i i N A G i S B = 1 N A G i S B
20 negicn i
21 1 3 4 nvs U NrmCVec i A G i S B X N i S A G i S B = i N A G i S B
22 20 21 mp3an2 U NrmCVec A G i S B X N i S A G i S B = i N A G i S B
23 5 11 22 syl2anc U NrmCVec A X B X N i S A G i S B = i N A G i S B
24 simp2 U NrmCVec A X B X A X
25 1 2 3 nvdi U NrmCVec i A X i S B X i S A G i S B = i S A G i S i S B
26 20 25 mp3anr1 U NrmCVec A X i S B X i S A G i S B = i S A G i S i S B
27 5 24 9 26 syl12anc U NrmCVec A X B X i S A G i S B = i S A G i S i S B
28 6 6 mulneg1i i i = i i
29 ixi i i = 1
30 29 negeqi i i = -1
31 negneg1e1 -1 = 1
32 30 31 eqtri i i = 1
33 28 32 eqtri i i = 1
34 33 oveq1i i i S B = 1 S B
35 1 3 nvsass U NrmCVec i i B X i i S B = i S i S B
36 20 35 mp3anr1 U NrmCVec i B X i i S B = i S i S B
37 6 36 mpanr1 U NrmCVec B X i i S B = i S i S B
38 1 3 nvsid U NrmCVec B X 1 S B = B
39 34 37 38 3eqtr3a U NrmCVec B X i S i S B = B
40 39 3adant2 U NrmCVec A X B X i S i S B = B
41 40 oveq2d U NrmCVec A X B X i S A G i S i S B = i S A G B
42 1 3 nvscl U NrmCVec i A X i S A X
43 20 42 mp3an2 U NrmCVec A X i S A X
44 43 3adant3 U NrmCVec A X B X i S A X
45 1 2 nvcom U NrmCVec i S A X B X i S A G B = B G i S A
46 44 45 syld3an2 U NrmCVec A X B X i S A G B = B G i S A
47 27 41 46 3eqtrd U NrmCVec A X B X i S A G i S B = B G i S A
48 47 fveq2d U NrmCVec A X B X N i S A G i S B = N B G i S A
49 23 48 eqtr3d U NrmCVec A X B X i N A G i S B = N B G i S A
50 19 49 eqtr3id U NrmCVec A X B X 1 N A G i S B = N B G i S A
51 15 50 eqtr3d U NrmCVec A X B X N A G i S B = N B G i S A