Theorem lmodgrp 19619

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  ∀wral 3133  ‘cfv 6336  (class class class)co 7137  Basecbs 16461  +_gcplusg 16543  ._rcmulr 16544  Scalarcsca 16546   ·_𝑠 cvsca 16547  Grpcgrp 18081  1_rcur 19229  Ringcrg 19275  LModclmod 19612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-nul 5191

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3483  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-br 5048  df-iota 6295  df-fv 6344  df-ov 7140  df-lmod 19614

This theorem is referenced by:  lmodbn0  19622  lmodvacl  19626  lmodass  19627  lmodlcan  19628  lmod0vcl  19641  lmod0vlid  19642  lmod0vrid  19643  lmod0vid  19644  lmodvsmmulgdi  19647  lmodfopne  19650  lmodvnegcl  19653  lmodvnegid  19654  lmodvsubcl  19657  lmodcom  19658  lmodabl  19659  lmodvpncan  19665  lmodvnpcan  19666  lmodsubeq0  19671  lmodsubid  19672  lmodvsghm  19673  lmodprop2d  19674  lsssubg  19707  islss3  19709  lssacs  19717  prdslmodd  19719  lspsnneg  19756  lspsnsub  19757  lmodindp1  19764  lmodvsinv2  19787  islmhm2  19788  0lmhm  19790  idlmhm  19791  pwsdiaglmhm  19807  pwssplit3  19811  lspexch  19879  lspsolvlem  19892  mplind  20260  ip0l  20758  ipsubdir  20764  ipsubdi  20765  ip2eq  20775  lsmcss  20814  dsmmlss  20866  frlm0  20876  frlmsubgval  20887  frlmplusgvalb  20891  frlmup1  20920  islindf4  20960  matgrp  21017  tlmtgp  22782  clmgrp  23650  ncvspi  23738  cphtcphnm  23811  ipcau2  23815  tcphcphlem1  23816  tcphcph  23818  rrxnm  23972  rrxds  23974  pjthlem2  24019  lmodvslmhm  30690  eqgvscpbl  30921  imaslmod  30924  quslmod  30925  linds2eq  30944  lbslsat  31019  lindsunlem  31025  lbsdiflsp0  31027  dimkerim  31028  lclkrlem2m  38682  mapdpglem14  38848  baerlem3lem1  38870  baerlem5amN  38879  baerlem5bmN  38880  baerlem5abmN  38881  mapdh6bN  38900  mapdh6cN  38901  hdmap1l6b  38974  hdmap1l6c  38975  hdmap11  39011  lvecgrp  39216  frlmsnic  39219  kercvrlsm  39770  pwssplit4  39776  pwslnmlem2  39780  mendring  39879  zlmodzxzsub  44488  lmodvsmdi  44510  lincvalsng  44551  lincvalsc0  44556  linc0scn0  44558  linc1  44560  lcoel0  44563  lindslinindimp2lem4  44596  snlindsntor  44606  lincresunit3  44616