Theorem lmodgrp 20887

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 2740	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2740	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2740	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		eqid 2740	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2740	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6		eqid 2740	. . 3 ⊢ (+g‘(Scalar‘𝑊)) = (+g‘(Scalar‘𝑊))
7		eqid 2740	. . 3 ⊢ (.r‘(Scalar‘𝑊)) = (.r‘(Scalar‘𝑊))
8		eqid 2740	. . 3 ⊢ (1r‘(Scalar‘𝑊)) = (1r‘(Scalar‘𝑊))
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 20884	. 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 1087   = wceq 1537   ∈ wcel 2108  ∀wral 3067  ‘cfv 6573  (class class class)co 7448  Basecbs 17258  +_gcplusg 17311  ._rcmulr 17312  Scalarcsca 17314   ·_𝑠 cvsca 17315  Grpcgrp 18973  1_rcur 20208  Ringcrg 20260  LModclmod 20880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-lmod 20882

This theorem is referenced by:  lmodgrpd  20890  lmodbn0  20891  lmodvacl  20895  lmodass  20896  lmodlcan  20897  lmod0vcl  20911  lmod0vlid  20912  lmod0vrid  20913  lmod0vid  20914  lmodvsmmulgdi  20917  lmodfopne  20920  lmodvnegcl  20923  lmodvnegid  20924  lmodvsubcl  20927  lmodcom  20928  lmodabl  20929  lmodvpncan  20935  lmodvnpcan  20936  lmodsubeq0  20941  lmodsubid  20942  lmodvsghm  20943  lmodprop2d  20944  lsssubg  20978  islss3  20980  lssacs  20988  prdslmodd  20990  lspsnneg  21027  lspsnsub  21028  lmodindp1  21035  lmodvsinv2  21059  islmhm2  21060  0lmhm  21062  idlmhm  21063  pwsdiaglmhm  21079  pwssplit3  21083  lspexch  21154  lspsolvlem  21167  ip0l  21677  ipsubdir  21683  ipsubdi  21684  ip2eq  21694  lsmcss  21733  dsmmlss  21787  frlm0  21797  frlmsubgval  21808  frlmplusgvalb  21812  frlmup1  21841  islindf4  21881  mplind  22117  matgrp  22457  tlmtgp  24225  clmgrp  25120  ncvspi  25209  cphtcphnm  25283  ipcau2  25287  tcphcphlem1  25288  tcphcph  25290  rrxnm  25444  rrxds  25446  pjthlem2  25491  lmodvslmhm  33033  eqgvscpbl  33343  imaslmod  33346  quslmod  33351  linds2eq  33374  lbslsat  33629  lindsunlem  33637  lbsdiflsp0  33639  dimkerim  33640  lclkrlem2m  41476  mapdpglem14  41642  baerlem3lem1  41664  baerlem5amN  41673  baerlem5bmN  41674  baerlem5abmN  41675  mapdh6bN  41694  mapdh6cN  41695  hdmap1l6b  41768  hdmap1l6c  41769  hdmap11  41805  frlmsnic  42495  kercvrlsm  43040  pwssplit4  43046  pwslnmlem2  43050  mendring  43149  zlmodzxzsub  48085  lmodvsmdi  48107  lincvalsng  48145  lincvalsc0  48150  linc0scn0  48152  linc1  48154  lcoel0  48157  lindslinindimp2lem4  48190  snlindsntor  48200  lincresunit3  48210