Theorem lmodgrp 20802

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 2733	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2733	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2733	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		eqid 2733	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2733	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6		eqid 2733	. . 3 ⊢ (+g‘(Scalar‘𝑊)) = (+g‘(Scalar‘𝑊))
7		eqid 2733	. . 3 ⊢ (.r‘(Scalar‘𝑊)) = (.r‘(Scalar‘𝑊))
8		eqid 2733	. . 3 ⊢ (1r‘(Scalar‘𝑊)) = (1r‘(Scalar‘𝑊))
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 20799	. 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 2113  ∀wral 3048  ‘cfv 6486  (class class class)co 7352  Basecbs 17122  +_gcplusg 17163  ._rcmulr 17164  Scalarcsca 17166   ·_𝑠 cvsca 17167  Grpcgrp 18848  1_rcur 20101  Ringcrg 20153  LModclmod 20795

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 2115  ax-9 2123  ax-ext 2705  ax-nul 5246

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 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rab 3397  df-v 3439  df-sbc 3738  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355  df-lmod 20797

This theorem is referenced by:  lmodgrpd  20805  lmodbn0  20806  lmodvacl  20810  lmodass  20811  lmodlcan  20812  lmod0vcl  20826  lmod0vlid  20827  lmod0vrid  20828  lmod0vid  20829  lmodvsmmulgdi  20832  lmodfopne  20835  lmodvnegcl  20838  lmodvnegid  20839  lmodvsubcl  20842  lmodcom  20843  lmodabl  20844  lmodvpncan  20850  lmodvnpcan  20851  lmodsubeq0  20856  lmodsubid  20857  lmodvsghm  20858  lmodprop2d  20859  lsssubg  20892  islss3  20894  lssacs  20902  prdslmodd  20904  lspsnneg  20941  lspsnsub  20942  lmodindp1  20949  lmodvsinv2  20973  islmhm2  20974  0lmhm  20976  idlmhm  20977  pwsdiaglmhm  20993  pwssplit3  20997  lspexch  21068  lspsolvlem  21081  ip0l  21575  ipsubdir  21581  ipsubdi  21582  ip2eq  21592  lsmcss  21631  dsmmlss  21683  frlm0  21693  frlmsubgval  21704  frlmplusgvalb  21708  frlmup1  21737  islindf4  21777  mplind  22006  matgrp  22346  tlmtgp  24112  clmgrp  24996  ncvspi  25084  cphtcphnm  25158  ipcau2  25162  tcphcphlem1  25163  tcphcph  25165  rrxnm  25319  rrxds  25321  pjthlem2  25366  lmodvslmhm  33037  eqgvscpbl  33322  imaslmod  33325  quslmod  33330  linds2eq  33353  lbslsat  33650  lindsunlem  33658  lbsdiflsp0  33660  dimkerim  33661  lclkrlem2m  41638  mapdpglem14  41804  baerlem3lem1  41826  baerlem5amN  41835  baerlem5bmN  41836  baerlem5abmN  41837  mapdh6bN  41856  mapdh6cN  41857  hdmap1l6b  41930  hdmap1l6c  41931  hdmap11  41967  frlmsnic  42658  kercvrlsm  43200  pwssplit4  43206  pwslnmlem2  43210  mendring  43305  zlmodzxzsub  48484  lmodvsmdi  48503  lincvalsng  48541  lincvalsc0  48546  linc0scn0  48548  linc1  48550  lcoel0  48553  lindslinindimp2lem4  48586  snlindsntor  48596  lincresunit3  48606