Theorem lmodgrp 20957

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  ∀wral 3079  ‘cfv 6525  (class class class)co 7400  Basecbs 17259  +_gcplusg 17300  ._rcmulr 17301  Scalarcsca 17303   ·_𝑠 cvsca 17304  Grpcgrp 18990  1_rcur 20254  Ringcrg 20306  LModclmod 20950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-nul 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403  df-lmod 20952

This theorem is referenced by:  lmodgrpd  20960  lmodbn0  20961  lmodvacl  20965  lmodass  20966  lmodlcan  20967  lmod0vcl  20981  lmod0vlid  20982  lmod0vrid  20983  lmod0vid  20984  lmodvsmmulgdi  20987  lmodfopne  20990  lmodvnegcl  20993  lmodvnegid  20994  lmodvsubcl  20997  lmodcom  20998  lmodabl  20999  lmodvpncan  21005  lmodvnpcan  21006  lmodsubeq0  21011  lmodsubid  21012  lmodvsghm  21013  lmodprop2d  21014  lsssubg  21047  islss3  21049  lssacs  21057  prdslmodd  21059  lspsnneg  21096  lspsnsub  21097  lmodindp1  21104  lmodvsinv2  21127  islmhm2  21128  0lmhm  21130  idlmhm  21131  pwsdiaglmhm  21147  pwssplit3  21151  lspexch  21222  lspsolvlem  21235  ip0l  21746  ipsubdir  21752  ipsubdi  21753  ip2eq  21763  lsmcss  21802  dsmmlss  21854  frlm0  21864  frlmsubgval  21875  frlmplusgvalb  21879  frlmup1  21908  islindf4  21948  mplind  22181  matgrp  22548  tlmtgp  24314  clmgrp  25188  ncvspi  25276  cphtcphnm  25350  ipcau2  25354  tcphcphlem1  25355  tcphcph  25357  rrxnm  25511  rrxds  25513  pjthlem2  25558  lmodvslmhm  33283  eqgvscpbl  33585  imaslmod  33588  quslmod  33593  linds2eq  33610  lbslsat  33923  lindsunlem  33931  lbsdiflsp0  33933  dimkerim  33934  lclkrlem2m  42155  mapdpglem14  42321  baerlem3lem1  42343  baerlem5amN  42352  baerlem5bmN  42353  baerlem5abmN  42354  mapdh6bN  42373  mapdh6cN  42374  hdmap1l6b  42447  hdmap1l6c  42448  hdmap11  42484  frlmsnic  43170  kercvrlsm  43672  pwssplit4  43678  pwslnmlem2  43682  mendring  43777  zlmodzxzsub  48991  lmodvsmdi  49010  lincvalsng  49047  lincvalsc0  49052  linc0scn0  49054  linc1  49056  lcoel0  49059  lindslinindimp2lem4  49092  snlindsntor  49102  lincresunit3  49112