Theorem lmodgrp 20881

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105  ∀wral 3058  ‘cfv 6562  (class class class)co 7430  Basecbs 17244  +_gcplusg 17297  ._rcmulr 17298  Scalarcsca 17300   ·_𝑠 cvsca 17301  Grpcgrp 18963  1_rcur 20198  Ringcrg 20250  LModclmod 20874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-nul 5311

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-lmod 20876

This theorem is referenced by:  lmodgrpd  20884  lmodbn0  20885  lmodvacl  20889  lmodass  20890  lmodlcan  20891  lmod0vcl  20905  lmod0vlid  20906  lmod0vrid  20907  lmod0vid  20908  lmodvsmmulgdi  20911  lmodfopne  20914  lmodvnegcl  20917  lmodvnegid  20918  lmodvsubcl  20921  lmodcom  20922  lmodabl  20923  lmodvpncan  20929  lmodvnpcan  20930  lmodsubeq0  20935  lmodsubid  20936  lmodvsghm  20937  lmodprop2d  20938  lsssubg  20972  islss3  20974  lssacs  20982  prdslmodd  20984  lspsnneg  21021  lspsnsub  21022  lmodindp1  21029  lmodvsinv2  21053  islmhm2  21054  0lmhm  21056  idlmhm  21057  pwsdiaglmhm  21073  pwssplit3  21077  lspexch  21148  lspsolvlem  21161  ip0l  21671  ipsubdir  21677  ipsubdi  21678  ip2eq  21688  lsmcss  21727  dsmmlss  21781  frlm0  21791  frlmsubgval  21802  frlmplusgvalb  21806  frlmup1  21835  islindf4  21875  mplind  22111  matgrp  22451  tlmtgp  24219  clmgrp  25114  ncvspi  25203  cphtcphnm  25277  ipcau2  25281  tcphcphlem1  25282  tcphcph  25284  rrxnm  25438  rrxds  25440  pjthlem2  25485  lmodvslmhm  33035  eqgvscpbl  33357  imaslmod  33360  quslmod  33365  linds2eq  33388  lbslsat  33643  lindsunlem  33651  lbsdiflsp0  33653  dimkerim  33654  lclkrlem2m  41501  mapdpglem14  41667  baerlem3lem1  41689  baerlem5amN  41698  baerlem5bmN  41699  baerlem5abmN  41700  mapdh6bN  41719  mapdh6cN  41720  hdmap1l6b  41793  hdmap1l6c  41794  hdmap11  41830  frlmsnic  42526  kercvrlsm  43071  pwssplit4  43077  pwslnmlem2  43081  mendring  43176  zlmodzxzsub  48204  lmodvsmdi  48223  lincvalsng  48261  lincvalsc0  48266  linc0scn0  48268  linc1  48270  lcoel0  48273  lindslinindimp2lem4  48306  snlindsntor  48316  lincresunit3  48326