MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmod0vs Structured version   Visualization version   GIF version
Theorem lmod0vs 20649
Description: Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 30530 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 481 . . . . 5 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ π‘Š ∈ LMod)
2 lmod0vs.f . . . . . . . 8 𝐹 = (Scalarβ€˜π‘Š)
32lmodring 20622 . . . . . . 7 (π‘Š ∈ LMod β†’ 𝐹 ∈ Ring)
43adantr 479 . . . . . 6 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ 𝐹 ∈ Ring)
5 eqid 2730 . . . . . . 7 (Baseβ€˜πΉ) = (Baseβ€˜πΉ)
6 lmod0vs.o . . . . . . 7 𝑂 = (0gβ€˜πΉ)
75, 6ring0cl 20155 . . . . . 6 (𝐹 ∈ Ring β†’ 𝑂 ∈ (Baseβ€˜πΉ))
84, 7syl 17 . . . . 5 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ 𝑂 ∈ (Baseβ€˜πΉ))
9 simpr 483 . . . . 5 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ 𝑋 ∈ 𝑉)
10 lmod0vs.v . . . . . 6 𝑉 = (Baseβ€˜π‘Š)
11 eqid 2730 . . . . . 6 (+gβ€˜π‘Š) = (+gβ€˜π‘Š)
12 lmod0vs.s . . . . . 6 Β· = ( ·𝑠 β€˜π‘Š)
13 eqid 2730 . . . . . 6 (+gβ€˜πΉ) = (+gβ€˜πΉ)
1410, 11, 2, 12, 5, 13lmodvsdir 20640 . . . . 5 ((π‘Š ∈ LMod ∧ (𝑂 ∈ (Baseβ€˜πΉ) ∧ 𝑂 ∈ (Baseβ€˜πΉ) ∧ 𝑋 ∈ 𝑉)) β†’ ((𝑂(+gβ€˜πΉ)𝑂) Β· 𝑋) = ((𝑂 Β· 𝑋)(+gβ€˜π‘Š)(𝑂 Β· 𝑋)))
151, 8, 8, 9, 14syl13anc 1370 . . . 4 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ ((𝑂(+gβ€˜πΉ)𝑂) Β· 𝑋) = ((𝑂 Β· 𝑋)(+gβ€˜π‘Š)(𝑂 Β· 𝑋)))
16 ringgrp 20132 . . . . . . 7 (𝐹 ∈ Ring β†’ 𝐹 ∈ Grp)
174, 16syl 17 . . . . . 6 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ 𝐹 ∈ Grp)
185, 13, 6grplid 18888 . . . . . 6 ((𝐹 ∈ Grp ∧ 𝑂 ∈ (Baseβ€˜πΉ)) β†’ (𝑂(+gβ€˜πΉ)𝑂) = 𝑂)
1917, 8, 18syl2anc 582 . . . . 5 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ (𝑂(+gβ€˜πΉ)𝑂) = 𝑂)
2019oveq1d 7426 . . . 4 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ ((𝑂(+gβ€˜πΉ)𝑂) Β· 𝑋) = (𝑂 Β· 𝑋))
2115, 20eqtr3d 2772 . . 3 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ ((𝑂 Β· 𝑋)(+gβ€˜π‘Š)(𝑂 Β· 𝑋)) = (𝑂 Β· 𝑋))
2210, 2, 12, 5lmodvscl 20632 . . . . 5 ((π‘Š ∈ LMod ∧ 𝑂 ∈ (Baseβ€˜πΉ) ∧ 𝑋 ∈ 𝑉) β†’ (𝑂 Β· 𝑋) ∈ 𝑉)
231, 8, 9, 22syl3anc 1369 . . . 4 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ (𝑂 Β· 𝑋) ∈ 𝑉)
24 lmod0vs.z . . . . 5 0 = (0gβ€˜π‘Š)
2510, 11, 24lmod0vid 20648 . . . 4 ((π‘Š ∈ LMod ∧ (𝑂 Β· 𝑋) ∈ 𝑉) β†’ (((𝑂 Β· 𝑋)(+gβ€˜π‘Š)(𝑂 Β· 𝑋)) = (𝑂 Β· 𝑋) ↔ 0 = (𝑂 Β· 𝑋)))
2623, 25syldan 589 . . 3 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ (((𝑂 Β· 𝑋)(+gβ€˜π‘Š)(𝑂 Β· 𝑋)) = (𝑂 Β· 𝑋) ↔ 0 = (𝑂 Β· 𝑋)))
2721, 26mpbid 231 . 2 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ 0 = (𝑂 Β· 𝑋))
2827eqcomd 2736 1 ((π‘Š ∈ LMod ∧ 𝑋 ∈ 𝑉) β†’ (𝑂 Β· 𝑋) = 0 )
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104  β€˜cfv 6542  (class class class)co 7411  Basecbs 17148  +gcplusg 17201  Scalarcsca 17204   ·𝑠 cvsca 17205  0gc0g 17389  Grpcgrp 18855  Ringcrg 20127  LModclmod 20614
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  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 6494  df-fun 6544  df-fv 6550  df-riota 7367  df-ov 7414  df-0g 17391  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-grp 18858  df-ring 20129  df-lmod 20616
This theorem is referenced by:  lmodvs0  20650  lmodvsmmulgdi  20651  lcomfsupp  20656  lmodvneg1  20659  mptscmfsupp0  20681  lvecvs0or  20866  lssvs0or  20868  lspsneleq  20873  lspdisj  20883  lspfixed  20886  lspexch  20887  lspsolvlem  20900  lspsolv  20901  uvcresum  21567  frlmsslsp  21570  frlmup1  21572  frlmup2  21573  ascl0  21657  mplcoe1  21811  mplbas2  21816  ply10s0  21998  ply1scl0OLD  22033  gsummoncoe1  22048  pmatcollpwscmatlem1  22511  idpm2idmp  22523  mp2pm2mplem4  22531  pm2mpmhmlem1  22540  monmat2matmon  22546  cpmidpmatlem3  22594  clm0vs  24842  plypf1  25961  lmodslmd  32619  evls1fpws  32920  r1p0  32951  ply1degltdimlem  32995  lbsdiflsp0  32999  fedgmullem2  33003  lshpkrlem1  38283  ldual0vs  38333  lclkrlem1  40680  lcd0vs  40789  baerlem3lem1  40881  baerlem5blem1  40883  hdmap14lem2a  41041  hdmap14lem4a  41045  hdmap14lem6  41047  hgmapval0  41066  selvvvval  41459  prjspersym  41651  prjspreln0  41653  prjspner1  41670  lmod0rng  46908  scmsuppss  47136  lmodvsmdi  47146  ply1mulgsumlem4  47157  lincval1  47187  lincvalsc0  47189  linc0scn0  47191  linc1  47193  ldepsprlem  47240
  Copyright terms: Public domain W3C validator