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

Theorem lmod0vs 19642
Description: Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 28771 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 486 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝑊 ∈ LMod)
2 lmod0vs.f . . . . . . . 8 𝐹 = (Scalar‘𝑊)
32lmodring 19617 . . . . . . 7 (𝑊 ∈ LMod → 𝐹 ∈ Ring)
43adantr 484 . . . . . 6 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝐹 ∈ Ring)
5 eqid 2821 . . . . . . 7 (Base‘𝐹) = (Base‘𝐹)
6 lmod0vs.o . . . . . . 7 𝑂 = (0g𝐹)
75, 6ring0cl 19297 . . . . . 6 (𝐹 ∈ Ring → 𝑂 ∈ (Base‘𝐹))
84, 7syl 17 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝑂 ∈ (Base‘𝐹))
9 simpr 488 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝑋𝑉)
10 lmod0vs.v . . . . . 6 𝑉 = (Base‘𝑊)
11 eqid 2821 . . . . . 6 (+g𝑊) = (+g𝑊)
12 lmod0vs.s . . . . . 6 · = ( ·𝑠𝑊)
13 eqid 2821 . . . . . 6 (+g𝐹) = (+g𝐹)
1410, 11, 2, 12, 5, 13lmodvsdir 19633 . . . . 5 ((𝑊 ∈ LMod ∧ (𝑂 ∈ (Base‘𝐹) ∧ 𝑂 ∈ (Base‘𝐹) ∧ 𝑋𝑉)) → ((𝑂(+g𝐹)𝑂) · 𝑋) = ((𝑂 · 𝑋)(+g𝑊)(𝑂 · 𝑋)))
151, 8, 8, 9, 14syl13anc 1369 . . . 4 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ((𝑂(+g𝐹)𝑂) · 𝑋) = ((𝑂 · 𝑋)(+g𝑊)(𝑂 · 𝑋)))
16 ringgrp 19280 . . . . . . 7 (𝐹 ∈ Ring → 𝐹 ∈ Grp)
174, 16syl 17 . . . . . 6 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 𝐹 ∈ Grp)
185, 13, 6grplid 18111 . . . . . 6 ((𝐹 ∈ Grp ∧ 𝑂 ∈ (Base‘𝐹)) → (𝑂(+g𝐹)𝑂) = 𝑂)
1917, 8, 18syl2anc 587 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (𝑂(+g𝐹)𝑂) = 𝑂)
2019oveq1d 7145 . . . 4 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ((𝑂(+g𝐹)𝑂) · 𝑋) = (𝑂 · 𝑋))
2115, 20eqtr3d 2858 . . 3 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → ((𝑂 · 𝑋)(+g𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋))
2210, 2, 12, 5lmodvscl 19626 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑂 ∈ (Base‘𝐹) ∧ 𝑋𝑉) → (𝑂 · 𝑋) ∈ 𝑉)
231, 8, 9, 22syl3anc 1368 . . . 4 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (𝑂 · 𝑋) ∈ 𝑉)
24 lmod0vs.z . . . . 5 0 = (0g𝑊)
2510, 11, 24lmod0vid 19641 . . . 4 ((𝑊 ∈ LMod ∧ (𝑂 · 𝑋) ∈ 𝑉) → (((𝑂 · 𝑋)(+g𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋) ↔ 0 = (𝑂 · 𝑋)))
2623, 25syldan 594 . . 3 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (((𝑂 · 𝑋)(+g𝑊)(𝑂 · 𝑋)) = (𝑂 · 𝑋) ↔ 0 = (𝑂 · 𝑋)))
2721, 26mpbid 235 . 2 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → 0 = (𝑂 · 𝑋))
2827eqcomd 2827 1 ((𝑊 ∈ LMod ∧ 𝑋𝑉) → (𝑂 · 𝑋) = 0 )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  cfv 6328  (class class class)co 7130  Basecbs 16461  +gcplusg 16543  Scalarcsca 16546   ·𝑠 cvsca 16547  0gc0g 16691  Grpcgrp 18081  Ringcrg 19275  LModclmod 19609
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-ral 3131  df-rex 3132  df-reu 3133  df-rmo 3134  df-rab 3135  df-v 3473  df-sbc 3750  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-opab 5102  df-mpt 5120  df-id 5433  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-iota 6287  df-fun 6330  df-fv 6336  df-riota 7088  df-ov 7133  df-0g 16693  df-mgm 17830  df-sgrp 17879  df-mnd 17890  df-grp 18084  df-ring 19277  df-lmod 19611
This theorem is referenced by:  lmodvs0  19643  lmodvsmmulgdi  19644  lcomfsupp  19649  lmodvneg1  19652  mptscmfsupp0  19674  lvecvs0or  19855  lssvs0or  19857  lspsneleq  19862  lspdisj  19872  lspfixed  19875  lspexch  19876  lspsolvlem  19889  lspsolv  19890  ascl0  20088  mplcoe1  20221  mplbas2  20226  ply10s0  20399  ply1scl0  20433  gsummoncoe1  20447  uvcresum  20912  frlmsslsp  20915  frlmup1  20917  frlmup2  20918  pmatcollpwscmatlem1  21372  idpm2idmp  21384  mp2pm2mplem4  21392  pm2mpmhmlem1  21401  monmat2matmon  21407  cpmidpmatlem3  21455  clm0vs  23678  plypf1  24787  lmodslmd  30839  lbsdiflsp0  31032  fedgmullem2  31036  lshpkrlem1  36284  ldual0vs  36334  lclkrlem1  38680  lcd0vs  38789  baerlem3lem1  38881  baerlem5blem1  38883  hdmap14lem2a  39041  hdmap14lem4a  39045  hdmap14lem6  39047  hgmapval0  39066  prjspersym  39396  prjspreln0  39398  lmod0rng  44284  scmsuppss  44565  lmodvsmdi  44575  ply1mulgsumlem4  44588  lincval1  44619  lincvalsc0  44621  linc0scn0  44623  linc1  44625  ldepsprlem  44672
  Copyright terms: Public domain W3C validator