Theorem lmodgrp 20773

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 20770	. 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 6511  (class class class)co 7387  Basecbs 17179  +_gcplusg 17220  ._rcmulr 17221  Scalarcsca 17223   ·_𝑠 cvsca 17224  Grpcgrp 18865  1_rcur 20090  Ringcrg 20142  LModclmod 20766

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 5261

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 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-lmod 20768

This theorem is referenced by:  lmodgrpd  20776  lmodbn0  20777  lmodvacl  20781  lmodass  20782  lmodlcan  20783  lmod0vcl  20797  lmod0vlid  20798  lmod0vrid  20799  lmod0vid  20800  lmodvsmmulgdi  20803  lmodfopne  20806  lmodvnegcl  20809  lmodvnegid  20810  lmodvsubcl  20813  lmodcom  20814  lmodabl  20815  lmodvpncan  20821  lmodvnpcan  20822  lmodsubeq0  20827  lmodsubid  20828  lmodvsghm  20829  lmodprop2d  20830  lsssubg  20863  islss3  20865  lssacs  20873  prdslmodd  20875  lspsnneg  20912  lspsnsub  20913  lmodindp1  20920  lmodvsinv2  20944  islmhm2  20945  0lmhm  20947  idlmhm  20948  pwsdiaglmhm  20964  pwssplit3  20968  lspexch  21039  lspsolvlem  21052  ip0l  21545  ipsubdir  21551  ipsubdi  21552  ip2eq  21562  lsmcss  21601  dsmmlss  21653  frlm0  21663  frlmsubgval  21674  frlmplusgvalb  21678  frlmup1  21707  islindf4  21747  mplind  21977  matgrp  22317  tlmtgp  24083  clmgrp  24968  ncvspi  25056  cphtcphnm  25130  ipcau2  25134  tcphcphlem1  25135  tcphcph  25137  rrxnm  25291  rrxds  25293  pjthlem2  25338  lmodvslmhm  32990  eqgvscpbl  33321  imaslmod  33324  quslmod  33329  linds2eq  33352  lbslsat  33612  lindsunlem  33620  lbsdiflsp0  33622  dimkerim  33623  lclkrlem2m  41513  mapdpglem14  41679  baerlem3lem1  41701  baerlem5amN  41710  baerlem5bmN  41711  baerlem5abmN  41712  mapdh6bN  41731  mapdh6cN  41732  hdmap1l6b  41805  hdmap1l6c  41806  hdmap11  41842  frlmsnic  42528  kercvrlsm  43072  pwssplit4  43078  pwslnmlem2  43082  mendring  43177  zlmodzxzsub  48348  lmodvsmdi  48367  lincvalsng  48405  lincvalsc0  48410  linc0scn0  48412  linc1  48414  lcoel0  48417  lindslinindimp2lem4  48450  snlindsntor  48460  lincresunit3  48470