Theorem lmodgrp 19353

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068   = wceq 1507   ∈ wcel 2048  ∀wral 3082  ‘cfv 6182  (class class class)co 6970  Basecbs 16329  +_gcplusg 16411  ._rcmulr 16412  Scalarcsca 16414   ·_𝑠 cvsca 16415  Grpcgrp 17881  1_rcur 18964  Ringcrg 19010  LModclmod 19346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745  ax-nul 5061

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-sbc 3678  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-br 4924  df-iota 6146  df-fv 6190  df-ov 6973  df-lmod 19348

This theorem is referenced by:  lmodbn0  19356  lmodvacl  19360  lmodass  19361  lmodlcan  19362  lmod0vcl  19375  lmod0vlid  19376  lmod0vrid  19377  lmod0vid  19378  lmodvsmmulgdi  19381  lmodfopne  19384  lmodvnegcl  19387  lmodvnegid  19388  lmodvsubcl  19391  lmodcom  19392  lmodabl  19393  lmodvpncan  19399  lmodvnpcan  19400  lmodsubeq0  19405  lmodsubid  19406  lmodvsghm  19407  lmodprop2d  19408  lsssubg  19441  islss3  19443  lssacs  19451  prdslmodd  19453  lspsnneg  19490  lspsnsub  19491  lmodindp1  19498  lmodvsinv2  19521  islmhm2  19522  0lmhm  19524  idlmhm  19525  pwsdiaglmhm  19541  pwssplit3  19545  lspexch  19613  lspsolvlem  19626  mplind  19985  ip0l  20472  ipsubdir  20478  ipsubdi  20479  ip2eq  20489  lsmcss  20528  dsmmlss  20580  frlm0  20590  frlmsubgval  20601  frlmplusgvalb  20605  frlmup1  20634  islindf4  20674  matgrp  20733  tlmtgp  22497  clmgrp  23365  ncvspi  23453  cphtcphnm  23526  ipcau2  23530  tcphcphlem1  23531  tcphcph  23533  rrxnm  23687  rrxds  23689  pjthlem2  23734  lmodvslmhm  30483  eqgvscpbl  30554  imaslmod  30557  quslmod  30558  linds2eq  30568  lbslsat  30599  lindsunlem  30605  lbsdiflsp0  30607  dimkerim  30608  lclkrlem2m  38048  mapdpglem14  38214  baerlem3lem1  38236  baerlem5amN  38245  baerlem5bmN  38246  baerlem5abmN  38247  mapdh6bN  38266  mapdh6cN  38267  hdmap1l6b  38340  hdmap1l6c  38341  hdmap11  38377  lvecgrp  38528  frlmsnic  38531  kercvrlsm  39024  pwssplit4  39030  pwslnmlem2  39034  mendring  39133  zlmodzxzsub  43712  lmodvsmdi  43736  lincvalsng  43778  lincvalsc0  43783  linc0scn0  43785  linc1  43787  lcoel0  43790  lindslinindimp2lem4  43823  snlindsntor  43833  lincresunit3  43843