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

Theorem lmodgrp 19072
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 2760 . . 3 (Base‘𝑊) = (Base‘𝑊)
2 eqid 2760 . . 3 (+g𝑊) = (+g𝑊)
3 eqid 2760 . . 3 ( ·𝑠𝑊) = ( ·𝑠𝑊)
4 eqid 2760 . . 3 (Scalar‘𝑊) = (Scalar‘𝑊)
5 eqid 2760 . . 3 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6 eqid 2760 . . 3 (+g‘(Scalar‘𝑊)) = (+g‘(Scalar‘𝑊))
7 eqid 2760 . . 3 (.r‘(Scalar‘𝑊)) = (.r‘(Scalar‘𝑊))
8 eqid 2760 . . 3 (1r‘(Scalar‘𝑊)) = (1r‘(Scalar‘𝑊))
91, 2, 3, 4, 5, 6, 7, 8islmod 19069 . 2 (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ (Scalar‘𝑊) ∈ Ring ∧ ∀𝑞 ∈ (Base‘(Scalar‘𝑊))∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠𝑊)(𝑤(+g𝑊)𝑥)) = ((𝑟( ·𝑠𝑊)𝑤)(+g𝑊)(𝑟( ·𝑠𝑊)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑊))𝑟)( ·𝑠𝑊)𝑤) = ((𝑞( ·𝑠𝑊)𝑤)(+g𝑊)(𝑟( ·𝑠𝑊)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠𝑊)𝑤) = (𝑞( ·𝑠𝑊)(𝑟( ·𝑠𝑊)𝑤)) ∧ ((1r‘(Scalar‘𝑊))( ·𝑠𝑊)𝑤) = 𝑤))))
109simp1bi 1140 1 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072   = wceq 1632  wcel 2139  wral 3050  cfv 6049  (class class class)co 6813  Basecbs 16059  +gcplusg 16143  .rcmulr 16144  Scalarcsca 16146   ·𝑠 cvsca 16147  Grpcgrp 17623  1rcur 18701  Ringcrg 18747  LModclmod 19065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-nul 4941
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6816  df-lmod 19067
This theorem is referenced by:  lmodbn0  19075  lmodvacl  19079  lmodass  19080  lmodlcan  19081  lmod0vcl  19094  lmod0vlid  19095  lmod0vrid  19096  lmod0vid  19097  lmodvsmmulgdi  19100  lmodfopne  19103  lmodvnegcl  19106  lmodvnegid  19107  lmodvsubcl  19110  lmodcom  19111  lmodabl  19112  lmodvpncan  19118  lmodvnpcan  19119  lmodsubeq0  19124  lmodsubid  19125  lmodvsghm  19126  lmodprop2d  19127  lsssubg  19159  islss3  19161  lssacs  19169  prdslmodd  19171  lspsnneg  19208  lspsnsub  19209  lmodindp1  19216  lmodvsinv2  19239  islmhm2  19240  0lmhm  19242  idlmhm  19243  pwsdiaglmhm  19259  pwssplit3  19263  lspexch  19331  lspsolvlem  19344  mplind  19704  ip0l  20183  ipsubdir  20189  ipsubdi  20190  ip2eq  20200  lsmcss  20238  dsmmlss  20290  frlm0  20300  frlmsubgval  20310  frlmup1  20339  islindf4  20379  matgrp  20438  tlmtgp  22200  clmgrp  23068  ncvspi  23156  cphtchnm  23229  ipcau2  23233  tchcphlem1  23234  tchcph  23236  rrxnm  23379  rrxds  23381  pjthlem2  23409  lclkrlem2m  37310  mapdpglem14  37476  baerlem3lem1  37498  baerlem5amN  37507  baerlem5bmN  37508  baerlem5abmN  37509  mapdh6bN  37528  mapdh6cN  37529  hdmap1l6b  37603  hdmap1l6c  37604  hdmap1neglem1N  37619  hdmap11  37642  kercvrlsm  38155  pwssplit4  38161  pwslnmlem2  38165  mendring  38264  zlmodzxzsub  42648  lmodvsmdi  42673  lincvalsng  42715  lincvalsc0  42720  linc0scn0  42722  linc1  42724  lcoel0  42727  lindslinindimp2lem4  42760  snlindsntor  42770  lincresunit3  42780
  Copyright terms: Public domain W3C validator