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 
|- V = ( Base ` W )
ncvsprp.n 
|- N = ( norm ` W )
ncvsprp.s 
|- .x. = ( .s ` W )
ncvsdif.p 
|- .+ = ( +g ` W )
ncvspi.f 
|- F = ( Scalar ` W )
ncvspi.k 
|- K = ( Base ` F )
Assertion ncvspi 
|- ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( N ` ( A .+ ( _i .x. B ) ) ) = ( N ` ( B .+ ( -u _i .x. A ) ) ) )

Proof

Step Hyp Ref Expression
1 ncvsprp.v 
 |-  V = ( Base ` W )
2 ncvsprp.n 
 |-  N = ( norm ` W )
3 ncvsprp.s 
 |-  .x. = ( .s ` W )
4 ncvsdif.p 
 |-  .+ = ( +g ` W )
5 ncvspi.f 
 |-  F = ( Scalar ` W )
6 ncvspi.k 
 |-  K = ( Base ` F )
7 elin 
 |-  ( W e. ( NrmVec i^i CVec ) <-> ( W e. NrmVec /\ W e. CVec ) )
8 nvcnlm 
 |-  ( W e. NrmVec -> W e. NrmMod )
9 nlmngp 
 |-  ( W e. NrmMod -> W e. NrmGrp )
10 8 9 syl 
 |-  ( W e. NrmVec -> W e. NrmGrp )
11 10 adantr 
 |-  ( ( W e. NrmVec /\ W e. CVec ) -> W e. NrmGrp )
12 7 11 sylbi 
 |-  ( W e. ( NrmVec i^i CVec ) -> W e. NrmGrp )
13 12 3ad2ant1 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> W e. NrmGrp )
14 nvclmod 
 |-  ( W e. NrmVec -> W e. LMod )
15 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
16 14 15 syl 
 |-  ( W e. NrmVec -> W e. Grp )
17 16 adantr 
 |-  ( ( W e. NrmVec /\ W e. CVec ) -> W e. Grp )
18 7 17 sylbi 
 |-  ( W e. ( NrmVec i^i CVec ) -> W e. Grp )
19 18 3ad2ant1 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> W e. Grp )
20 simp2l 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> A e. V )
21 id 
 |-  ( W e. CVec -> W e. CVec )
22 21 cvsclm 
 |-  ( W e. CVec -> W e. CMod )
23 7 22 simplbiim 
 |-  ( W e. ( NrmVec i^i CVec ) -> W e. CMod )
24 23 3ad2ant1 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> W e. CMod )
25 simp3 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> _i e. K )
26 simp2r 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> B e. V )
27 1 5 3 6 clmvscl 
 |-  ( ( W e. CMod /\ _i e. K /\ B e. V ) -> ( _i .x. B ) e. V )
28 24 25 26 27 syl3anc 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( _i .x. B ) e. V )
29 1 4 grpcl 
 |-  ( ( W e. Grp /\ A e. V /\ ( _i .x. B ) e. V ) -> ( A .+ ( _i .x. B ) ) e. V )
30 19 20 28 29 syl3anc 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( A .+ ( _i .x. B ) ) e. V )
31 1 2 nmcl 
 |-  ( ( W e. NrmGrp /\ ( A .+ ( _i .x. B ) ) e. V ) -> ( N ` ( A .+ ( _i .x. B ) ) ) e. RR )
32 13 30 31 syl2anc 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( N ` ( A .+ ( _i .x. B ) ) ) e. RR )
33 32 recnd 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( N ` ( A .+ ( _i .x. B ) ) ) e. CC )
34 33 mulid2d 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( 1 x. ( N ` ( A .+ ( _i .x. B ) ) ) ) = ( N ` ( A .+ ( _i .x. B ) ) ) )
35 ax-icn 
 |-  _i e. CC
36 35 absnegi 
 |-  ( abs ` -u _i ) = ( abs ` _i )
37 absi 
 |-  ( abs ` _i ) = 1
38 36 37 eqtri 
 |-  ( abs ` -u _i ) = 1
39 38 oveq1i 
 |-  ( ( abs ` -u _i ) x. ( N ` ( A .+ ( _i .x. B ) ) ) ) = ( 1 x. ( N ` ( A .+ ( _i .x. B ) ) ) )
