Metamath Proof Explorer

Theorem ncvspi

Description: The norm of a vector plus the imaginary scalar product of another. (Contributed by NM, 2-Feb-2007) (Revised by AV, 8-Oct-2021)

Ref Expression
Hypotheses ncvsprp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ncvsprp.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
ncvsprp.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
ncvsdif.p ⊢ + = ( +g ‘ 𝑊 )
ncvspi.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
ncvspi.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion ncvspi ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐵 + ( - i · 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 ncvsprp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 ncvsprp.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
3 ncvsprp.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 ncvsdif.p ⊢ + = ( +g ‘ 𝑊 )
5 ncvspi.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
6 ncvspi.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
7 elin ⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ↔ ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec ) )
8 nvcnlm ⊢ ( 𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod )
9 nlmngp ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp )
10 8 9 syl ⊢ ( 𝑊 ∈ NrmVec → 𝑊 ∈ NrmGrp )
11 10 adantr ⊢ ( ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec ) → 𝑊 ∈ NrmGrp )
12 7 11 sylbi ⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) → 𝑊 ∈ NrmGrp )
13 12 3ad2ant1 ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → 𝑊 ∈ NrmGrp )
14 nvclmod ⊢ ( 𝑊 ∈ NrmVec → 𝑊 ∈ LMod )
15 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
16 14 15 syl ⊢ ( 𝑊 ∈ NrmVec → 𝑊 ∈ Grp )
17 16 adantr ⊢ ( ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec ) → 𝑊 ∈ Grp )
18 7 17 sylbi ⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) → 𝑊 ∈ Grp )
19 18 3ad2ant1 ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → 𝑊 ∈ Grp )
20 simp2l ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → 𝐴 ∈ 𝑉 )
21 id ⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ ℂVec )
22 21 cvsclm ⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ ℂMod )
23 7 22 simplbiim ⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) → 𝑊 ∈ ℂMod )
24 23 3ad2ant1 ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → 𝑊 ∈ ℂMod )
25 simp3 ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → i ∈ 𝐾 )
26 simp2r ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → 𝐵 ∈ 𝑉 )
27 1 5 3 6 clmvscl ⊢ ( ( 𝑊 ∈ ℂMod ∧ i ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ) → ( i · 𝐵 ) ∈ 𝑉 )
28 24 25 26 27 syl3anc ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( i · 𝐵 ) ∈ 𝑉 )
29 1 4 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑉 ∧ ( i · 𝐵 ) ∈ 𝑉 ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ 𝑉 )
30 19 20 28 29 syl3anc ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ 𝑉 )
31 1 2 nmcl ⊢ ( ( 𝑊 ∈ NrmGrp ∧ ( 𝐴 + ( i · 𝐵 ) ) ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℝ )
32 13 30 31 syl2anc ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℝ )
33 32 recnd ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℂ )
34 33 mulid2d ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( 1 · ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) = ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) )
35 ax-icn ⊢ i ∈ ℂ
36 35 absnegi ⊢ ( abs ‘ - i ) = ( abs ‘ i )
37 absi ⊢ ( abs ‘ i ) = 1
38 36 37 eqtri ⊢ ( abs ‘ - i ) = 1
39 38 oveq1i ⊢ ( ( abs ‘ - i ) · ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) = ( 1 · ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) )
40 simp1 ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → 𝑊 ∈ ( NrmVec ∩ ℂVec ) )
41 5 6 clmneg ⊢ ( ( 𝑊 ∈ ℂMod ∧ i ∈ 𝐾 ) → - i = ( ( invg ‘ 𝐹 ) ‘ i ) )
42 22 41 sylan ⊢ ( ( 𝑊 ∈ ℂVec ∧ i ∈ 𝐾 ) → - i = ( ( invg ‘ 𝐹 ) ‘ i ) )
43 5 clmfgrp ⊢ ( 𝑊 ∈ ℂMod → 𝐹 ∈ Grp )
44 22 43 syl ⊢ ( 𝑊 ∈ ℂVec → 𝐹 ∈ Grp )
45 eqid ⊢ ( invg ‘ 𝐹 ) = ( invg ‘ 𝐹 )
46 6 45 grpinvcl ⊢ ( ( 𝐹 ∈ Grp ∧ i ∈ 𝐾 ) → ( ( invg ‘ 𝐹 ) ‘ i ) ∈ 𝐾 )
47 44 46 sylan ⊢ ( ( 𝑊 ∈ ℂVec ∧ i ∈ 𝐾 ) → ( ( invg ‘ 𝐹 ) ‘ i ) ∈ 𝐾 )
48 42 47 eqeltrd ⊢ ( ( 𝑊 ∈ ℂVec ∧ i ∈ 𝐾 ) → - i ∈ 𝐾 )
49 48 ex ⊢ ( 𝑊 ∈ ℂVec → ( i ∈ 𝐾 → - i ∈ 𝐾 ) )
50 7 49 simplbiim ⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) → ( i ∈ 𝐾 → - i ∈ 𝐾 ) )
51 50 imp ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ i ∈ 𝐾 ) → - i ∈ 𝐾 )
52 51 3adant2 ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → - i ∈ 𝐾 )
53 1 2 3 5 6 ncvsprp ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ - i ∈ 𝐾 ∧ ( 𝐴 + ( i · 𝐵 ) ) ∈ 𝑉 ) → ( 𝑁 ‘ ( - i · ( 𝐴 + ( i · 𝐵 ) ) ) ) = ( ( abs ‘ - i ) · ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) )
54 40 52 30 53 syl3anc ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( 𝑁 ‘ ( - i · ( 𝐴 + ( i · 𝐵 ) ) ) ) = ( ( abs ‘ - i ) · ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) )
55 1 5 3 6 4 clmvsdi ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( - i ∈ 𝐾 ∧ 𝐴 ∈ 𝑉 ∧ ( i · 𝐵 ) ∈ 𝑉 ) ) → ( - i · ( 𝐴 + ( i · 𝐵 ) ) ) = ( ( - i · 𝐴 ) + ( - i · ( i · 𝐵 ) ) ) )
56 24 52 20 28 55 syl13anc ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( - i · ( 𝐴 + ( i · 𝐵 ) ) ) = ( ( - i · 𝐴 ) + ( - i · ( i · 𝐵 ) ) ) )
57 35 35 mulneg1i ⊢ ( - i · i ) = - ( i · i )
58 ixi ⊢ ( i · i ) = - 1
59 58 negeqi ⊢ - ( i · i ) = - - 1
60 negneg1e1 ⊢ - - 1 = 1
61 59 60 eqtri ⊢ - ( i · i ) = 1
62 57 61 eqtri ⊢ ( - i · i ) = 1
63 62 oveq1i ⊢ ( ( - i · i ) · 𝐵 ) = ( 1 · 𝐵 )
64 1 5 3 6 clmvsass ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( - i ∈ 𝐾 ∧ i ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ) ) → ( ( - i · i ) · 𝐵 ) = ( - i · ( i · 𝐵 ) ) )
65 24 52 25 26 64 syl13anc ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( ( - i · i ) · 𝐵 ) = ( - i · ( i · 𝐵 ) ) )
66 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ 𝑉 )
67 23 66 anim12i ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉 ) )
68 67 3adant3 ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( 𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉 ) )
69 1 3 clmvs1 ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉 ) → ( 1 · 𝐵 ) = 𝐵 )
70 68 69 syl ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( 1 · 𝐵 ) = 𝐵 )
71 63 65 70 3eqtr3a ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( - i · ( i · 𝐵 ) ) = 𝐵 )
72 71 oveq2d ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( ( - i · 𝐴 ) + ( - i · ( i · 𝐵 ) ) ) = ( ( - i · 𝐴 ) + 𝐵 ) )
73 clmabl ⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ Abel )
74 22 73 syl ⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ Abel )
75 7 74 simplbiim ⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) → 𝑊 ∈ Abel )
76 75 3ad2ant1 ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → 𝑊 ∈ Abel )
77 1 5 3 6 clmvscl ⊢ ( ( 𝑊 ∈ ℂMod ∧ - i ∈ 𝐾 ∧ 𝐴 ∈ 𝑉 ) → ( - i · 𝐴 ) ∈ 𝑉 )
78 24 52 20 77 syl3anc ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( - i · 𝐴 ) ∈ 𝑉 )
79 1 4 ablcom ⊢ ( ( 𝑊 ∈ Abel ∧ ( - i · 𝐴 ) ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( - i · 𝐴 ) + 𝐵 ) = ( 𝐵 + ( - i · 𝐴 ) ) )
80 76 78 26 79 syl3anc ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( ( - i · 𝐴 ) + 𝐵 ) = ( 𝐵 + ( - i · 𝐴 ) ) )
81 56 72 80 3eqtrd ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( - i · ( 𝐴 + ( i · 𝐵 ) ) ) = ( 𝐵 + ( - i · 𝐴 ) ) )
82 81 fveq2d ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( 𝑁 ‘ ( - i · ( 𝐴 + ( i · 𝐵 ) ) ) ) = ( 𝑁 ‘ ( 𝐵 + ( - i · 𝐴 ) ) ) )
83 54 82 eqtr3d ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( ( abs ‘ - i ) · ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) = ( 𝑁 ‘ ( 𝐵 + ( - i · 𝐴 ) ) ) )
84 39 83 eqtr3id ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( 1 · ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) = ( 𝑁 ‘ ( 𝐵 + ( - i · 𝐴 ) ) ) )
85 34 84 eqtr3d ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ i ∈ 𝐾 ) → ( 𝑁 ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐵 + ( - i · 𝐴 ) ) ) )