Theorem lmodgrp 19860

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089   = wceq 1543   ∈ wcel 2112  ∀wral 3051  ‘cfv 6358  (class class class)co 7191  Basecbs 16666  +_gcplusg 16749  ._rcmulr 16750  Scalarcsca 16752   ·_𝑠 cvsca 16753  Grpcgrp 18319  1_rcur 19470  Ringcrg 19516  LModclmod 19853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-nul 5184

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-iota 6316  df-fv 6366  df-ov 7194  df-lmod 19855

This theorem is referenced by:  lmodbn0  19863  lmodvacl  19867  lmodass  19868  lmodlcan  19869  lmod0vcl  19882  lmod0vlid  19883  lmod0vrid  19884  lmod0vid  19885  lmodvsmmulgdi  19888  lmodfopne  19891  lmodvnegcl  19894  lmodvnegid  19895  lmodvsubcl  19898  lmodcom  19899  lmodabl  19900  lmodvpncan  19906  lmodvnpcan  19907  lmodsubeq0  19912  lmodsubid  19913  lmodvsghm  19914  lmodprop2d  19915  lsssubg  19948  islss3  19950  lssacs  19958  prdslmodd  19960  lspsnneg  19997  lspsnsub  19998  lmodindp1  20005  lmodvsinv2  20028  islmhm2  20029  0lmhm  20031  idlmhm  20032  pwsdiaglmhm  20048  pwssplit3  20052  lspexch  20120  lspsolvlem  20133  ip0l  20552  ipsubdir  20558  ipsubdi  20559  ip2eq  20569  lsmcss  20608  dsmmlss  20660  frlm0  20670  frlmsubgval  20681  frlmplusgvalb  20685  frlmup1  20714  islindf4  20754  mplind  20982  matgrp  21281  tlmtgp  23047  clmgrp  23919  ncvspi  24007  cphtcphnm  24081  ipcau2  24085  tcphcphlem1  24086  tcphcph  24088  rrxnm  24242  rrxds  24244  pjthlem2  24289  lmodvslmhm  30983  eqgvscpbl  31218  imaslmod  31221  quslmod  31222  linds2eq  31243  lbslsat  31367  lindsunlem  31373  lbsdiflsp0  31375  dimkerim  31376  lclkrlem2m  39219  mapdpglem14  39385  baerlem3lem1  39407  baerlem5amN  39416  baerlem5bmN  39417  baerlem5abmN  39418  mapdh6bN  39437  mapdh6cN  39438  hdmap1l6b  39511  hdmap1l6c  39512  hdmap11  39548  lmodgrpd  39909  lvecgrp  39910  frlmsnic  39916  kercvrlsm  40552  pwssplit4  40558  pwslnmlem2  40562  mendring  40661  zlmodzxzsub  45312  lmodvsmdi  45334  lincvalsng  45373  lincvalsc0  45378  linc0scn0  45380  linc1  45382  lcoel0  45385  lindslinindimp2lem4  45418  snlindsntor  45428  lincresunit3  45438