Theorem lmodgrp 20830

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 20827	. 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 1542   ∈ wcel 2114  ∀wral 3052  ‘cfv 6500  (class class class)co 7368  Basecbs 17148  +_gcplusg 17189  ._rcmulr 17190  Scalarcsca 17192   ·_𝑠 cvsca 17193  Grpcgrp 18875  1_rcur 20128  Ringcrg 20180  LModclmod 20823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5253

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-lmod 20825

This theorem is referenced by:  lmodgrpd  20833  lmodbn0  20834  lmodvacl  20838  lmodass  20839  lmodlcan  20840  lmod0vcl  20854  lmod0vlid  20855  lmod0vrid  20856  lmod0vid  20857  lmodvsmmulgdi  20860  lmodfopne  20863  lmodvnegcl  20866  lmodvnegid  20867  lmodvsubcl  20870  lmodcom  20871  lmodabl  20872  lmodvpncan  20878  lmodvnpcan  20879  lmodsubeq0  20884  lmodsubid  20885  lmodvsghm  20886  lmodprop2d  20887  lsssubg  20920  islss3  20922  lssacs  20930  prdslmodd  20932  lspsnneg  20969  lspsnsub  20970  lmodindp1  20977  lmodvsinv2  21001  islmhm2  21002  0lmhm  21004  idlmhm  21005  pwsdiaglmhm  21021  pwssplit3  21025  lspexch  21096  lspsolvlem  21109  ip0l  21603  ipsubdir  21609  ipsubdi  21610  ip2eq  21620  lsmcss  21659  dsmmlss  21711  frlm0  21721  frlmsubgval  21732  frlmplusgvalb  21736  frlmup1  21765  islindf4  21805  mplind  22037  matgrp  22386  tlmtgp  24152  clmgrp  25036  ncvspi  25124  cphtcphnm  25198  ipcau2  25202  tcphcphlem1  25203  tcphcph  25205  rrxnm  25359  rrxds  25361  pjthlem2  25406  lmodvslmhm  33143  eqgvscpbl  33442  imaslmod  33445  quslmod  33450  linds2eq  33473  lbslsat  33793  lindsunlem  33801  lbsdiflsp0  33803  dimkerim  33804  lclkrlem2m  41889  mapdpglem14  42055  baerlem3lem1  42077  baerlem5amN  42086  baerlem5bmN  42087  baerlem5abmN  42088  mapdh6bN  42107  mapdh6cN  42108  hdmap1l6b  42181  hdmap1l6c  42182  hdmap11  42218  frlmsnic  42904  kercvrlsm  43434  pwssplit4  43440  pwslnmlem2  43444  mendring  43539  zlmodzxzsub  48714  lmodvsmdi  48733  lincvalsng  48770  lincvalsc0  48775  linc0scn0  48777  linc1  48779  lcoel0  48782  lindslinindimp2lem4  48815  snlindsntor  48825  lincresunit3  48835