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 ยท ๐ด ) ) ) )