Theorem lmodgrp 20818

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ∀wral 3051  ‘cfv 6492  (class class class)co 7358  Basecbs 17136  +_gcplusg 17177  ._rcmulr 17178  Scalarcsca 17180   ·_𝑠 cvsca 17181  Grpcgrp 18863  1_rcur 20116  Ringcrg 20168  LModclmod 20811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-lmod 20813

This theorem is referenced by:  lmodgrpd  20821  lmodbn0  20822  lmodvacl  20826  lmodass  20827  lmodlcan  20828  lmod0vcl  20842  lmod0vlid  20843  lmod0vrid  20844  lmod0vid  20845  lmodvsmmulgdi  20848  lmodfopne  20851  lmodvnegcl  20854  lmodvnegid  20855  lmodvsubcl  20858  lmodcom  20859  lmodabl  20860  lmodvpncan  20866  lmodvnpcan  20867  lmodsubeq0  20872  lmodsubid  20873  lmodvsghm  20874  lmodprop2d  20875  lsssubg  20908  islss3  20910  lssacs  20918  prdslmodd  20920  lspsnneg  20957  lspsnsub  20958  lmodindp1  20965  lmodvsinv2  20989  islmhm2  20990  0lmhm  20992  idlmhm  20993  pwsdiaglmhm  21009  pwssplit3  21013  lspexch  21084  lspsolvlem  21097  ip0l  21591  ipsubdir  21597  ipsubdi  21598  ip2eq  21608  lsmcss  21647  dsmmlss  21699  frlm0  21709  frlmsubgval  21720  frlmplusgvalb  21724  frlmup1  21753  islindf4  21793  mplind  22025  matgrp  22374  tlmtgp  24140  clmgrp  25024  ncvspi  25112  cphtcphnm  25186  ipcau2  25190  tcphcphlem1  25191  tcphcph  25193  rrxnm  25347  rrxds  25349  pjthlem2  25394  lmodvslmhm  33133  eqgvscpbl  33431  imaslmod  33434  quslmod  33439  linds2eq  33462  lbslsat  33773  lindsunlem  33781  lbsdiflsp0  33783  dimkerim  33784  lclkrlem2m  41775  mapdpglem14  41941  baerlem3lem1  41963  baerlem5amN  41972  baerlem5bmN  41973  baerlem5abmN  41974  mapdh6bN  41993  mapdh6cN  41994  hdmap1l6b  42067  hdmap1l6c  42068  hdmap11  42104  frlmsnic  42791  kercvrlsm  43321  pwssplit4  43327  pwslnmlem2  43331  mendring  43426  zlmodzxzsub  48602  lmodvsmdi  48621  lincvalsng  48658  lincvalsc0  48663  linc0scn0  48665  linc1  48667  lcoel0  48670  lindslinindimp2lem4  48703  snlindsntor  48713  lincresunit3  48723