Theorem lmodgrp 20800

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 2731	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2731	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2731	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		eqid 2731	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2731	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6		eqid 2731	. . 3 ⊢ (+g‘(Scalar‘𝑊)) = (+g‘(Scalar‘𝑊))
7		eqid 2731	. . 3 ⊢ (.r‘(Scalar‘𝑊)) = (.r‘(Scalar‘𝑊))
8		eqid 2731	. . 3 ⊢ (1r‘(Scalar‘𝑊)) = (1r‘(Scalar‘𝑊))
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 20797	. 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 1541   ∈ wcel 2111  ∀wral 3047  ‘cfv 6481  (class class class)co 7346  Basecbs 17120  +_gcplusg 17161  ._rcmulr 17162  Scalarcsca 17164   ·_𝑠 cvsca 17165  Grpcgrp 18846  1_rcur 20099  Ringcrg 20151  LModclmod 20793

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rab 3396  df-v 3438  df-sbc 3737  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349  df-lmod 20795

This theorem is referenced by:  lmodgrpd  20803  lmodbn0  20804  lmodvacl  20808  lmodass  20809  lmodlcan  20810  lmod0vcl  20824  lmod0vlid  20825  lmod0vrid  20826  lmod0vid  20827  lmodvsmmulgdi  20830  lmodfopne  20833  lmodvnegcl  20836  lmodvnegid  20837  lmodvsubcl  20840  lmodcom  20841  lmodabl  20842  lmodvpncan  20848  lmodvnpcan  20849  lmodsubeq0  20854  lmodsubid  20855  lmodvsghm  20856  lmodprop2d  20857  lsssubg  20890  islss3  20892  lssacs  20900  prdslmodd  20902  lspsnneg  20939  lspsnsub  20940  lmodindp1  20947  lmodvsinv2  20971  islmhm2  20972  0lmhm  20974  idlmhm  20975  pwsdiaglmhm  20991  pwssplit3  20995  lspexch  21066  lspsolvlem  21079  ip0l  21573  ipsubdir  21579  ipsubdi  21580  ip2eq  21590  lsmcss  21629  dsmmlss  21681  frlm0  21691  frlmsubgval  21702  frlmplusgvalb  21706  frlmup1  21735  islindf4  21775  mplind  22005  matgrp  22345  tlmtgp  24111  clmgrp  24995  ncvspi  25083  cphtcphnm  25157  ipcau2  25161  tcphcphlem1  25162  tcphcph  25164  rrxnm  25318  rrxds  25320  pjthlem2  25365  lmodvslmhm  33030  eqgvscpbl  33315  imaslmod  33318  quslmod  33323  linds2eq  33346  lbslsat  33629  lindsunlem  33637  lbsdiflsp0  33639  dimkerim  33640  lclkrlem2m  41617  mapdpglem14  41783  baerlem3lem1  41805  baerlem5amN  41814  baerlem5bmN  41815  baerlem5abmN  41816  mapdh6bN  41835  mapdh6cN  41836  hdmap1l6b  41909  hdmap1l6c  41910  hdmap11  41946  frlmsnic  42632  kercvrlsm  43175  pwssplit4  43181  pwslnmlem2  43185  mendring  43280  zlmodzxzsub  48459  lmodvsmdi  48478  lincvalsng  48516  lincvalsc0  48521  linc0scn0  48523  linc1  48525  lcoel0  48528  lindslinindimp2lem4  48561  snlindsntor  48571  lincresunit3  48581