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 mullidd ⊢ ( ( 𝑈 ∈ 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 𝑆 𝐴 ) ) ) )