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

Theorem lmod0vs 19596
Description: Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 28714 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
Hypotheses
Ref Expression
lmod0vs.v 𝑉 = (Base‘𝑊)
lmod0vs.f 𝐹 = (Scalar‘𝑊)
lmod0vs.s · = ( ·𝑠𝑊)
lmod0vs.o 𝑂 = (0g𝐹)
lmod0vs.z 0 = (0g𝑊)
Assertion
Ref Expression
lmod0vs ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (𝑂 · 𝑋) = 0 )

Proof of Theorem lmod0vs
StepHypRef Expression
1 simpl 483 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝑊 ∈ LMod)
2 lmod0vs.f . . . . . . . 8 𝐹 = (Scalar‘𝑊)
32lmodring 19571 . . . . . . 7 (𝑊 ∈ LMod → 𝐹 ∈ Ring)
43adantr 481 . . . . . 6 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝐹 ∈ Ring)
5 eqid 2818 . . . . . . 7 (Base‘𝐹) = (Base‘𝐹)
6 lmod0vs.o . . . . . . 7 𝑂 = (0g𝐹)
75, 6ring0cl 19248 . . . . . 6 (𝐹 ∈ Ring → 𝑂 ∈ (Base‘𝐹))
84, 7syl 17 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝑂 ∈ (Base‘𝐹))
9 simpr 485 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝑋𝑉)
10 lmod0vs.v . . . . . 6 𝑉 = (Base‘𝑊)
11 eqid 2818 . . . . . 6 (+g𝑊) = (+g𝑊)
12 lmod0vs.s . . . . . 6 · = ( ·𝑠𝑊)
13 eqid 2818 . . . . . 6 (+g𝐹) = (+g𝐹)
1410, 11, 2, 12, 5, 13lmodvsdir 19587 . . . . 5 ((𝑊 ∈ LMod ∧ (𝑂 ∈ (Base‘𝐹) ∧ 𝑂 ∈ (Base‘𝐹) ∧ 𝑋𝑉)) → ((𝑂(+g𝐹)𝑂) · 𝑋) = ((𝑂 · 𝑋)(+g𝑊)(𝑂 · 𝑋)))
151, 8, 8, 9, 14syl13anc 1364 . . . 4 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ((𝑂(+g𝐹)𝑂) · 𝑋) = ((𝑂 · 𝑋)(+g𝑊)(𝑂 · 𝑋)))
16 ringgrp 19231 . . . . . . 7 (𝐹 ∈ Ring → 𝐹 ∈ Grp)
174, 16syl 17 . . . . . 6 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝐹 ∈ Grp)
185, 13, 6grplid 18071 . . . . . 6 ((𝐹 ∈ Grp ∧ 𝑂 ∈ (Base‘𝐹)) → (𝑂(+g𝐹)𝑂) = 𝑂)
1917, 8, 18syl2anc 584 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (𝑂(+g𝐹)𝑂) = 𝑂)
2019oveq1d 7160 . . . 4 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ((𝑂(+g𝐹)𝑂) · 𝑋) = (𝑂 · 𝑋))
2115, 20eqtr3d 2855 . . 3 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ((𝑂 · 𝑋)(+g𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋))
2210, 2, 12, 5lmodvscl 19580 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑂 ∈ (Base‘𝐹) ∧ 𝑋𝑉) → (𝑂 · 𝑋) ∈ 𝑉)
231, 8, 9, 22syl3anc 1363 . . . 4 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (𝑂 · 𝑋) ∈ 𝑉)
24 lmod0vs.z . . . . 5 0 = (0g𝑊)
2510, 11, 24lmod0vid 19595 . . . 4 ((𝑊 ∈ LMod ∧ (𝑂 · 𝑋) ∈ 𝑉) → (((𝑂 · 𝑋)(+g𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋) ↔ 0 = (𝑂 · 𝑋)))
2623, 25syldan 591 . . 3 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (((𝑂 · 𝑋)(+g𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋) ↔ 0 = (𝑂 · 𝑋)))
2721, 26mpbid 233 . 2 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 0 = (𝑂 · 𝑋))
2827eqcomd 2824 1 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (𝑂 · 𝑋) = 0 )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  cfv 6348  (class class class)co 7145  Basecbs 16471  +gcplusg 16553  Scalarcsca 16556   ·𝑠 cvsca 16557  0gc0g 16701  Grpcgrp 18041  Ringcrg 19226  LModclmod 19563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-iota 6307  df-fun 6350  df-fv 6356  df-riota 7103  df-ov 7148  df-0g 16703  df-mgm 17840  df-sgrp 17889  df-mnd 17900  df-grp 18044  df-ring 19228  df-lmod 19565
This theorem is referenced by:  lmodvs0  19597  lmodvsmmulgdi  19598  lcomfsupp  19603  lmodvneg1  19606  mptscmfsupp0  19628  lvecvs0or  19809  lssvs0or  19811  lspsneleq  19816  lspdisj  19826  lspfixed  19829  lspexch  19830  lspsolvlem  19843  lspsolv  19844  ascl0  20041  mplcoe1  20174  mplbas2  20179  ply10s0  20352  ply1scl0  20386  gsummoncoe1  20400  uvcresum  20865  frlmsslsp  20868  frlmup1  20870  frlmup2  20871  pmatcollpwscmatlem1  21325  idpm2idmp  21337  mp2pm2mplem4  21345  pm2mpmhmlem1  21354  monmat2matmon  21360  cpmidpmatlem3  21408  clm0vs  23626  plypf1  24729  lmodslmd  30759  lbsdiflsp0  30921  fedgmullem2  30925  lshpkrlem1  36126  ldual0vs  36176  lclkrlem1  38522  lcd0vs  38631  baerlem3lem1  38723  baerlem5blem1  38725  hdmap14lem2a  38883  hdmap14lem4a  38887  hdmap14lem6  38889  hgmapval0  38908  prjspersym  39135  prjspreln0  39137  lmod0rng  44067  scmsuppss  44348  lmodvsmdi  44358  ply1mulgsumlem4  44371  lincval1  44402  lincvalsc0  44404  linc0scn0  44406  linc1  44408  ldepsprlem  44455
  Copyright terms: Public domain W3C validator