40 simp1 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> W e. ( NrmVec i^i CVec ) )
41 5 6 clmneg 
 |-  ( ( W e. CMod /\ _i e. K ) -> -u _i = ( ( invg ` F ) ` _i ) )
42 22 41 sylan 
 |-  ( ( W e. CVec /\ _i e. K ) -> -u _i = ( ( invg ` F ) ` _i ) )
43 5 clmfgrp 
 |-  ( W e. CMod -> F e. Grp )
44 22 43 syl 
 |-  ( W e. CVec -> F e. Grp )
45 eqid 
 |-  ( invg ` F ) = ( invg ` F )
46 6 45 grpinvcl 
 |-  ( ( F e. Grp /\ _i e. K ) -> ( ( invg ` F ) ` _i ) e. K )
47 44 46 sylan 
 |-  ( ( W e. CVec /\ _i e. K ) -> ( ( invg ` F ) ` _i ) e. K )
48 42 47 eqeltrd 
 |-  ( ( W e. CVec /\ _i e. K ) -> -u _i e. K )
49 48 ex 
 |-  ( W e. CVec -> ( _i e. K -> -u _i e. K ) )
50 7 49 simplbiim 
 |-  ( W e. ( NrmVec i^i CVec ) -> ( _i e. K -> -u _i e. K ) )
51 50 imp 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ _i e. K ) -> -u _i e. K )
52 51 3adant2 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> -u _i e. K )
53 1 2 3 5 6 ncvsprp 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ -u _i e. K /\ ( A .+ ( _i .x. B ) ) e. V ) -> ( N ` ( -u _i .x. ( A .+ ( _i .x. B ) ) ) ) = ( ( abs ` -u _i ) x. ( N ` ( A .+ ( _i .x. B ) ) ) ) )
54 40 52 30 53 syl3anc 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( N ` ( -u _i .x. ( A .+ ( _i .x. B ) ) ) ) = ( ( abs ` -u _i ) x. ( N ` ( A .+ ( _i .x. B ) ) ) ) )
55 1 5 3 6 4 clmvsdi 
 |-  ( ( W e. CMod /\ ( -u _i e. K /\ A e. V /\ ( _i .x. B ) e. V ) ) -> ( -u _i .x. ( A .+ ( _i .x. B ) ) ) = ( ( -u _i .x. A ) .+ ( -u _i .x. ( _i .x. B ) ) ) )
56 24 52 20 28 55 syl13anc 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( -u _i .x. ( A .+ ( _i .x. B ) ) ) = ( ( -u _i .x. A ) .+ ( -u _i .x. ( _i .x. B ) ) ) )
57 35 35 mulneg1i 
 |-  ( -u _i x. _i ) = -u ( _i x. _i )
58 ixi 
 |-  ( _i x. _i ) = -u 1
59 58 negeqi 
 |-  -u ( _i x. _i ) = -u -u 1
60 negneg1e1 
 |-  -u -u 1 = 1
61 59 60 eqtri 
 |-  -u ( _i x. _i ) = 1
62 57 61 eqtri 
 |-  ( -u _i x. _i ) = 1
63 62 oveq1i 
 |-  ( ( -u _i x. _i ) .x. B ) = ( 1 .x. B )
64 1 5 3 6 clmvsass 
 |-  ( ( W e. CMod /\ ( -u _i e. K /\ _i e. K /\ B e. V ) ) -> ( ( -u _i x. _i ) .x. B ) = ( -u _i .x. ( _i .x. B ) ) )
65 24 52 25 26 64 syl13anc 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( ( -u _i x. _i ) .x. B ) = ( -u _i .x. ( _i .x. B ) ) )
66 simpr 
 |-  ( ( A e. V /\ B e. V ) -> B e. V )
67 23 66 anim12i 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) ) -> ( W e. CMod /\ B e. V ) )
68 67 3adant3 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( W e. CMod /\ B e. V ) )
69 1 3 clmvs1 
 |-  ( ( W e. CMod /\ B e. V ) -> ( 1 .x. B ) = B )
70 68 69 syl 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( 1 .x. B ) = B )
71 63 65 70 3eqtr3a 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( -u _i .x. ( _i .x. B ) ) = B )
72 71 oveq2d 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( ( -u _i .x. A ) .+ ( -u _i .x. ( _i .x. B ) ) ) = ( ( -u _i .x. A ) .+ B ) )
73 clmabl 
 |-  ( W e. CMod -> W e. Abel )
74 22 73 syl 
 |-  ( W e. CVec -> W e. Abel )
75 7 74 simplbiim 
 |-  ( W e. ( NrmVec i^i CVec ) -> W e. Abel )
76 75 3ad2ant1 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> W e. Abel )
77 1 5 3 6 clmvscl 
 |-  ( ( W e. CMod /\ -u _i e. K /\ A e. V ) -> ( -u _i .x. A ) e. V )
78 24 52 20 77 syl3anc 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( -u _i .x. A ) e. V )
79 1 4 ablcom 
 |-  ( ( W e. Abel /\ ( -u _i .x. A ) e. V /\ B e. V ) -> ( ( -u _i .x. A ) .+ B ) = ( B .+ ( -u _i .x. A ) ) )
80 76 78 26 79 syl3anc 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( ( -u _i .x. A ) .+ B ) = ( B .+ ( -u _i .x. A ) ) )
81 56 72 80 3eqtrd 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( -u _i .x. ( A .+ ( _i .x. B ) ) ) = ( B .+ ( -u _i .x. A ) ) )
82 81 fveq2d 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( N ` ( -u _i .x. ( A .+ ( _i .x. B ) ) ) ) = ( N ` ( B .+ ( -u _i .x. A ) ) ) )
83 54 82 eqtr3d 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( ( abs ` -u _i ) x. ( N ` ( A .+ ( _i .x. B ) ) ) ) = ( N ` ( B .+ ( -u _i .x. A ) ) ) )
84 39 83 syl5eqr 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( 1 x. ( N ` ( A .+ ( _i .x. B ) ) ) ) = ( N ` ( B .+ ( -u _i .x. A ) ) ) )
85 34 84 eqtr3d 
 |-  ( ( W e. ( NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( N ` ( A .+ ( _i .x. B ) ) ) = ( N ` ( B .+ ( -u _i .x. A ) ) ) )