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 mullidd ⊢ 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