Theorem lmodgrp 20969

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 2763	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2763	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2763	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		eqid 2763	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2763	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6		eqid 2763	. . 3 ⊢ (+g‘(Scalar‘𝑊)) = (+g‘(Scalar‘𝑊))
7		eqid 2763	. . 3 ⊢ (.r‘(Scalar‘𝑊)) = (.r‘(Scalar‘𝑊))
8		eqid 2763	. . 3 ⊢ (1r‘(Scalar‘𝑊)) = (1r‘(Scalar‘𝑊))
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 20966	. 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)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ‘cfv 6538  (class class class)co 7412  Basecbs 17270  +_gcplusg 17311  ._rcmulr 17312  Scalarcsca 17314   ·_𝑠 cvsca 17315  Grpcgrp 19001  1_rcur 20264  Ringcrg 20316  LModclmod 20962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-lmod 20964

This theorem is referenced by:  lmodgrpd  20972  lmodbn0  20973  lmodvacl  20977  lmodass  20978  lmodlcan  20979  lmod0vcl  20993  lmod0vlid  20994  lmod0vrid  20995  lmod0vid  20996  lmodvsmmulgdi  20999  lmodfopne  21002  lmodvnegcl  21005  lmodvnegid  21006  lmodvsubcl  21009  lmodcom  21010  lmodabl  21011  lmodvpncan  21017  lmodvnpcan  21018  lmodsubeq0  21023  lmodsubid  21024  lmodvsghm  21025  lmodprop2d  21026  lsssubg  21059  islss3  21061  lssacs  21069  prdslmodd  21071  lspsnneg  21108  lspsnsub  21109  lmodindp1  21116  lmodvsinv2  21139  islmhm2  21140  0lmhm  21142  idlmhm  21143  pwsdiaglmhm  21159  pwssplit3  21163  lspexch  21234  lspsolvlem  21247  ip0l  21767  ipsubdir  21773  ipsubdi  21774  ip2eq  21784  lsmcss  21823  dsmmlss  21875  frlm0  21885  frlmsubgval  21896  frlmplusgvalb  21900  frlmup1  21929  islindf4  21969  mplind  22202  matgrp  22568  tlmtgp  24334  clmgrp  25208  ncvspi  25296  cphtcphnm  25370  ipcau2  25374  tcphcphlem1  25375  tcphcph  25377  rrxnm  25531  rrxds  25533  pjthlem2  25578  lmodvslmhm  33351  eqgvscpbl  33651  imaslmod  33654  quslmod  33659  linds2eq  33675  lbslsat  33987  lindsunlem  33995  lbsdiflsp0  33997  dimkerim  33998  lclkrlem2m  42274  mapdpglem14  42440  baerlem3lem1  42462  baerlem5amN  42471  baerlem5bmN  42472  baerlem5abmN  42473  mapdh6bN  42492  mapdh6cN  42493  hdmap1l6b  42566  hdmap1l6c  42567  hdmap11  42603  frlmsnic  43291  kercvrlsm  43793  pwssplit4  43799  pwslnmlem2  43803  mendring  43898  zlmodzxzsub  49123  lmodvsmdi  49142  lincvalsng  49179  lincvalsc0  49184  linc0scn0  49186  linc1  49188  lcoel0  49191  lindslinindimp2lem4  49224  snlindsntor  49234  lincresunit3  49244