Theorem lmodgrp 21057

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 2762	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2762	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2762	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		eqid 2762	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2762	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6		eqid 2762	. . 3 ⊢ (+g‘(Scalar‘𝑊)) = (+g‘(Scalar‘𝑊))
7		eqid 2762	. . 3 ⊢ (.r‘(Scalar‘𝑊)) = (.r‘(Scalar‘𝑊))
8		eqid 2762	. . 3 ⊢ (1r‘(Scalar‘𝑊)) = (1r‘(Scalar‘𝑊))
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 21054	. 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 3078  ‘cfv 6537  (class class class)co 7417  Basecbs 17307  +_gcplusg 17348  ._rcmulr 17349  Scalarcsca 17351   ·_𝑠 cvsca 17352  Grpcgrp 19063  1_rcur 20326  Ringcrg 20378  LModclmod 21050

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 2734  ax-nul 5267

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-lmod 21052

This theorem is used by:  lmodgrpd  21060  lmodbn0  21061  lmodvacl  21065  lmodass  21066  lmodlcan  21067  lmod0vcl  21081  lmod0vlid  21082  lmod0vrid  21083  lmod0vid  21084  lmodvsmmulgdi  21087  lmodfopne  21090  lmodvnegcl  21093  lmodvnegid  21094  lmodvsubcl  21097  lmodcom  21098  lmodabl  21099  lmodvpncan  21105  lmodvnpcan  21106  lmodsubeq0  21111  lmodsubid  21112  lmodvsghm  21113  lmodprop2d  21114  lsssubg  21147  islss3  21149  lssacs  21157  prdslmodd  21159  lspsnneg  21196  lspsnsub  21197  lmodindp1  21204  lmodvsinv2  21227  islmhm2  21228  0lmhm  21230  idlmhm  21231  pwsdiaglmhm  21247  pwssplit3  21251  lspexch  21322  lspsolvlem  21335  ip0l  21855  ipsubdir  21861  ipsubdi  21862  ip2eq  21872  lsmcss  21911  dsmmlss  21963  frlm0  21973  frlmsubgval  21984  frlmplusgvalb  21988  frlmup1  22017  islindf4  22057  mplind  22292  matgrp  22658  tlmtgp  24428  clmgrp  25302  ncvspi  25390  cphtcphnm  25464  ipcau2  25468  tcphcphlem1  25469  tcphcph  25471  rrxnm  25625  rrxds  25627  pjthlem2  25672  lmodvslmhm  33498  eqgvscpbl  33798  imaslmod  33801  quslmod  33806  linds2eq  33822  lbslsat  34134  lindsunlem  34142  lbsdiflsp0  34144  dimkerim  34145  lclkrlem2m  42400  mapdpglem14  42566  baerlem3lem1  42588  baerlem5amN  42597  baerlem5bmN  42598  baerlem5abmN  42599  mapdh6bN  42618  mapdh6cN  42619  hdmap1l6b  42692  hdmap1l6c  42693  hdmap11  42729  frlmsnic  43430  kercvrlsm  43932  pwssplit4  43938  pwslnmlem2  43942  mendring  44037  zlmodzxzsub  49298  lmodvsmdi  49317  lincvalsng  49354  lincvalsc0  49359  linc0scn0  49361  linc1  49363  lcoel0  49366  lindslinindimp2lem4  49399  snlindsntor  49409  lincresunit3  49419