Theorem lmodgrp 20788

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 2729	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2729	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2729	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		eqid 2729	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2729	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6		eqid 2729	. . 3 ⊢ (+g‘(Scalar‘𝑊)) = (+g‘(Scalar‘𝑊))
7		eqid 2729	. . 3 ⊢ (.r‘(Scalar‘𝑊)) = (.r‘(Scalar‘𝑊))
8		eqid 2729	. . 3 ⊢ (1r‘(Scalar‘𝑊)) = (1r‘(Scalar‘𝑊))
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 20785	. 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 3044  ‘cfv 6486  (class class class)co 7353  Basecbs 17138  +_gcplusg 17179  ._rcmulr 17180  Scalarcsca 17182   ·_𝑠 cvsca 17183  Grpcgrp 18830  1_rcur 20084  Ringcrg 20136  LModclmod 20781

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 2701  ax-nul 5248

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-lmod 20783

This theorem is referenced by:  lmodgrpd  20791  lmodbn0  20792  lmodvacl  20796  lmodass  20797  lmodlcan  20798  lmod0vcl  20812  lmod0vlid  20813  lmod0vrid  20814  lmod0vid  20815  lmodvsmmulgdi  20818  lmodfopne  20821  lmodvnegcl  20824  lmodvnegid  20825  lmodvsubcl  20828  lmodcom  20829  lmodabl  20830  lmodvpncan  20836  lmodvnpcan  20837  lmodsubeq0  20842  lmodsubid  20843  lmodvsghm  20844  lmodprop2d  20845  lsssubg  20878  islss3  20880  lssacs  20888  prdslmodd  20890  lspsnneg  20927  lspsnsub  20928  lmodindp1  20935  lmodvsinv2  20959  islmhm2  20960  0lmhm  20962  idlmhm  20963  pwsdiaglmhm  20979  pwssplit3  20983  lspexch  21054  lspsolvlem  21067  ip0l  21561  ipsubdir  21567  ipsubdi  21568  ip2eq  21578  lsmcss  21617  dsmmlss  21669  frlm0  21679  frlmsubgval  21690  frlmplusgvalb  21694  frlmup1  21723  islindf4  21763  mplind  21993  matgrp  22333  tlmtgp  24099  clmgrp  24984  ncvspi  25072  cphtcphnm  25146  ipcau2  25150  tcphcphlem1  25151  tcphcph  25153  rrxnm  25307  rrxds  25309  pjthlem2  25354  lmodvslmhm  33016  eqgvscpbl  33297  imaslmod  33300  quslmod  33305  linds2eq  33328  lbslsat  33588  lindsunlem  33596  lbsdiflsp0  33598  dimkerim  33599  lclkrlem2m  41498  mapdpglem14  41664  baerlem3lem1  41686  baerlem5amN  41695  baerlem5bmN  41696  baerlem5abmN  41697  mapdh6bN  41716  mapdh6cN  41717  hdmap1l6b  41790  hdmap1l6c  41791  hdmap11  41827  frlmsnic  42513  kercvrlsm  43056  pwssplit4  43062  pwslnmlem2  43066  mendring  43161  zlmodzxzsub  48345  lmodvsmdi  48364  lincvalsng  48402  lincvalsc0  48407  linc0scn0  48409  linc1  48411  lcoel0  48414  lindslinindimp2lem4  48447  snlindsntor  48457  lincresunit3  48467