Theorem lmodgrp 21147

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  ∀wral 3076  ‘cfv 6538  (class class class)co 7420  Basecbs 17392  +_gcplusg 17433  ._rcmulr 17434  Scalarcsca 17436   ·_𝑠 cvsca 17437  Grpcgrp 19149  1_rcur 20412  Ringcrg 20464  LModclmod 21140

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-lmod 21142

This theorem is used by:  lmodgrpd  21150  lmodbn0  21151  lmodvacl  21155  lmodass  21156  lmodlcan  21157  lmod0vcl  21171  lmod0vlid  21172  lmod0vrid  21173  lmod0vid  21174  lmodvsmmulgdi  21177  lmodfopne  21180  lmodvnegcl  21183  lmodvnegid  21184  lmodvsubcl  21187  lmodcom  21188  lmodabl  21189  lmodvpncan  21195  lmodvnpcan  21196  lmodsubeq0  21201  lmodsubid  21202  lmodvsghm  21203  lmodprop2d  21204  lsssubg  21237  islss3  21239  lssacs  21247  prdslmodd  21249  lspsnneg  21286  lspsnsub  21287  lmodindp1  21294  lmodvsinv2  21317  islmhm2  21318  0lmhm  21320  idlmhm  21321  pwsdiaglmhm  21337  pwssplit3  21341  lspexch  21412  lspsolvlem  21425  ip0l  21947  ipsubdir  21953  ipsubdi  21954  ip2eq  21964  lsmcss  22003  dsmmlss  22055  frlm0  22065  frlmsubgval  22076  frlmplusgvalb  22080  frlmup1  22109  islindf4  22149  mplind  22384  matgrp  22750  tlmtgp  24520  clmgrp  25394  ncvspi  25482  cphtcphnm  25556  ipcau2  25560  tcphcphlem1  25561  tcphcph  25563  rrxnm  25717  rrxds  25719  pjthlem2  25764  lmodvslmhm  33657  eqgvscpbl  33957  imaslmod  33960  quslmod  33965  linds2eq  33982  lbslsat  34294  lindsunlem  34302  lbsdiflsp0  34304  dimkerim  34305  lclkrlem2m  42669  mapdpglem14  42835  baerlem3lem1  42857  baerlem5amN  42866  baerlem5bmN  42867  baerlem5abmN  42868  mapdh6bN  42887  mapdh6cN  42888  hdmap1l6b  42961  hdmap1l6c  42962  hdmap11  42998  frlmsnic  43697  kercvrlsm  44178  pwssplit4  44184  pwslnmlem2  44188  mendring  44283  zlmodzxzsub  49565  lmodvsmdi  49584  lincvalsng  49621  lincvalsc0  49626  linc0scn0  49628  linc1  49630  lcoel0  49633  lindslinindimp2lem4  49666  snlindsntor  49676  lincresunit3  49686