Theorem lmodgrp 21175

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 21172	. 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)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ∀wral 3080  ‘cfv 6561  (class class class)co 7446  Basecbs 17419  +_gcplusg 17460  ._rcmulr 17461  Scalarcsca 17463   ·_𝑠 cvsca 17464  Grpcgrp 19176  1_rcur 20440  Ringcrg 20492  LModclmod 21168

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5264

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6515  df-fv 6569  df-ov 7449  df-lmod 21170

This theorem is used by:  lmodgrpd  21178  lmodbn0  21179  lmodvacl  21183  lmodass  21184  lmodlcan  21185  lmod0vcl  21199  lmod0vlid  21200  lmod0vrid  21201  lmod0vid  21202  lmodvsmmulgdi  21205  lmodfopne  21208  lmodvnegcl  21211  lmodvnegid  21212  lmodvsubcl  21215  lmodcom  21216  lmodabl  21217  lmodvpncan  21223  lmodvnpcan  21224  lmodsubeq0  21229  lmodsubid  21230  lmodvsghm  21231  lmodprop2d  21232  lsssubg  21265  islss3  21267  lssacs  21275  prdslmodd  21277  lspsnneg  21314  lspsnsub  21315  lmodindp1  21322  lmodvsinv2  21345  islmhm2  21346  0lmhm  21348  idlmhm  21349  pwsdiaglmhm  21365  pwssplit3  21369  lspexch  21440  lspsolvlem  21453  ip0l  21975  ipsubdir  21981  ipsubdi  21982  ip2eq  21992  lsmcss  22031  dsmmlss  22083  frlm0  22093  frlmsubgval  22104  frlmplusgvalb  22108  frlmup1  22137  islindf4  22177  mplind  22412  matgrp  22778  tlmtgp  24548  clmgrp  25422  ncvspi  25510  cphtcphnm  25584  ipcau2  25588  tcphcphlem1  25589  tcphcph  25591  rrxnm  25745  rrxds  25747  pjthlem2  25792  lmodvslmhm  33687  eqgvscpbl  33995  imaslmod  33998  quslmod  34003  linds2eq  34020  lbslsat  34331  lindsunlem  34339  lbsdiflsp0  34341  dimkerim  34342  lclkrlem2m  42779  mapdpglem14  42945  baerlem3lem1  42967  baerlem5amN  42976  baerlem5bmN  42977  baerlem5abmN  42978  mapdh6bN  42997  mapdh6cN  42998  hdmap1l6b  43071  hdmap1l6c  43072  hdmap11  43108  frlmsnic  43808  kercvrlsm  44289  pwssplit4  44295  pwslnmlem2  44299  mendring  44393  zlmodzxzsub  49687  lmodvsmdi  49706  lincvalsng  49743  lincvalsc0  49748  linc0scn0  49750  linc1  49752  lcoel0  49755  lindslinindimp2lem4  49788  snlindsntor  49798  lincresunit3  49808