Theorem lmodgrp 20780

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3045  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  +_gcplusg 17227  ._rcmulr 17228  Scalarcsca 17230   ·_𝑠 cvsca 17231  Grpcgrp 18872  1_rcur 20097  Ringcrg 20149  LModclmod 20773

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-lmod 20775

This theorem is referenced by:  lmodgrpd  20783  lmodbn0  20784  lmodvacl  20788  lmodass  20789  lmodlcan  20790  lmod0vcl  20804  lmod0vlid  20805  lmod0vrid  20806  lmod0vid  20807  lmodvsmmulgdi  20810  lmodfopne  20813  lmodvnegcl  20816  lmodvnegid  20817  lmodvsubcl  20820  lmodcom  20821  lmodabl  20822  lmodvpncan  20828  lmodvnpcan  20829  lmodsubeq0  20834  lmodsubid  20835  lmodvsghm  20836  lmodprop2d  20837  lsssubg  20870  islss3  20872  lssacs  20880  prdslmodd  20882  lspsnneg  20919  lspsnsub  20920  lmodindp1  20927  lmodvsinv2  20951  islmhm2  20952  0lmhm  20954  idlmhm  20955  pwsdiaglmhm  20971  pwssplit3  20975  lspexch  21046  lspsolvlem  21059  ip0l  21552  ipsubdir  21558  ipsubdi  21559  ip2eq  21569  lsmcss  21608  dsmmlss  21660  frlm0  21670  frlmsubgval  21681  frlmplusgvalb  21685  frlmup1  21714  islindf4  21754  mplind  21984  matgrp  22324  tlmtgp  24090  clmgrp  24975  ncvspi  25063  cphtcphnm  25137  ipcau2  25141  tcphcphlem1  25142  tcphcph  25144  rrxnm  25298  rrxds  25300  pjthlem2  25345  lmodvslmhm  32997  eqgvscpbl  33328  imaslmod  33331  quslmod  33336  linds2eq  33359  lbslsat  33619  lindsunlem  33627  lbsdiflsp0  33629  dimkerim  33630  lclkrlem2m  41520  mapdpglem14  41686  baerlem3lem1  41708  baerlem5amN  41717  baerlem5bmN  41718  baerlem5abmN  41719  mapdh6bN  41738  mapdh6cN  41739  hdmap1l6b  41812  hdmap1l6c  41813  hdmap11  41849  frlmsnic  42535  kercvrlsm  43079  pwssplit4  43085  pwslnmlem2  43089  mendring  43184  zlmodzxzsub  48352  lmodvsmdi  48371  lincvalsng  48409  lincvalsc0  48414  linc0scn0  48416  linc1  48418  lcoel0  48421  lindslinindimp2lem4  48454  snlindsntor  48464  lincresunit3  48474