Theorem lmodgrp 20865

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  ∀wral 3061  ‘cfv 6561  (class class class)co 7431  Basecbs 17247  +_gcplusg 17297  ._rcmulr 17298  Scalarcsca 17300   ·_𝑠 cvsca 17301  Grpcgrp 18951  1_rcur 20178  Ringcrg 20230  LModclmod 20858

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-lmod 20860

This theorem is referenced by:  lmodgrpd  20868  lmodbn0  20869  lmodvacl  20873  lmodass  20874  lmodlcan  20875  lmod0vcl  20889  lmod0vlid  20890  lmod0vrid  20891  lmod0vid  20892  lmodvsmmulgdi  20895  lmodfopne  20898  lmodvnegcl  20901  lmodvnegid  20902  lmodvsubcl  20905  lmodcom  20906  lmodabl  20907  lmodvpncan  20913  lmodvnpcan  20914  lmodsubeq0  20919  lmodsubid  20920  lmodvsghm  20921  lmodprop2d  20922  lsssubg  20955  islss3  20957  lssacs  20965  prdslmodd  20967  lspsnneg  21004  lspsnsub  21005  lmodindp1  21012  lmodvsinv2  21036  islmhm2  21037  0lmhm  21039  idlmhm  21040  pwsdiaglmhm  21056  pwssplit3  21060  lspexch  21131  lspsolvlem  21144  ip0l  21654  ipsubdir  21660  ipsubdi  21661  ip2eq  21671  lsmcss  21710  dsmmlss  21764  frlm0  21774  frlmsubgval  21785  frlmplusgvalb  21789  frlmup1  21818  islindf4  21858  mplind  22094  matgrp  22436  tlmtgp  24204  clmgrp  25101  ncvspi  25190  cphtcphnm  25264  ipcau2  25268  tcphcphlem1  25269  tcphcph  25271  rrxnm  25425  rrxds  25427  pjthlem2  25472  lmodvslmhm  33053  eqgvscpbl  33378  imaslmod  33381  quslmod  33386  linds2eq  33409  lbslsat  33667  lindsunlem  33675  lbsdiflsp0  33677  dimkerim  33678  lclkrlem2m  41521  mapdpglem14  41687  baerlem3lem1  41709  baerlem5amN  41718  baerlem5bmN  41719  baerlem5abmN  41720  mapdh6bN  41739  mapdh6cN  41740  hdmap1l6b  41813  hdmap1l6c  41814  hdmap11  41850  frlmsnic  42550  kercvrlsm  43095  pwssplit4  43101  pwslnmlem2  43105  mendring  43200  zlmodzxzsub  48276  lmodvsmdi  48295  lincvalsng  48333  lincvalsc0  48338  linc0scn0  48340  linc1  48342  lcoel0  48345  lindslinindimp2lem4  48378  snlindsntor  48388  lincresunit3  48398