Theorem lmodgrp 21051

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3076  ‘cfv 6533  (class class class)co 7413  Basecbs 17301  +_gcplusg 17342  ._rcmulr 17343  Scalarcsca 17345   ·_𝑠 cvsca 17346  Grpcgrp 19057  1_rcur 20320  Ringcrg 20372  LModclmod 21044

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7416  df-lmod 21046

This theorem is used by:  lmodgrpd  21054  lmodbn0  21055  lmodvacl  21059  lmodass  21060  lmodlcan  21061  lmod0vcl  21075  lmod0vlid  21076  lmod0vrid  21077  lmod0vid  21078  lmodvsmmulgdi  21081  lmodfopne  21084  lmodvnegcl  21087  lmodvnegid  21088  lmodvsubcl  21091  lmodcom  21092  lmodabl  21093  lmodvpncan  21099  lmodvnpcan  21100  lmodsubeq0  21105  lmodsubid  21106  lmodvsghm  21107  lmodprop2d  21108  lsssubg  21141  islss3  21143  lssacs  21151  prdslmodd  21153  lspsnneg  21190  lspsnsub  21191  lmodindp1  21198  lmodvsinv2  21221  islmhm2  21222  0lmhm  21224  idlmhm  21225  pwsdiaglmhm  21241  pwssplit3  21245  lspexch  21316  lspsolvlem  21329  ip0l  21849  ipsubdir  21855  ipsubdi  21856  ip2eq  21866  lsmcss  21905  dsmmlss  21957  frlm0  21967  frlmsubgval  21978  frlmplusgvalb  21982  frlmup1  22011  islindf4  22051  mplind  22286  matgrp  22652  tlmtgp  24422  clmgrp  25296  ncvspi  25384  cphtcphnm  25458  ipcau2  25462  tcphcphlem1  25463  tcphcph  25465  rrxnm  25619  rrxds  25621  pjthlem2  25666  lmodvslmhm  33490  eqgvscpbl  33790  imaslmod  33793  quslmod  33798  linds2eq  33814  lbslsat  34126  lindsunlem  34134  lbsdiflsp0  34136  dimkerim  34137  lclkrlem2m  42392  mapdpglem14  42558  baerlem3lem1  42580  baerlem5amN  42589  baerlem5bmN  42590  baerlem5abmN  42591  mapdh6bN  42610  mapdh6cN  42611  hdmap1l6b  42684  hdmap1l6c  42685  hdmap11  42721  frlmsnic  43422  kercvrlsm  43924  pwssplit4  43930  pwslnmlem2  43934  mendring  44029  zlmodzxzsub  49290  lmodvsmdi  49309  lincvalsng  49346  lincvalsc0  49351  linc0scn0  49353  linc1  49355  lcoel0  49358  lindslinindimp2lem4  49391  snlindsntor  49401  lincresunit3  49411