Theorem lmodgrp 20822

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 2735	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2735	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2735	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		eqid 2735	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2735	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6		eqid 2735	. . 3 ⊢ (+g‘(Scalar‘𝑊)) = (+g‘(Scalar‘𝑊))
7		eqid 2735	. . 3 ⊢ (.r‘(Scalar‘𝑊)) = (.r‘(Scalar‘𝑊))
8		eqid 2735	. . 3 ⊢ (1r‘(Scalar‘𝑊)) = (1r‘(Scalar‘𝑊))
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 20819	. 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 2108  ∀wral 3051  ‘cfv 6530  (class class class)co 7403  Basecbs 17226  +_gcplusg 17269  ._rcmulr 17270  Scalarcsca 17272   ·_𝑠 cvsca 17273  Grpcgrp 18914  1_rcur 20139  Ringcrg 20191  LModclmod 20815

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-lmod 20817

This theorem is referenced by:  lmodgrpd  20825  lmodbn0  20826  lmodvacl  20830  lmodass  20831  lmodlcan  20832  lmod0vcl  20846  lmod0vlid  20847  lmod0vrid  20848  lmod0vid  20849  lmodvsmmulgdi  20852  lmodfopne  20855  lmodvnegcl  20858  lmodvnegid  20859  lmodvsubcl  20862  lmodcom  20863  lmodabl  20864  lmodvpncan  20870  lmodvnpcan  20871  lmodsubeq0  20876  lmodsubid  20877  lmodvsghm  20878  lmodprop2d  20879  lsssubg  20912  islss3  20914  lssacs  20922  prdslmodd  20924  lspsnneg  20961  lspsnsub  20962  lmodindp1  20969  lmodvsinv2  20993  islmhm2  20994  0lmhm  20996  idlmhm  20997  pwsdiaglmhm  21013  pwssplit3  21017  lspexch  21088  lspsolvlem  21101  ip0l  21594  ipsubdir  21600  ipsubdi  21601  ip2eq  21611  lsmcss  21650  dsmmlss  21702  frlm0  21712  frlmsubgval  21723  frlmplusgvalb  21727  frlmup1  21756  islindf4  21796  mplind  22026  matgrp  22366  tlmtgp  24132  clmgrp  25017  ncvspi  25106  cphtcphnm  25180  ipcau2  25184  tcphcphlem1  25185  tcphcph  25187  rrxnm  25341  rrxds  25343  pjthlem2  25388  lmodvslmhm  32990  eqgvscpbl  33311  imaslmod  33314  quslmod  33319  linds2eq  33342  lbslsat  33602  lindsunlem  33610  lbsdiflsp0  33612  dimkerim  33613  lclkrlem2m  41484  mapdpglem14  41650  baerlem3lem1  41672  baerlem5amN  41681  baerlem5bmN  41682  baerlem5abmN  41683  mapdh6bN  41702  mapdh6cN  41703  hdmap1l6b  41776  hdmap1l6c  41777  hdmap11  41813  frlmsnic  42510  kercvrlsm  43054  pwssplit4  43060  pwslnmlem2  43064  mendring  43159  zlmodzxzsub  48283  lmodvsmdi  48302  lincvalsng  48340  lincvalsc0  48345  linc0scn0  48347  linc1  48349  lcoel0  48352  lindslinindimp2lem4  48385  snlindsntor  48395  lincresunit3  48405