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

Theorem lmodgrp 19638
Description: A left module is a group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.)
Assertion
Ref Expression
lmodgrp (𝑊 ∈ LMod → 𝑊 ∈ Grp)

Proof of Theorem lmodgrp
Dummy variables 𝑟 𝑞 𝑤 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2801 . . 3 (Base‘𝑊) = (Base‘𝑊)
2 eqid 2801 . . 3 (+g𝑊) = (+g𝑊)
3 eqid 2801 . . 3 ( ·𝑠𝑊) = ( ·𝑠𝑊)
4 eqid 2801 . . 3 (Scalar‘𝑊) = (Scalar‘𝑊)
5 eqid 2801 . . 3 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6 eqid 2801 . . 3 (+g‘(Scalar‘𝑊)) = (+g‘(Scalar‘𝑊))
7 eqid 2801 . . 3 (.r‘(Scalar‘𝑊)) = (.r‘(Scalar‘𝑊))
8 eqid 2801 . . 3 (1r‘(Scalar‘𝑊)) = (1r‘(Scalar‘𝑊))
91, 2, 3, 4, 5, 6, 7, 8islmod 19635 . 2 (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ (Scalar‘𝑊) ∈ Ring ∧ ∀𝑞 ∈ (Base‘(Scalar‘𝑊))∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠𝑊)(𝑤(+g𝑊)𝑥)) = ((𝑟( ·𝑠𝑊)𝑤)(+g𝑊)(𝑟( ·𝑠𝑊)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑊))𝑟)( ·𝑠𝑊)𝑤) = ((𝑞( ·𝑠𝑊)𝑤)(+g𝑊)(𝑟( ·𝑠𝑊)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠𝑊)𝑤) = (𝑞( ·𝑠𝑊)(𝑟( ·𝑠𝑊)𝑤)) ∧ ((1r‘(Scalar‘𝑊))( ·𝑠𝑊)𝑤) = 𝑤))))
109simp1bi 1142 1 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084   = wceq 1538  wcel 2112  wral 3109  cfv 6328  (class class class)co 7139  Basecbs 16479  +gcplusg 16561  .rcmulr 16562  Scalarcsca 16564   ·𝑠 cvsca 16565  Grpcgrp 18099  1rcur 19248  Ringcrg 19294  LModclmod 19631
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-nul 5177
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 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-ov 7142  df-lmod 19633
This theorem is referenced by:  lmodbn0  19641  lmodvacl  19645  lmodass  19646  lmodlcan  19647  lmod0vcl  19660  lmod0vlid  19661  lmod0vrid  19662  lmod0vid  19663  lmodvsmmulgdi  19666  lmodfopne  19669  lmodvnegcl  19672  lmodvnegid  19673  lmodvsubcl  19676  lmodcom  19677  lmodabl  19678  lmodvpncan  19684  lmodvnpcan  19685  lmodsubeq0  19690  lmodsubid  19691  lmodvsghm  19692  lmodprop2d  19693  lsssubg  19726  islss3  19728  lssacs  19736  prdslmodd  19738  lspsnneg  19775  lspsnsub  19776  lmodindp1  19783  lmodvsinv2  19806  islmhm2  19807  0lmhm  19809  idlmhm  19810  pwsdiaglmhm  19826  pwssplit3  19830  lspexch  19898  lspsolvlem  19911  ip0l  20329  ipsubdir  20335  ipsubdi  20336  ip2eq  20346  lsmcss  20385  dsmmlss  20437  frlm0  20447  frlmsubgval  20458  frlmplusgvalb  20462  frlmup1  20491  islindf4  20531  mplind  20745  matgrp  21039  tlmtgp  22805  clmgrp  23677  ncvspi  23765  cphtcphnm  23838  ipcau2  23842  tcphcphlem1  23843  tcphcph  23845  rrxnm  23999  rrxds  24001  pjthlem2  24046  lmodvslmhm  30739  eqgvscpbl  30974  imaslmod  30977  quslmod  30978  linds2eq  30999  lbslsat  31106  lindsunlem  31112  lbsdiflsp0  31114  dimkerim  31115  lclkrlem2m  38814  mapdpglem14  38980  baerlem3lem1  39002  baerlem5amN  39011  baerlem5bmN  39012  baerlem5abmN  39013  mapdh6bN  39032  mapdh6cN  39033  hdmap1l6b  39106  hdmap1l6c  39107  hdmap11  39143  lmodgrpd  39440  lvecgrp  39441  frlmsnic  39446  kercvrlsm  40020  pwssplit4  40026  pwslnmlem2  40030  mendring  40129  zlmodzxzsub  44755  lmodvsmdi  44777  lincvalsng  44818  lincvalsc0  44823  linc0scn0  44825  linc1  44827  lcoel0  44830  lindslinindimp2lem4  44863  snlindsntor  44873  lincresunit3  44883
  Copyright terms: Public domain W3C validator