# 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 )`
` |-  ( ( W e. NrmVec /\ W e. CVec ) -> W e. NrmGrp )`
12 7 11 sylbi
` |-  ( W e. ( NrmVec i^i CVec ) -> W e. NrmGrp )`
` |-  ( ( 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 )`
` |-  ( ( W e. NrmVec /\ W e. CVec ) -> W e. Grp )`
18 7 17 sylbi
` |-  ( W e. ( NrmVec i^i CVec ) -> W e. Grp )`
` |-  ( ( 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 )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) ) ) )`