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

Theorem lmod0vs 20909
Description: Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 31038 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 482 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝑊 ∈ LMod)
2 lmod0vs.f . . . . . . . 8 𝐹 = (Scalar‘𝑊)
32lmodring 20882 . . . . . . 7 (𝑊 ∈ LMod → 𝐹 ∈ Ring)
43adantr 480 . . . . . 6 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝐹 ∈ Ring)
5 eqid 2734 . . . . . . 7 (Base‘𝐹) = (Base‘𝐹)
6 lmod0vs.o . . . . . . 7 𝑂 = (0g𝐹)
75, 6ring0cl 20280 . . . . . 6 (𝐹 ∈ Ring → 𝑂 ∈ (Base‘𝐹))
84, 7syl 17 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝑂 ∈ (Base‘𝐹))
9 simpr 484 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝑋𝑉)
10 lmod0vs.v . . . . . 6 𝑉 = (Base‘𝑊)
11 eqid 2734 . . . . . 6 (+g𝑊) = (+g𝑊)
12 lmod0vs.s . . . . . 6 · = ( ·𝑠𝑊)
13 eqid 2734 . . . . . 6 (+g𝐹) = (+g𝐹)
1410, 11, 2, 12, 5, 13lmodvsdir 20900 . . . . 5 ((𝑊 ∈ LMod ∧ (𝑂 ∈ (Base‘𝐹) ∧ 𝑂 ∈ (Base‘𝐹) ∧ 𝑋𝑉)) → ((𝑂(+g𝐹)𝑂) · 𝑋) = ((𝑂 · 𝑋)(+g𝑊)(𝑂 · 𝑋)))
151, 8, 8, 9, 14syl13anc 1371 . . . 4 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ((𝑂(+g𝐹)𝑂) · 𝑋) = ((𝑂 · 𝑋)(+g𝑊)(𝑂 · 𝑋)))
16 ringgrp 20255 . . . . . . 7 (𝐹 ∈ Ring → 𝐹 ∈ Grp)
174, 16syl 17 . . . . . 6 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝐹 ∈ Grp)
185, 13, 6grplid 18997 . . . . . 6 ((𝐹 ∈ Grp ∧ 𝑂 ∈ (Base‘𝐹)) → (𝑂(+g𝐹)𝑂) = 𝑂)
1917, 8, 18syl2anc 584 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (𝑂(+g𝐹)𝑂) = 𝑂)
2019oveq1d 7445 . . . 4 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ((𝑂(+g𝐹)𝑂) · 𝑋) = (𝑂 · 𝑋))
2115, 20eqtr3d 2776 . . 3 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ((𝑂 · 𝑋)(+g𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋))
2210, 2, 12, 5lmodvscl 20892 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑂 ∈ (Base‘𝐹) ∧ 𝑋𝑉) → (𝑂 · 𝑋) ∈ 𝑉)
231, 8, 9, 22syl3anc 1370 . . . 4 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (𝑂 · 𝑋) ∈ 𝑉)
24 lmod0vs.z . . . . 5 0 = (0g𝑊)
2510, 11, 24lmod0vid 20908 . . . 4 ((𝑊 ∈ LMod ∧ (𝑂 · 𝑋) ∈ 𝑉) → (((𝑂 · 𝑋)(+g𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋) ↔ 0 = (𝑂 · 𝑋)))
2623, 25syldan 591 . . 3 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (((𝑂 · 𝑋)(+g𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋) ↔ 0 = (𝑂 · 𝑋)))
2721, 26mpbid 232 . 2 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 0 = (𝑂 · 𝑋))
2827eqcomd 2740 1 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (𝑂 · 𝑋) = 0 )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1536  wcel 2105  cfv 6562  (class class class)co 7430  Basecbs 17244  +gcplusg 17297  Scalarcsca 17300   ·𝑠 cvsca 17301  0gc0g 17485  Grpcgrp 18963  Ringcrg 20250  LModclmod 20874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fv 6570  df-riota 7387  df-ov 7433  df-0g 17487  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-grp 18966  df-ring 20252  df-lmod 20876
This theorem is referenced by:  lmodvs0  20910  lmodvsmmulgdi  20911  lcomfsupp  20916  lmodvneg1  20919  mptscmfsupp0  20941  lvecvs0or  21127  lssvs0or  21129  lspsneleq  21134  lspdisj  21144  lspfixed  21147  lspexch  21148  lspsolvlem  21161  lspsolv  21162  uvcresum  21830  frlmsslsp  21833  frlmup1  21835  frlmup2  21836  ascl0  21921  mplcoe1  22072  mplbas2  22077  ply10s0  22274  ply1scl0OLD  22309  gsummoncoe1  22327  evls1fpws  22388  pmatcollpwscmatlem1  22810  idpm2idmp  22822  mp2pm2mplem4  22830  pm2mpmhmlem1  22839  monmat2matmon  22845  cpmidpmatlem3  22893  clm0vs  25141  plypf1  26265  lmodslmd  33192  r1p0  33605  ply1degltdimlem  33649  lbsdiflsp0  33653  fedgmullem2  33657  lshpkrlem1  39091  ldual0vs  39141  lclkrlem1  41488  lcd0vs  41597  baerlem3lem1  41689  baerlem5blem1  41691  hdmap14lem2a  41849  hdmap14lem4a  41853  hdmap14lem6  41855  hgmapval0  41874  selvvvval  42571  prjspersym  42593  prjspreln0  42595  prjspner1  42612  lmod0rng  48072  scmsuppss  48215  lmodvsmdi  48223  ply1mulgsumlem4  48234  lincval1  48264  lincvalsc0  48266  linc0scn0  48268  linc1  48270  ldepsprlem  48317
  Copyright terms: Public domain W3C validator