Theorem lmodgrp 20621

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104  ∀wral 3059  ‘cfv 6542  (class class class)co 7411  Basecbs 17148  +_gcplusg 17201  ._rcmulr 17202  Scalarcsca 17204   ·_𝑠 cvsca 17205  Grpcgrp 18855  1_rcur 20075  Ringcrg 20127  LModclmod 20614

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-nul 5305

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rab 3431  df-v 3474  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-ov 7414  df-lmod 20616

This theorem is referenced by:  lmodgrpd  20624  lmodbn0  20625  lmodvacl  20629  lmodass  20630  lmodlcan  20631  lmod0vcl  20645  lmod0vlid  20646  lmod0vrid  20647  lmod0vid  20648  lmodvsmmulgdi  20651  lmodfopne  20654  lmodvnegcl  20657  lmodvnegid  20658  lmodvsubcl  20661  lmodcom  20662  lmodabl  20663  lmodvpncan  20669  lmodvnpcan  20670  lmodsubeq0  20675  lmodsubid  20676  lmodvsghm  20677  lmodprop2d  20678  lsssubg  20712  islss3  20714  lssacs  20722  prdslmodd  20724  lspsnneg  20761  lspsnsub  20762  lmodindp1  20769  lmodvsinv2  20792  islmhm2  20793  0lmhm  20795  idlmhm  20796  pwsdiaglmhm  20812  pwssplit3  20816  lspexch  20887  lspsolvlem  20900  ip0l  21408  ipsubdir  21414  ipsubdi  21415  ip2eq  21425  lsmcss  21464  dsmmlss  21518  frlm0  21528  frlmsubgval  21539  frlmplusgvalb  21543  frlmup1  21572  islindf4  21612  mplind  21850  matgrp  22152  tlmtgp  23920  clmgrp  24815  ncvspi  24904  cphtcphnm  24978  ipcau2  24982  tcphcphlem1  24983  tcphcph  24985  rrxnm  25139  rrxds  25141  pjthlem2  25186  lmodvslmhm  32472  eqgvscpbl  32735  imaslmod  32738  quslmod  32743  linds2eq  32771  lbslsat  32989  lindsunlem  32997  lbsdiflsp0  32999  dimkerim  33000  lclkrlem2m  40693  mapdpglem14  40859  baerlem3lem1  40881  baerlem5amN  40890  baerlem5bmN  40891  baerlem5abmN  40892  mapdh6bN  40911  mapdh6cN  40912  hdmap1l6b  40985  hdmap1l6c  40986  hdmap11  41022  frlmsnic  41412  kercvrlsm  42127  pwssplit4  42133  pwslnmlem2  42137  mendring  42236  zlmodzxzsub  47124  lmodvsmdi  47146  lincvalsng  47184  lincvalsc0  47189  linc0scn0  47191  linc1  47193  lcoel0  47196  lindslinindimp2lem4  47229  snlindsntor  47239  lincresunit3  47249