MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ncvspi Structured version   Visualization version   GIF version

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

Proof of Theorem ncvspi
StepHypRef Expression
1 elin 4167 . . . . . . 7 (𝑊 ∈ (NrmVec ∩ ℂVec) ↔ (𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec))
2 nvcnlm 23297 . . . . . . . . 9 (𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod)
3 nlmngp 23278 . . . . . . . . 9 (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp)
42, 3syl 17 . . . . . . . 8 (𝑊 ∈ NrmVec → 𝑊 ∈ NrmGrp)
54adantr 483 . . . . . . 7 ((𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec) → 𝑊 ∈ NrmGrp)
61, 5sylbi 219 . . . . . 6 (𝑊 ∈ (NrmVec ∩ ℂVec) → 𝑊 ∈ NrmGrp)
763ad2ant1 1127 . . . . 5 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → 𝑊 ∈ NrmGrp)
8 nvclmod 23299 . . . . . . . . . 10 (𝑊 ∈ NrmVec → 𝑊 ∈ LMod)
9 lmodgrp 19633 . . . . . . . . . 10 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
108, 9syl 17 . . . . . . . . 9 (𝑊 ∈ NrmVec → 𝑊 ∈ Grp)
1110adantr 483 . . . . . . . 8 ((𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec) → 𝑊 ∈ Grp)
121, 11sylbi 219 . . . . . . 7 (𝑊 ∈ (NrmVec ∩ ℂVec) → 𝑊 ∈ Grp)
13123ad2ant1 1127 . . . . . 6 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → 𝑊 ∈ Grp)
14 simp2l 1193 . . . . . 6 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → 𝐴𝑉)
15 id 22 . . . . . . . . . 10 (𝑊 ∈ ℂVec → 𝑊 ∈ ℂVec)
1615cvsclm 23722 . . . . . . . . 9 (𝑊 ∈ ℂVec → 𝑊 ∈ ℂMod)
171, 16simplbiim 507 . . . . . . . 8 (𝑊 ∈ (NrmVec ∩ ℂVec) → 𝑊 ∈ ℂMod)
18173ad2ant1 1127 . . . . . . 7 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → 𝑊 ∈ ℂMod)
19 simp3 1132 . . . . . . 7 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → i ∈ 𝐾)
20 simp2r 1194 . . . . . . 7 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → 𝐵𝑉)
21 ncvsprp.v . . . . . . . 8 𝑉 = (Base‘𝑊)
22 ncvspi.f . . . . . . . 8 𝐹 = (Scalar‘𝑊)
23 ncvsprp.s . . . . . . . 8 · = ( ·𝑠𝑊)
24 ncvspi.k . . . . . . . 8 𝐾 = (Base‘𝐹)
2521, 22, 23, 24clmvscl 23684 . . . . . . 7 ((𝑊 ∈ ℂMod ∧ i ∈ 𝐾𝐵𝑉) → (i · 𝐵) ∈ 𝑉)
2618, 19, 20, 25syl3anc 1365 . . . . . 6 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → (i · 𝐵) ∈ 𝑉)
27 ncvsdif.p . . . . . . 7 + = (+g𝑊)
2821, 27grpcl 18103 . . . . . 6 ((𝑊 ∈ Grp ∧ 𝐴𝑉 ∧ (i · 𝐵) ∈ 𝑉) → (𝐴 + (i · 𝐵)) ∈ 𝑉)
2913, 14, 26, 28syl3anc 1365 . . . . 5 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → (𝐴 + (i · 𝐵)) ∈ 𝑉)
30 ncvsprp.n . . . . . 6 𝑁 = (norm‘𝑊)
3121, 30nmcl 23217 . . . . 5 ((𝑊 ∈ NrmGrp ∧ (𝐴 + (i · 𝐵)) ∈ 𝑉) → (𝑁‘(𝐴 + (i · 𝐵))) ∈ ℝ)
327, 29, 31syl2anc 586 . . . 4 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → (𝑁‘(𝐴 + (i · 𝐵))) ∈ ℝ)
3332recnd 10661 . . 3 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → (𝑁‘(𝐴 + (i · 𝐵))) ∈ ℂ)
3433mulid2d 10651 . 2 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → (1 · (𝑁‘(𝐴 + (i · 𝐵)))) = (𝑁‘(𝐴 + (i · 𝐵))))
35 ax-icn 10588 . . . . . 6 i ∈ ℂ
3635absnegi 14752 . . . . 5 (abs‘-i) = (abs‘i)
37 absi 14638 . . . . 5 (abs‘i) = 1
3836, 37eqtri 2842 . . . 4 (abs‘-i) = 1
3938oveq1i 7158 . . 3 ((abs‘-i) · (𝑁‘(𝐴 + (i · 𝐵)))) = (1 · (𝑁‘(𝐴 + (i · 𝐵))))
40 simp1 1130 . . . . 5 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → 𝑊 ∈ (NrmVec ∩ ℂVec))
4122, 24clmneg 23677 . . . . . . . . . . 11 ((𝑊 ∈ ℂMod ∧ i ∈ 𝐾) → -i = ((invg𝐹)‘i))
4216, 41sylan 582 . . . . . . . . . 10 ((𝑊 ∈ ℂVec ∧ i ∈ 𝐾) → -i = ((invg𝐹)‘i))
4322clmfgrp 23667 . . . . . . . . . . . 12 (𝑊 ∈ ℂMod → 𝐹 ∈ Grp)
4416, 43syl 17 . . . . . . . . . . 11 (𝑊 ∈ ℂVec → 𝐹 ∈ Grp)
45 eqid 2819 . . . . . . . . . . . 12 (invg𝐹) = (invg𝐹)
4624, 45grpinvcl 18143 . . . . . . . . . . 11 ((𝐹 ∈ Grp ∧ i ∈ 𝐾) → ((invg𝐹)‘i) ∈ 𝐾)
4744, 46sylan 582 . . . . . . . . . 10 ((𝑊 ∈ ℂVec ∧ i ∈ 𝐾) → ((invg𝐹)‘i) ∈ 𝐾)
4842, 47eqeltrd 2911 . . . . . . . . 9 ((𝑊 ∈ ℂVec ∧ i ∈ 𝐾) → -i ∈ 𝐾)
4948ex 415 . . . . . . . 8 (𝑊 ∈ ℂVec → (i ∈ 𝐾 → -i ∈ 𝐾))
501, 49simplbiim 507 . . . . . . 7 (𝑊 ∈ (NrmVec ∩ ℂVec) → (i ∈ 𝐾 → -i ∈ 𝐾))
5150imp 409 . . . . . 6 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ i ∈ 𝐾) → -i ∈ 𝐾)
52513adant2 1125 . . . . 5 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → -i ∈ 𝐾)
5321, 30, 23, 22, 24ncvsprp 23748 . . . . 5 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ -i ∈ 𝐾 ∧ (𝐴 + (i · 𝐵)) ∈ 𝑉) → (𝑁‘(-i · (𝐴 + (i · 𝐵)))) = ((abs‘-i) · (𝑁‘(𝐴 + (i · 𝐵)))))
5440, 52, 29, 53syl3anc 1365 . . . 4 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → (𝑁‘(-i · (𝐴 + (i · 𝐵)))) = ((abs‘-i) · (𝑁‘(𝐴 + (i · 𝐵)))))
5521, 22, 23, 24, 27clmvsdi 23688 . . . . . . 7 ((𝑊 ∈ ℂMod ∧ (-i ∈ 𝐾𝐴𝑉 ∧ (i · 𝐵) ∈ 𝑉)) → (-i · (𝐴 + (i · 𝐵))) = ((-i · 𝐴) + (-i · (i · 𝐵))))
5618, 52, 14, 26, 55syl13anc 1366 . . . . . 6 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → (-i · (𝐴 + (i · 𝐵))) = ((-i · 𝐴) + (-i · (i · 𝐵))))
5735, 35mulneg1i 11078 . . . . . . . . . 10 (-i · i) = -(i · i)
58 ixi 11261 . . . . . . . . . . . 12 (i · i) = -1
5958negeqi 10871 . . . . . . . . . . 11 -(i · i) = --1
60 negneg1e1 11747 . . . . . . . . . . 11 --1 = 1
6159, 60eqtri 2842 . . . . . . . . . 10 -(i · i) = 1
6257, 61eqtri 2842 . . . . . . . . 9 (-i · i) = 1
6362oveq1i 7158 . . . . . . . 8 ((-i · i) · 𝐵) = (1 · 𝐵)
6421, 22, 23, 24clmvsass 23685 . . . . . . . . 9 ((𝑊 ∈ ℂMod ∧ (-i ∈ 𝐾 ∧ i ∈ 𝐾𝐵𝑉)) → ((-i · i) · 𝐵) = (-i · (i · 𝐵)))
6518, 52, 19, 20, 64syl13anc 1366 . . . . . . . 8 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → ((-i · i) · 𝐵) = (-i · (i · 𝐵)))
66 simpr 487 . . . . . . . . . . 11 ((𝐴𝑉𝐵𝑉) → 𝐵𝑉)
6717, 66anim12i 614 . . . . . . . . . 10 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉)) → (𝑊 ∈ ℂMod ∧ 𝐵𝑉))
68673adant3 1126 . . . . . . . . 9 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → (𝑊 ∈ ℂMod ∧ 𝐵𝑉))
6921, 23clmvs1 23689 . . . . . . . . 9 ((𝑊 ∈ ℂMod ∧ 𝐵𝑉) → (1 · 𝐵) = 𝐵)
7068, 69syl 17 . . . . . . . 8 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → (1 · 𝐵) = 𝐵)
7163, 65, 703eqtr3a 2878 . . . . . . 7 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → (-i · (i · 𝐵)) = 𝐵)
7271oveq2d 7164 . . . . . 6 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → ((-i · 𝐴) + (-i · (i · 𝐵))) = ((-i · 𝐴) + 𝐵))
73 clmabl 23665 . . . . . . . . . 10 (𝑊 ∈ ℂMod → 𝑊 ∈ Abel)
7416, 73syl 17 . . . . . . . . 9 (𝑊 ∈ ℂVec → 𝑊 ∈ Abel)
751, 74simplbiim 507 . . . . . . . 8 (𝑊 ∈ (NrmVec ∩ ℂVec) → 𝑊 ∈ Abel)
76753ad2ant1 1127 . . . . . . 7 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → 𝑊 ∈ Abel)
7721, 22, 23, 24clmvscl 23684 . . . . . . . 8 ((𝑊 ∈ ℂMod ∧ -i ∈ 𝐾𝐴𝑉) → (-i · 𝐴) ∈ 𝑉)
7818, 52, 14, 77syl3anc 1365 . . . . . . 7 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → (-i · 𝐴) ∈ 𝑉)
7921, 27ablcom 18916 . . . . . . 7 ((𝑊 ∈ Abel ∧ (-i · 𝐴) ∈ 𝑉𝐵𝑉) → ((-i · 𝐴) + 𝐵) = (𝐵 + (-i · 𝐴)))
8076, 78, 20, 79syl3anc 1365 . . . . . 6 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → ((-i · 𝐴) + 𝐵) = (𝐵 + (-i · 𝐴)))
8156, 72, 803eqtrd 2858 . . . . 5 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → (-i · (𝐴 + (i · 𝐵))) = (𝐵 + (-i · 𝐴)))
8281fveq2d 6667 . . . 4 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → (𝑁‘(-i · (𝐴 + (i · 𝐵)))) = (𝑁‘(𝐵 + (-i · 𝐴))))
8354, 82eqtr3d 2856 . . 3 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → ((abs‘-i) · (𝑁‘(𝐴 + (i · 𝐵)))) = (𝑁‘(𝐵 + (-i · 𝐴))))
8439, 83syl5eqr 2868 . 2 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → (1 · (𝑁‘(𝐴 + (i · 𝐵)))) = (𝑁‘(𝐵 + (-i · 𝐴))))
8534, 84eqtr3d 2856 1 ((𝑊 ∈ (NrmVec ∩ ℂVec) ∧ (𝐴𝑉𝐵𝑉) ∧ i ∈ 𝐾) → (𝑁‘(𝐴 + (i · 𝐵))) = (𝑁‘(𝐵 + (-i · 𝐴))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  w3a 1081   = wceq 1530  wcel 2107  cin 3933  cfv 6348  (class class class)co 7148  cr 10528  1c1 10530  ici 10531   · cmul 10534  -cneg 10863  abscabs 14585  Basecbs 16475  +gcplusg 16557  Scalarcsca 16560   ·𝑠 cvsca 16561  Grpcgrp 18095  invgcminusg 18096  Abelcabl 18899  LModclmod 19626  normcnm 23178  NrmGrpcngp 23179  NrmModcnlm 23182  NrmVeccnvc 23183  ℂModcclm 23658  ℂVecccvs 23719
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-oadd 8098  df-er 8281  df-map 8400  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-sup 8898  df-inf 8899  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-fz 12885  df-seq 13362  df-exp 13422  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-0g 16707  df-topgen 16709  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-grp 18098  df-minusg 18099  df-subg 18268  df-cmn 18900  df-abl 18901  df-mgp 19232  df-ur 19244  df-ring 19291  df-cring 19292  df-subrg 19525  df-lmod 19628  df-psmet 20529  df-xmet 20530  df-met 20531  df-bl 20532  df-mopn 20533  df-cnfld 20538  df-top 21494  df-topon 21511  df-topsp 21533  df-bases 21546  df-xms 22922  df-ms 22923  df-nm 23184  df-ngp 23185  df-nlm 23188  df-nvc 23189  df-clm 23659  df-cvs 23720
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator