Theorem lmodgrp 19635

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 2821	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2821	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2821	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		eqid 2821	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2821	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6		eqid 2821	. . 3 ⊢ (+g‘(Scalar‘𝑊)) = (+g‘(Scalar‘𝑊))
7		eqid 2821	. . 3 ⊢ (.r‘(Scalar‘𝑊)) = (.r‘(Scalar‘𝑊))
8		eqid 2821	. . 3 ⊢ (1r‘(Scalar‘𝑊)) = (1r‘(Scalar‘𝑊))
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 19632	. 2 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ (Scalar‘𝑊) ∈ Ring ∧ ∀𝑞 ∈ (Base‘(Scalar‘𝑊))∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠 ‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑊))𝑟)( ·𝑠 ‘𝑊)𝑤) = ((𝑞( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠 ‘𝑊)𝑤) = (𝑞( ·𝑠 ‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤)) ∧ ((1r‘(Scalar‘𝑊))( ·𝑠 ‘𝑊)𝑤) = 𝑤))))
10	9	simp1bi 1141	1 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110  ∀wral 3138  ‘cfv 6349  (class class class)co 7150  Basecbs 16477  +_gcplusg 16559  ._rcmulr 16560  Scalarcsca 16562   ·_𝑠 cvsca 16563  Grpcgrp 18097  1_rcur 19245  Ringcrg 19291  LModclmod 19628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-nul 5202

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7153  df-lmod 19630

This theorem is referenced by:  lmodbn0  19638  lmodvacl  19642  lmodass  19643  lmodlcan  19644  lmod0vcl  19657  lmod0vlid  19658  lmod0vrid  19659  lmod0vid  19660  lmodvsmmulgdi  19663  lmodfopne  19666  lmodvnegcl  19669  lmodvnegid  19670  lmodvsubcl  19673  lmodcom  19674  lmodabl  19675  lmodvpncan  19681  lmodvnpcan  19682  lmodsubeq0  19687  lmodsubid  19688  lmodvsghm  19689  lmodprop2d  19690  lsssubg  19723  islss3  19725  lssacs  19733  prdslmodd  19735  lspsnneg  19772  lspsnsub  19773  lmodindp1  19780  lmodvsinv2  19803  islmhm2  19804  0lmhm  19806  idlmhm  19807  pwsdiaglmhm  19823  pwssplit3  19827  lspexch  19895  lspsolvlem  19908  mplind  20276  ip0l  20774  ipsubdir  20780  ipsubdi  20781  ip2eq  20791  lsmcss  20830  dsmmlss  20882  frlm0  20892  frlmsubgval  20903  frlmplusgvalb  20907  frlmup1  20936  islindf4  20976  matgrp  21033  tlmtgp  22798  clmgrp  23666  ncvspi  23754  cphtcphnm  23827  ipcau2  23831  tcphcphlem1  23832  tcphcph  23834  rrxnm  23988  rrxds  23990  pjthlem2  24035  lmodvslmhm  30683  eqgvscpbl  30914  imaslmod  30917  quslmod  30918  linds2eq  30936  lbslsat  31009  lindsunlem  31015  lbsdiflsp0  31017  dimkerim  31018  lclkrlem2m  38649  mapdpglem14  38815  baerlem3lem1  38837  baerlem5amN  38846  baerlem5bmN  38847  baerlem5abmN  38848  mapdh6bN  38867  mapdh6cN  38868  hdmap1l6b  38941  hdmap1l6c  38942  hdmap11  38978  lvecgrp  39139  frlmsnic  39142  kercvrlsm  39676  pwssplit4  39682  pwslnmlem2  39686  mendring  39785  zlmodzxzsub  44402  lmodvsmdi  44424  lincvalsng  44465  lincvalsc0  44470  linc0scn0  44472  linc1  44474  lcoel0  44477  lindslinindimp2lem4  44510  snlindsntor  44520  lincresunit3  44530