Theorem lmodgrp 20864

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 2740	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2740	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2740	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		eqid 2740	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2740	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6		eqid 2740	. . 3 ⊢ (+g‘(Scalar‘𝑊)) = (+g‘(Scalar‘𝑊))
7		eqid 2740	. . 3 ⊢ (.r‘(Scalar‘𝑊)) = (.r‘(Scalar‘𝑊))
8		eqid 2740	. . 3 ⊢ (1r‘(Scalar‘𝑊)) = (1r‘(Scalar‘𝑊))
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 20861	. 2 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ (Scalar‘𝑊) ∈ Ring ∧ ∀𝑞 ∈ (Base‘(Scalar‘𝑊))∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠 ‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑊))𝑟)( ·𝑠 ‘𝑊)𝑤) = ((𝑞( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠 ‘𝑊)𝑤) = (𝑞( ·𝑠 ‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤)) ∧ ((1r‘(Scalar‘𝑊))( ·𝑠 ‘𝑊)𝑤) = 𝑤))))
10	9	simp1bi 1151	1 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ∀wral 3054  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  +_gcplusg 17218  ._rcmulr 17219  Scalarcsca 17221   ·_𝑠 cvsca 17222  Grpcgrp 18907  1_rcur 20160  Ringcrg 20212  LModclmod 20857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-lmod 20859

This theorem is referenced by:  lmodgrpd  20867  lmodbn0  20868  lmodvacl  20872  lmodass  20873  lmodlcan  20874  lmod0vcl  20888  lmod0vlid  20889  lmod0vrid  20890  lmod0vid  20891  lmodvsmmulgdi  20894  lmodfopne  20897  lmodvnegcl  20900  lmodvnegid  20901  lmodvsubcl  20904  lmodcom  20905  lmodabl  20906  lmodvpncan  20912  lmodvnpcan  20913  lmodsubeq0  20918  lmodsubid  20919  lmodvsghm  20920  lmodprop2d  20921  lsssubg  20954  islss3  20956  lssacs  20964  prdslmodd  20966  lspsnneg  21003  lspsnsub  21004  lmodindp1  21011  lmodvsinv2  21034  islmhm2  21035  0lmhm  21037  idlmhm  21038  pwsdiaglmhm  21054  pwssplit3  21058  lspexch  21129  lspsolvlem  21142  ip0l  21618  ipsubdir  21624  ipsubdi  21625  ip2eq  21635  lsmcss  21674  dsmmlss  21726  frlm0  21736  frlmsubgval  21747  frlmplusgvalb  21751  frlmup1  21780  islindf4  21820  mplind  22053  matgrp  22420  tlmtgp  24186  clmgrp  25060  ncvspi  25148  cphtcphnm  25222  ipcau2  25226  tcphcphlem1  25227  tcphcph  25229  rrxnm  25383  rrxds  25385  pjthlem2  25430  lmodvslmhm  33138  eqgvscpbl  33440  imaslmod  33443  quslmod  33448  linds2eq  33471  lbslsat  33807  lindsunlem  33815  lbsdiflsp0  33817  dimkerim  33818  lclkrlem2m  42018  mapdpglem14  42184  baerlem3lem1  42206  baerlem5amN  42215  baerlem5bmN  42216  baerlem5abmN  42217  mapdh6bN  42236  mapdh6cN  42237  hdmap1l6b  42310  hdmap1l6c  42311  hdmap11  42347  frlmsnic  43033  kercvrlsm  43535  pwssplit4  43541  pwslnmlem2  43545  mendring  43640  zlmodzxzsub  48858  lmodvsmdi  48877  lincvalsng  48914  lincvalsc0  48919  linc0scn0  48921  linc1  48923  lcoel0  48926  lindslinindimp2lem4  48959  snlindsntor  48969  lincresunit3  48979