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

Theorem lmodvneg1 18670
Description: Minus 1 times a vector is the negative of the vector. Equation 2 of [Kreyszig] p. 51. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
Hypotheses
Ref Expression
lmodvneg1.v 𝑉 = (Base‘𝑊)
lmodvneg1.n 𝑁 = (invg𝑊)
lmodvneg1.f 𝐹 = (Scalar‘𝑊)
lmodvneg1.s · = ( ·𝑠𝑊)
lmodvneg1.u 1 = (1r𝐹)
lmodvneg1.m 𝑀 = (invg𝐹)
Assertion
Ref Expression
lmodvneg1 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ((𝑀1 ) · 𝑋) = (𝑁𝑋))

Proof of Theorem lmodvneg1
StepHypRef Expression
1 simpl 471 . . . 4 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝑊 ∈ LMod)
2 lmodvneg1.f . . . . . . 7 𝐹 = (Scalar‘𝑊)
32lmodfgrp 18636 . . . . . 6 (𝑊 ∈ LMod → 𝐹 ∈ Grp)
43adantr 479 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝐹 ∈ Grp)
5 eqid 2604 . . . . . . 7 (Base‘𝐹) = (Base‘𝐹)
6 lmodvneg1.u . . . . . . 7 1 = (1r𝐹)
72, 5, 6lmod1cl 18654 . . . . . 6 (𝑊 ∈ LMod → 1 ∈ (Base‘𝐹))
87adantr 479 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 1 ∈ (Base‘𝐹))
9 lmodvneg1.m . . . . . 6 𝑀 = (invg𝐹)
105, 9grpinvcl 17231 . . . . 5 ((𝐹 ∈ Grp ∧ 1 ∈ (Base‘𝐹)) → (𝑀1 ) ∈ (Base‘𝐹))
114, 8, 10syl2anc 690 . . . 4 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (𝑀1 ) ∈ (Base‘𝐹))
12 simpr 475 . . . 4 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝑋𝑉)
13 lmodvneg1.v . . . . 5 𝑉 = (Base‘𝑊)
14 lmodvneg1.s . . . . 5 · = ( ·𝑠𝑊)
1513, 2, 14, 5lmodvscl 18644 . . . 4 ((𝑊 ∈ LMod ∧ (𝑀1 ) ∈ (Base‘𝐹) ∧ 𝑋𝑉) → ((𝑀1 ) · 𝑋) ∈ 𝑉)
161, 11, 12, 15syl3anc 1317 . . 3 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ((𝑀1 ) · 𝑋) ∈ 𝑉)
17 eqid 2604 . . . 4 (+g𝑊) = (+g𝑊)
18 eqid 2604 . . . 4 (0g𝑊) = (0g𝑊)
1913, 17, 18lmod0vrid 18658 . . 3 ((𝑊 ∈ LMod ∧ ((𝑀1 ) · 𝑋) ∈ 𝑉) → (((𝑀1 ) · 𝑋)(+g𝑊)(0g𝑊)) = ((𝑀1 ) · 𝑋))
2016, 19syldan 485 . 2 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (((𝑀1 ) · 𝑋)(+g𝑊)(0g𝑊)) = ((𝑀1 ) · 𝑋))
21 lmodvneg1.n . . . . . 6 𝑁 = (invg𝑊)
2213, 21lmodvnegcl 18668 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (𝑁𝑋) ∈ 𝑉)
2313, 17lmodass 18642 . . . . 5 ((𝑊 ∈ LMod ∧ (((𝑀1 ) · 𝑋) ∈ 𝑉𝑋𝑉 ∧ (𝑁𝑋) ∈ 𝑉)) → ((((𝑀1 ) · 𝑋)(+g𝑊)𝑋)(+g𝑊)(𝑁𝑋)) = (((𝑀1 ) · 𝑋)(+g𝑊)(𝑋(+g𝑊)(𝑁𝑋))))
241, 16, 12, 22, 23syl13anc 1319 . . . 4 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ((((𝑀1 ) · 𝑋)(+g𝑊)𝑋)(+g𝑊)(𝑁𝑋)) = (((𝑀1 ) · 𝑋)(+g𝑊)(𝑋(+g𝑊)(𝑁𝑋))))
2513, 2, 14, 6lmodvs1 18655 . . . . . . 7 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ( 1 · 𝑋) = 𝑋)
2625oveq2d 6538 . . . . . 6 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (((𝑀1 ) · 𝑋)(+g𝑊)( 1 · 𝑋)) = (((𝑀1 ) · 𝑋)(+g𝑊)𝑋))
27 eqid 2604 . . . . . . . . . 10 (+g𝐹) = (+g𝐹)
28 eqid 2604 . . . . . . . . . 10 (0g𝐹) = (0g𝐹)
295, 27, 28, 9grplinv 17232 . . . . . . . . 9 ((𝐹 ∈ Grp ∧ 1 ∈ (Base‘𝐹)) → ((𝑀1 )(+g𝐹) 1 ) = (0g𝐹))
304, 8, 29syl2anc 690 . . . . . . . 8 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ((𝑀1 )(+g𝐹) 1 ) = (0g𝐹))
3130oveq1d 6537 . . . . . . 7 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (((𝑀1 )(+g𝐹) 1 ) · 𝑋) = ((0g𝐹) · 𝑋))
3213, 17, 2, 14, 5, 27lmodvsdir 18651 . . . . . . . 8 ((𝑊 ∈ LMod ∧ ((𝑀1 ) ∈ (Base‘𝐹) ∧ 1 ∈ (Base‘𝐹) ∧ 𝑋𝑉)) → (((𝑀1 )(+g𝐹) 1 ) · 𝑋) = (((𝑀1 ) · 𝑋)(+g𝑊)( 1 · 𝑋)))
331, 11, 8, 12, 32syl13anc 1319 . . . . . . 7 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (((𝑀1 )(+g𝐹) 1 ) · 𝑋) = (((𝑀1 ) · 𝑋)(+g𝑊)( 1 · 𝑋)))
3413, 2, 14, 28, 18lmod0vs 18660 . . . . . . 7 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ((0g𝐹) · 𝑋) = (0g𝑊))
3531, 33, 343eqtr3d 2646 . . . . . 6 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (((𝑀1 ) · 𝑋)(+g𝑊)( 1 · 𝑋)) = (0g𝑊))
3626, 35eqtr3d 2640 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (((𝑀1 ) · 𝑋)(+g𝑊)𝑋) = (0g𝑊))
3736oveq1d 6537 . . . 4 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ((((𝑀1 ) · 𝑋)(+g𝑊)𝑋)(+g𝑊)(𝑁𝑋)) = ((0g𝑊)(+g𝑊)(𝑁𝑋)))
3824, 37eqtr3d 2640 . . 3 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (((𝑀1 ) · 𝑋)(+g𝑊)(𝑋(+g𝑊)(𝑁𝑋))) = ((0g𝑊)(+g𝑊)(𝑁𝑋)))
3913, 17, 18, 21lmodvnegid 18669 . . . 4 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (𝑋(+g𝑊)(𝑁𝑋)) = (0g𝑊))
4039oveq2d 6538 . . 3 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (((𝑀1 ) · 𝑋)(+g𝑊)(𝑋(+g𝑊)(𝑁𝑋))) = (((𝑀1 ) · 𝑋)(+g𝑊)(0g𝑊)))
4113, 17, 18lmod0vlid 18657 . . . 4 ((𝑊 ∈ LMod ∧ (𝑁𝑋) ∈ 𝑉) → ((0g𝑊)(+g𝑊)(𝑁𝑋)) = (𝑁𝑋))
4222, 41syldan 485 . . 3 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ((0g𝑊)(+g𝑊)(𝑁𝑋)) = (𝑁𝑋))
4338, 40, 423eqtr3d 2646 . 2 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (((𝑀1 ) · 𝑋)(+g𝑊)(0g𝑊)) = (𝑁𝑋))
4420, 43eqtr3d 2640 1 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ((𝑀1 ) · 𝑋) = (𝑁𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1975  cfv 5785  (class class class)co 6522  Basecbs 15636  +gcplusg 15709  Scalarcsca 15712   ·𝑠 cvsca 15713  0gc0g 15864  Grpcgrp 17186  invgcminusg 17187  1rcur 18265  LModclmod 18627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584  ax-rep 4688  ax-sep 4698  ax-nul 4707  ax-pow 4759  ax-pr 4823  ax-un 6819  ax-cnex 9843  ax-resscn 9844  ax-1cn 9845  ax-icn 9846  ax-addcl 9847  ax-addrcl 9848  ax-mulcl 9849  ax-mulrcl 9850  ax-mulcom 9851  ax-addass 9852  ax-mulass 9853  ax-distr 9854  ax-i2m1 9855  ax-1ne0 9856  ax-1rid 9857  ax-rnegex 9858  ax-rrecex 9859  ax-cnre 9860  ax-pre-lttri 9861  ax-pre-lttrn 9862  ax-pre-ltadd 9863  ax-pre-mulgt0 9864
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2456  df-mo 2457  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-ne 2776  df-nel 2777  df-ral 2895  df-rex 2896  df-reu 2897  df-rmo 2898  df-rab 2899  df-v 3169  df-sbc 3397  df-csb 3494  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-pss 3550  df-nul 3869  df-if 4031  df-pw 4104  df-sn 4120  df-pr 4122  df-tp 4124  df-op 4126  df-uni 4362  df-iun 4446  df-br 4573  df-opab 4633  df-mpt 4634  df-tr 4670  df-eprel 4934  df-id 4938  df-po 4944  df-so 4945  df-fr 4982  df-we 4984  df-xp 5029  df-rel 5030  df-cnv 5031  df-co 5032  df-dm 5033  df-rn 5034  df-res 5035  df-ima 5036  df-pred 5578  df-ord 5624  df-on 5625  df-lim 5626  df-suc 5627  df-iota 5749  df-fun 5787  df-fn 5788  df-f 5789  df-f1 5790  df-fo 5791  df-f1o 5792  df-fv 5793  df-riota 6484  df-ov 6525  df-oprab 6526  df-mpt2 6527  df-om 6930  df-wrecs 7266  df-recs 7327  df-rdg 7365  df-er 7601  df-en 7814  df-dom 7815  df-sdom 7816  df-pnf 9927  df-mnf 9928  df-xr 9929  df-ltxr 9930  df-le 9931  df-sub 10114  df-neg 10115  df-nn 10863  df-2 10921  df-ndx 15639  df-slot 15640  df-base 15641  df-sets 15642  df-plusg 15722  df-0g 15866  df-mgm 17006  df-sgrp 17048  df-mnd 17059  df-grp 17189  df-minusg 17190  df-mgp 18254  df-ur 18266  df-ring 18313  df-lmod 18629
This theorem is referenced by:  lmodvsneg  18671  lmodvsubval2  18682  lssvnegcl  18718  lspsnneg  18768  lmodvsinv  18798  lspsolvlem  18904  tlmtgp  21746  clmvneg1  22633  deg1invg  23582
  Copyright terms: Public domain W3C validator