Theorem lmodgrp 20798

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 2731	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2731	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2731	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		eqid 2731	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2731	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6		eqid 2731	. . 3 ⊢ (+g‘(Scalar‘𝑊)) = (+g‘(Scalar‘𝑊))
7		eqid 2731	. . 3 ⊢ (.r‘(Scalar‘𝑊)) = (.r‘(Scalar‘𝑊))
8		eqid 2731	. . 3 ⊢ (1r‘(Scalar‘𝑊)) = (1r‘(Scalar‘𝑊))
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 20795	. 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 2111  ∀wral 3047  ‘cfv 6481  (class class class)co 7346  Basecbs 17117  +_gcplusg 17158  ._rcmulr 17159  Scalarcsca 17161   ·_𝑠 cvsca 17162  Grpcgrp 18843  1_rcur 20097  Ringcrg 20149  LModclmod 20791

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 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-lmod 20793

This theorem is referenced by:  lmodgrpd  20801  lmodbn0  20802  lmodvacl  20806  lmodass  20807  lmodlcan  20808  lmod0vcl  20822  lmod0vlid  20823  lmod0vrid  20824  lmod0vid  20825  lmodvsmmulgdi  20828  lmodfopne  20831  lmodvnegcl  20834  lmodvnegid  20835  lmodvsubcl  20838  lmodcom  20839  lmodabl  20840  lmodvpncan  20846  lmodvnpcan  20847  lmodsubeq0  20852  lmodsubid  20853  lmodvsghm  20854  lmodprop2d  20855  lsssubg  20888  islss3  20890  lssacs  20898  prdslmodd  20900  lspsnneg  20937  lspsnsub  20938  lmodindp1  20945  lmodvsinv2  20969  islmhm2  20970  0lmhm  20972  idlmhm  20973  pwsdiaglmhm  20989  pwssplit3  20993  lspexch  21064  lspsolvlem  21077  ip0l  21571  ipsubdir  21577  ipsubdi  21578  ip2eq  21588  lsmcss  21627  dsmmlss  21679  frlm0  21689  frlmsubgval  21700  frlmplusgvalb  21704  frlmup1  21733  islindf4  21773  mplind  22003  matgrp  22343  tlmtgp  24109  clmgrp  24993  ncvspi  25081  cphtcphnm  25155  ipcau2  25159  tcphcphlem1  25160  tcphcph  25162  rrxnm  25316  rrxds  25318  pjthlem2  25363  lmodvslmhm  33025  eqgvscpbl  33310  imaslmod  33313  quslmod  33318  linds2eq  33341  lbslsat  33624  lindsunlem  33632  lbsdiflsp0  33634  dimkerim  33635  lclkrlem2m  41557  mapdpglem14  41723  baerlem3lem1  41745  baerlem5amN  41754  baerlem5bmN  41755  baerlem5abmN  41756  mapdh6bN  41775  mapdh6cN  41776  hdmap1l6b  41849  hdmap1l6c  41850  hdmap11  41886  frlmsnic  42572  kercvrlsm  43115  pwssplit4  43121  pwslnmlem2  43125  mendring  43220  zlmodzxzsub  48390  lmodvsmdi  48409  lincvalsng  48447  lincvalsc0  48452  linc0scn0  48454  linc1  48456  lcoel0  48459  lindslinindimp2lem4  48492  snlindsntor  48502  lincresunit3  48512