Theorem lmodgrp 20202

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.

Step	Hyp	Ref	Expression
1		eqid 2737	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2737	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2737	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		eqid 2737	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2737	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6		eqid 2737	. . 3 ⊢ (+g‘(Scalar‘𝑊)) = (+g‘(Scalar‘𝑊))
7		eqid 2737	. . 3 ⊢ (.r‘(Scalar‘𝑊)) = (.r‘(Scalar‘𝑊))
8		eqid 2737	. . 3 ⊢ (1r‘(Scalar‘𝑊)) = (1r‘(Scalar‘𝑊))
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 20199	. 2 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ (Scalar‘𝑊) ∈ Ring ∧ ∀𝑞 ∈ (Base‘(Scalar‘𝑊))∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠 ‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑊))𝑟)( ·𝑠 ‘𝑊)𝑤) = ((𝑞( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠 ‘𝑊)𝑤) = (𝑞( ·𝑠 ‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤)) ∧ ((1r‘(Scalar‘𝑊))( ·𝑠 ‘𝑊)𝑤) = 𝑤))))
10	9	simp1bi 1144	1 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  ∀wral 3062  ‘cfv 6465  (class class class)co 7315  Basecbs 16982  +_gcplusg 17032  ._rcmulr 17033  Scalarcsca 17035   ·_𝑠 cvsca 17036  Grpcgrp 18646  1_rcur 19805  Ringcrg 19851  LModclmod 20195

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708  ax-nul 5245

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-ral 3063  df-rab 3405  df-v 3443  df-sbc 3727  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-iota 6417  df-fv 6473  df-ov 7318  df-lmod 20197

This theorem is referenced by:  lmodbn0  20205  lmodvacl  20209  lmodass  20210  lmodlcan  20211  lmod0vcl  20224  lmod0vlid  20225  lmod0vrid  20226  lmod0vid  20227  lmodvsmmulgdi  20230  lmodfopne  20233  lmodvnegcl  20236  lmodvnegid  20237  lmodvsubcl  20240  lmodcom  20241  lmodabl  20242  lmodvpncan  20248  lmodvnpcan  20249  lmodsubeq0  20254  lmodsubid  20255  lmodvsghm  20256  lmodprop2d  20257  lsssubg  20291  islss3  20293  lssacs  20301  prdslmodd  20303  lspsnneg  20340  lspsnsub  20341  lmodindp1  20348  lmodvsinv2  20371  islmhm2  20372  0lmhm  20374  idlmhm  20375  pwsdiaglmhm  20391  pwssplit3  20395  lspexch  20463  lspsolvlem  20476  ip0l  20913  ipsubdir  20919  ipsubdi  20920  ip2eq  20930  lsmcss  20969  dsmmlss  21023  frlm0  21033  frlmsubgval  21044  frlmplusgvalb  21048  frlmup1  21077  islindf4  21117  mplind  21350  matgrp  21651  tlmtgp  23419  clmgrp  24303  ncvspi  24392  cphtcphnm  24466  ipcau2  24470  tcphcphlem1  24471  tcphcph  24473  rrxnm  24627  rrxds  24629  pjthlem2  24674  lmodvslmhm  31418  eqgvscpbl  31654  imaslmod  31657  quslmod  31658  linds2eq  31680  lbslsat  31805  lindsunlem  31811  lbsdiflsp0  31813  dimkerim  31814  lclkrlem2m  39738  mapdpglem14  39904  baerlem3lem1  39926  baerlem5amN  39935  baerlem5bmN  39936  baerlem5abmN  39937  mapdh6bN  39956  mapdh6cN  39957  hdmap1l6b  40030  hdmap1l6c  40031  hdmap11  40067  lmodgrpd  40459  lvecgrp  40460  frlmsnic  40466  kercvrlsm  41112  pwssplit4  41118  pwslnmlem2  41122  mendring  41221  zlmodzxzsub  45948  lmodvsmdi  45970  lincvalsng  46009  lincvalsc0  46014  linc0scn0  46016  linc1  46018  lcoel0  46021  lindslinindimp2lem4  46054  snlindsntor  46064  lincresunit3  46074