# 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}={\mathrm{Base}}_{{W}}$
ncvsprp.n ${⊢}{N}=\mathrm{norm}\left({W}\right)$
ncvsprp.s
ncvsdif.p
ncvspi.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
ncvspi.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
Assertion ncvspi

### Proof

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