MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmod0vs Structured version   Visualization version   GIF version
Theorem lmod0vs 20497
Description: Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 30250 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 20471 . . . . . . 7 (π‘Š ∈ LMod β†’ 𝐹 ∈ Ring)
43adantr 481 . . . . . 6 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ 𝐹 ∈ Ring)
5 eqid 2732 . . . . . . 7 (Baseβ€˜πΉ) = (Baseβ€˜πΉ)
6 lmod0vs.o . . . . . . 7 𝑂 = (0gβ€˜πΉ)
75, 6ring0cl 20077 . . . . . 6 (𝐹 ∈ Ring β†’ 𝑂 ∈ (Baseβ€˜πΉ))
84, 7syl 17 . . . . 5 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ 𝑂 ∈ (Baseβ€˜πΉ))
9 simpr 485 . . . . 5 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ 𝑋 ∈ 𝑉)
10 lmod0vs.v . . . . . 6 𝑉 = (Baseβ€˜π‘Š)
11 eqid 2732 . . . . . 6 (+gβ€˜π‘Š) = (+gβ€˜π‘Š)
12 lmod0vs.s . . . . . 6 Β· = ( ·𝑠 β€˜π‘Š)
13 eqid 2732 . . . . . 6 (+gβ€˜πΉ) = (+gβ€˜πΉ)
1410, 11, 2, 12, 5, 13lmodvsdir 20488 . . . . 5 ((π‘Š ∈ LMod ∧ (𝑂 ∈ (Baseβ€˜πΉ) ∧ 𝑂 ∈ (Baseβ€˜πΉ) ∧ 𝑋 ∈ 𝑉)) β†’ ((𝑂(+gβ€˜πΉ)𝑂) Β· 𝑋) = ((𝑂 Β· 𝑋)(+gβ€˜π‘Š)(𝑂 Β· 𝑋)))
151, 8, 8, 9, 14syl13anc 1372 . . . 4 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ ((𝑂(+gβ€˜πΉ)𝑂) Β· 𝑋) = ((𝑂 Β· 𝑋)(+gβ€˜π‘Š)(𝑂 Β· 𝑋)))
16 ringgrp 20054 . . . . . . 7 (𝐹 ∈ Ring β†’ 𝐹 ∈ Grp)
174, 16syl 17 . . . . . 6 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ 𝐹 ∈ Grp)
185, 13, 6grplid 18848 . . . . . 6 ((𝐹 ∈ Grp ∧ 𝑂 ∈ (Baseβ€˜πΉ)) β†’ (𝑂(+gβ€˜πΉ)𝑂) = 𝑂)
1917, 8, 18syl2anc 584 . . . . 5 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ (𝑂(+gβ€˜πΉ)𝑂) = 𝑂)
2019oveq1d 7420 . . . 4 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ ((𝑂(+gβ€˜πΉ)𝑂) Β· 𝑋) = (𝑂 Β· 𝑋))
2115, 20eqtr3d 2774 . . 3 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ ((𝑂 Β· 𝑋)(+gβ€˜π‘Š)(𝑂 Β· 𝑋)) = (𝑂 Β· 𝑋))
2210, 2, 12, 5lmodvscl 20481 . . . . 5 ((π‘Š ∈ LMod ∧ 𝑂 ∈ (Baseβ€˜πΉ) ∧ 𝑋 ∈ 𝑉) β†’ (𝑂 Β· 𝑋) ∈ 𝑉)
231, 8, 9, 22syl3anc 1371 . . . 4 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ (𝑂 Β· 𝑋) ∈ 𝑉)
24 lmod0vs.z . . . . 5 0 = (0gβ€˜π‘Š)
2510, 11, 24lmod0vid 20496 . . . 4 ((π‘Š ∈ LMod ∧ (𝑂 Β· 𝑋) ∈ 𝑉) β†’ (((𝑂 Β· 𝑋)(+gβ€˜π‘Š)(𝑂 Β· 𝑋)) = (𝑂 Β· 𝑋) ↔ 0 = (𝑂 Β· 𝑋)))
2623, 25syldan 591 . . 3 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ (((𝑂 Β· 𝑋)(+gβ€˜π‘Š)(𝑂 Β· 𝑋)) = (𝑂 Β· 𝑋) ↔ 0 = (𝑂 Β· 𝑋)))
2721, 26mpbid 231 . 2 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ 0 = (𝑂 Β· 𝑋))
2827eqcomd 2738 1 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ (𝑂 Β· 𝑋) = 0 )
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  β€˜cfv 6540  (class class class)co 7405  Basecbs 17140  +gcplusg 17193  Scalarcsca 17196   ·𝑠 cvsca 17197  0gc0g 17381  Grpcgrp 18815  Ringcrg 20049  LModclmod 20463
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-iota 6492  df-fun 6542  df-fv 6548  df-riota 7361  df-ov 7408  df-0g 17383  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-grp 18818  df-ring 20051  df-lmod 20465
This theorem is referenced by:  lmodvs0  20498  lmodvsmmulgdi  20499  lcomfsupp  20504  lmodvneg1  20507  mptscmfsupp0  20529  lvecvs0or  20713  lssvs0or  20715  lspsneleq  20720  lspdisj  20730  lspfixed  20733  lspexch  20734  lspsolvlem  20747  lspsolv  20748  uvcresum  21339  frlmsslsp  21342  frlmup1  21344  frlmup2  21345  ascl0  21429  mplcoe1  21583  mplbas2  21588  ply10s0  21769  ply1scl0OLD  21804  gsummoncoe1  21819  pmatcollpwscmatlem1  22282  idpm2idmp  22294  mp2pm2mplem4  22302  pm2mpmhmlem1  22311  monmat2matmon  22317  cpmidpmatlem3  22365  clm0vs  24602  plypf1  25717  lmodslmd  32336  evls1fpws  32634  ply1degltdimlem  32695  lbsdiflsp0  32699  fedgmullem2  32703  lshpkrlem1  37968  ldual0vs  38018  lclkrlem1  40365  lcd0vs  40474  baerlem3lem1  40566  baerlem5blem1  40568  hdmap14lem2a  40726  hdmap14lem4a  40730  hdmap14lem6  40732  hgmapval0  40751  selvvvval  41154  prjspersym  41345  prjspreln0  41347  prjspner1  41364  lmod0rng  46628  scmsuppss  47001  lmodvsmdi  47011  ply1mulgsumlem4  47023  lincval1  47053  lincvalsc0  47055  linc0scn0  47057  linc1  47059  ldepsprlem  47106
  Copyright terms: Public domain W3C validator