Theorem lmodgrp 18918

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  ∀wral 2941  ‘cfv 5926  (class class class)co 6690  Basecbs 15904  +_gcplusg 15988  ._rcmulr 15989  Scalarcsca 15991   ·_𝑠 cvsca 15992  Grpcgrp 17469  1_rcur 18547  Ringcrg 18593  LModclmod 18911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-nul 4822

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-lmod 18913

This theorem is referenced by:  lmodbn0  18921  lmodvacl  18925  lmodass  18926  lmodlcan  18927  lmod0vcl  18940  lmod0vlid  18941  lmod0vrid  18942  lmod0vid  18943  lmodvsmmulgdi  18946  lmodfopne  18949  lmodvnegcl  18952  lmodvnegid  18953  lmodvsubcl  18956  lmodcom  18957  lmodabl  18958  lmodvpncan  18964  lmodvnpcan  18965  lmodsubeq0  18970  lmodsubid  18971  lmodvsghm  18972  lmodprop2d  18973  lsssubg  19005  islss3  19007  lssacs  19015  prdslmodd  19017  lspsnneg  19054  lspsnsub  19055  lmodindp1  19062  lmodvsinv2  19085  islmhm2  19086  0lmhm  19088  idlmhm  19089  pwsdiaglmhm  19105  pwssplit3  19109  lspexch  19177  lspsolvlem  19190  mplind  19550  ip0l  20029  ipsubdir  20035  ipsubdi  20036  ip2eq  20046  lsmcss  20084  dsmmlss  20136  frlm0  20146  frlmsubgval  20156  frlmup1  20185  islindf4  20225  matgrp  20284  tlmtgp  22046  clmgrp  22914  ncvspi  23002  cphtchnm  23075  ipcau2  23079  tchcphlem1  23080  tchcph  23082  rrxnm  23225  rrxds  23227  pjthlem2  23255  lclkrlem2m  37125  mapdpglem14  37291  baerlem3lem1  37313  baerlem5amN  37322  baerlem5bmN  37323  baerlem5abmN  37324  mapdh6bN  37343  mapdh6cN  37344  hdmap1l6b  37418  hdmap1l6c  37419  hdmap1neglem1N  37434  hdmap11  37457  kercvrlsm  37970  pwssplit4  37976  pwslnmlem2  37980  mendring  38079  zlmodzxzsub  42463  lmodvsmdi  42488  lincvalsng  42530  lincvalsc0  42535  linc0scn0  42537  linc1  42539  lcoel0  42542  lindslinindimp2lem4  42575  snlindsntor  42585  lincresunit3  42595