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=normCV⁡U
Assertion nvpi ⊢U∈NrmCVec∧A∈X∧B∈X→N⁡AGiSB=N⁡BG−iSA

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=normCV⁡U
5 simp1 ⊢U∈NrmCVec∧A∈X∧B∈X→U∈NrmCVec
6 ax-icn ⊢i∈ℂ
7 1 3 nvscl ⊢U∈NrmCVec∧i∈ℂ∧B∈X→iSB∈X
8 6 7 mp3an2 ⊢U∈NrmCVec∧B∈X→iSB∈X
9 8 3adant2 ⊢U∈NrmCVec∧A∈X∧B∈X→iSB∈X
10 1 2 nvgcl ⊢U∈NrmCVec∧A∈X∧iSB∈X→AGiSB∈X
11 9 10 syld3an3 ⊢U∈NrmCVec∧A∈X∧B∈X→AGiSB∈X
12 1 4 nvcl ⊢U∈NrmCVec∧AGiSB∈X→N⁡AGiSB∈ℝ
13 5 11 12 syl2anc ⊢U∈NrmCVec∧A∈X∧B∈X→N⁡AGiSB∈ℝ
14 13 recnd ⊢U∈NrmCVec∧A∈X∧B∈X→N⁡AGiSB∈ℂ
15 14 mullidd ⊢U∈NrmCVec∧A∈X∧B∈X→1⁢N⁡AGiSB=N⁡AGiSB
16 6 absnegi ⊢−i=i
17 absi ⊢i=1
18 16 17 eqtri ⊢−i=1
19 18 oveq1i ⊢−i⁢N⁡AGiSB=1⁢N⁡AGiSB
20 negicn ⊢−i∈ℂ
21 1 3 4 nvs ⊢U∈NrmCVec∧−i∈ℂ∧AGiSB∈X→N⁡−iSAGiSB=−i⁢N⁡AGiSB
22 20 21 mp3an2 ⊢U∈NrmCVec∧AGiSB∈X→N⁡−iSAGiSB=−i⁢N⁡AGiSB
23 5 11 22 syl2anc ⊢U∈NrmCVec∧A∈X∧B∈X→N⁡−iSAGiSB=−i⁢N⁡AGiSB
24 simp2 ⊢U∈NrmCVec∧A∈X∧B∈X→A∈X
25 1 2 3 nvdi ⊢U∈NrmCVec∧−i∈ℂ∧A∈X∧iSB∈X→−iSAGiSB=−iSAG−iSiSB
26 20 25 mp3anr1 ⊢U∈NrmCVec∧A∈X∧iSB∈X→−iSAGiSB=−iSAG−iSiSB
27 5 24 9 26 syl12anc ⊢U∈NrmCVec∧A∈X∧B∈X→−iSAGiSB=−iSAG−iSiSB
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⁢iSB=1SB
35 1 3 nvsass ⊢U∈NrmCVec∧−i∈ℂ∧i∈ℂ∧B∈X→−i⁢iSB=−iSiSB
36 20 35 mp3anr1 ⊢U∈NrmCVec∧i∈ℂ∧B∈X→−i⁢iSB=−iSiSB
37 6 36 mpanr1 ⊢U∈NrmCVec∧B∈X→−i⁢iSB=−iSiSB
38 1 3 nvsid ⊢U∈NrmCVec∧B∈X→1SB=B
39 34 37 38 3eqtr3a ⊢U∈NrmCVec∧B∈X→−iSiSB=B
40 39 3adant2 ⊢U∈NrmCVec∧A∈X∧B∈X→−iSiSB=B
41 40 oveq2d ⊢U∈NrmCVec∧A∈X∧B∈X→−iSAG−iSiSB=−iSAGB
42 1 3 nvscl ⊢U∈NrmCVec∧−i∈ℂ∧A∈X→−iSA∈X
43 20 42 mp3an2 ⊢U∈NrmCVec∧A∈X→−iSA∈X
44 43 3adant3 ⊢U∈NrmCVec∧A∈X∧B∈X→−iSA∈X
45 1 2 nvcom ⊢U∈NrmCVec∧−iSA∈X∧B∈X→−iSAGB=BG−iSA
46 44 45 syld3an2 ⊢U∈NrmCVec∧A∈X∧B∈X→−iSAGB=BG−iSA
47 27 41 46 3eqtrd ⊢U∈NrmCVec∧A∈X∧B∈X→−iSAGiSB=BG−iSA
48 47 fveq2d ⊢U∈NrmCVec∧A∈X∧B∈X→N⁡−iSAGiSB=N⁡BG−iSA
49 23 48 eqtr3d ⊢U∈NrmCVec∧A∈X∧B∈X→−i⁢N⁡AGiSB=N⁡BG−iSA
50 19 49 eqtr3id ⊢U∈NrmCVec∧A∈X∧B∈X→1⁢N⁡AGiSB=N⁡BG−iSA
51 15 50 eqtr3d ⊢U∈NrmCVec∧A∈X∧B∈X→N⁡AGiSB=N⁡BG−iSA