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 𝑋 = ( BaseSet ‘ 𝑈 )
nvdif.2 𝐺 = ( +𝑣𝑈 )
nvdif.4 𝑆 = ( ·𝑠OLD𝑈 )
nvdif.6 𝑁 = ( normCV𝑈 )
Assertion nvpi ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 nvdif.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvdif.2 𝐺 = ( +𝑣𝑈 )
3 nvdif.4 𝑆 = ( ·𝑠OLD𝑈 )
4 nvdif.6 𝑁 = ( normCV𝑈 )
5 simp1 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → 𝑈 ∈ NrmCVec )
6 ax-icn i ∈ ℂ
7 1 3 nvscl ( ( 𝑈 ∈ NrmCVec ∧ i ∈ ℂ ∧ 𝐵𝑋 ) → ( i 𝑆 𝐵 ) ∈ 𝑋 )
8 6 7 mp3an2 ( ( 𝑈 ∈ NrmCVec ∧ 𝐵𝑋 ) → ( i 𝑆 𝐵 ) ∈ 𝑋 )
9 8 3adant2 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( i 𝑆 𝐵 ) ∈ 𝑋 )
10 1 2 nvgcl ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ∧ ( i 𝑆 𝐵 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ∈ 𝑋 )
11 9 10 syld3an3 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ∈ 𝑋 )
12 1 4 nvcl ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ∈ ℝ )
13 5 11 12 syl2anc ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ∈ ℝ )
14 13 recnd ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ∈ ℂ )
15 14 mulid2d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( 1 · ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) )
16 6 absnegi ( abs ‘ - i ) = ( abs ‘ i )
17 absi ( abs ‘ i ) = 1
18 16 17 eqtri ( abs ‘ - i ) = 1
19 18 oveq1i ( ( abs ‘ - i ) · ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) = ( 1 · ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) )
20 negicn - i ∈ ℂ
21 1 3 4 nvs ( ( 𝑈 ∈ NrmCVec ∧ - i ∈ ℂ ∧ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( - i 𝑆 ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) = ( ( abs ‘ - i ) · ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) )
22 20 21 mp3an2 ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( - i 𝑆 ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) = ( ( abs ‘ - i ) · ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) )
23 5 11 22 syl2anc ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝑁 ‘ ( - i 𝑆 ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) = ( ( abs ‘ - i ) · ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) )
24 simp2 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → 𝐴𝑋 )
25 1 2 3 nvdi ( ( 𝑈 ∈ NrmCVec ∧ ( - i ∈ ℂ ∧ 𝐴𝑋 ∧ ( i 𝑆 𝐵 ) ∈ 𝑋 ) ) → ( - i 𝑆 ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) = ( ( - i 𝑆 𝐴 ) 𝐺 ( - i 𝑆 ( i 𝑆 𝐵 ) ) ) )
26 20 25 mp3anr1 ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋 ∧ ( i 𝑆 𝐵 ) ∈ 𝑋 ) ) → ( - i 𝑆 ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) = ( ( - i 𝑆 𝐴 ) 𝐺 ( - i 𝑆 ( i 𝑆 𝐵 ) ) ) )
27 5 24 9 26 syl12anc ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( - i 𝑆 ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) = ( ( - i 𝑆 𝐴 ) 𝐺 ( - i 𝑆 ( i 𝑆 𝐵 ) ) ) )
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 ) 𝑆 𝐵 ) = ( 1 𝑆 𝐵 )
35 1 3 nvsass ( ( 𝑈 ∈ NrmCVec ∧ ( - i ∈ ℂ ∧ i ∈ ℂ ∧ 𝐵𝑋 ) ) → ( ( - i · i ) 𝑆 𝐵 ) = ( - i 𝑆 ( i 𝑆 𝐵 ) ) )
36 20 35 mp3anr1 ( ( 𝑈 ∈ NrmCVec ∧ ( i ∈ ℂ ∧ 𝐵𝑋 ) ) → ( ( - i · i ) 𝑆 𝐵 ) = ( - i 𝑆 ( i 𝑆 𝐵 ) ) )
37 6 36 mpanr1 ( ( 𝑈 ∈ NrmCVec ∧ 𝐵𝑋 ) → ( ( - i · i ) 𝑆 𝐵 ) = ( - i 𝑆 ( i 𝑆 𝐵 ) ) )
38 1 3 nvsid ( ( 𝑈 ∈ NrmCVec ∧ 𝐵𝑋 ) → ( 1 𝑆 𝐵 ) = 𝐵 )
39 34 37 38 3eqtr3a ( ( 𝑈 ∈ NrmCVec ∧ 𝐵𝑋 ) → ( - i 𝑆 ( i 𝑆 𝐵 ) ) = 𝐵 )
40 39 3adant2 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( - i 𝑆 ( i 𝑆 𝐵 ) ) = 𝐵 )
41 40 oveq2d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( ( - i 𝑆 𝐴 ) 𝐺 ( - i 𝑆 ( i 𝑆 𝐵 ) ) ) = ( ( - i 𝑆 𝐴 ) 𝐺 𝐵 ) )
42 1 3 nvscl ( ( 𝑈 ∈ NrmCVec ∧ - i ∈ ℂ ∧ 𝐴𝑋 ) → ( - i 𝑆 𝐴 ) ∈ 𝑋 )
43 20 42 mp3an2 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( - i 𝑆 𝐴 ) ∈ 𝑋 )
44 43 3adant3 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( - i 𝑆 𝐴 ) ∈ 𝑋 )
45 1 2 nvcom ( ( 𝑈 ∈ NrmCVec ∧ ( - i 𝑆 𝐴 ) ∈ 𝑋𝐵𝑋 ) → ( ( - i 𝑆 𝐴 ) 𝐺 𝐵 ) = ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) )
46 44 45 syld3an2 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( ( - i 𝑆 𝐴 ) 𝐺 𝐵 ) = ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) )
47 27 41 46 3eqtrd ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( - i 𝑆 ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) = ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) )
48 47 fveq2d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝑁 ‘ ( - i 𝑆 ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) = ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) )
49 23 48 eqtr3d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( ( abs ‘ - i ) · ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) = ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) )
50 19 49 eqtr3id ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( 1 · ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) ) = ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) )
51 15 50 eqtr3d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( i 𝑆 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐵 𝐺 ( - i 𝑆 𝐴 ) ) ) )