Theorem lmodgrp 20853

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 20850	. 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 6492  (class class class)co 7360  Basecbs 17170  +_gcplusg 17211  ._rcmulr 17212  Scalarcsca 17214   ·_𝑠 cvsca 17215  Grpcgrp 18900  1_rcur 20153  Ringcrg 20205  LModclmod 20846

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 5241

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 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-lmod 20848

This theorem is referenced by:  lmodgrpd  20856  lmodbn0  20857  lmodvacl  20861  lmodass  20862  lmodlcan  20863  lmod0vcl  20877  lmod0vlid  20878  lmod0vrid  20879  lmod0vid  20880  lmodvsmmulgdi  20883  lmodfopne  20886  lmodvnegcl  20889  lmodvnegid  20890  lmodvsubcl  20893  lmodcom  20894  lmodabl  20895  lmodvpncan  20901  lmodvnpcan  20902  lmodsubeq0  20907  lmodsubid  20908  lmodvsghm  20909  lmodprop2d  20910  lsssubg  20943  islss3  20945  lssacs  20953  prdslmodd  20955  lspsnneg  20992  lspsnsub  20993  lmodindp1  21000  lmodvsinv2  21024  islmhm2  21025  0lmhm  21027  idlmhm  21028  pwsdiaglmhm  21044  pwssplit3  21048  lspexch  21119  lspsolvlem  21132  ip0l  21626  ipsubdir  21632  ipsubdi  21633  ip2eq  21643  lsmcss  21682  dsmmlss  21734  frlm0  21744  frlmsubgval  21755  frlmplusgvalb  21759  frlmup1  21788  islindf4  21828  mplind  22058  matgrp  22405  tlmtgp  24171  clmgrp  25045  ncvspi  25133  cphtcphnm  25207  ipcau2  25211  tcphcphlem1  25212  tcphcph  25214  rrxnm  25368  rrxds  25370  pjthlem2  25415  lmodvslmhm  33126  eqgvscpbl  33425  imaslmod  33428  quslmod  33433  linds2eq  33456  lbslsat  33776  lindsunlem  33784  lbsdiflsp0  33786  dimkerim  33787  lclkrlem2m  41979  mapdpglem14  42145  baerlem3lem1  42167  baerlem5amN  42176  baerlem5bmN  42177  baerlem5abmN  42178  mapdh6bN  42197  mapdh6cN  42198  hdmap1l6b  42271  hdmap1l6c  42272  hdmap11  42308  frlmsnic  42999  kercvrlsm  43529  pwssplit4  43535  pwslnmlem2  43539  mendring  43634  zlmodzxzsub  48848  lmodvsmdi  48867  lincvalsng  48904  lincvalsc0  48909  linc0scn0  48911  linc1  48913  lcoel0  48916  lindslinindimp2lem4  48949  snlindsntor  48959  lincresunit3  48969