Theorem lmodgrp 21122

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ‘cfv 6531  (class class class)co 7412  Basecbs 17367  +_gcplusg 17408  ._rcmulr 17409  Scalarcsca 17411   ·_𝑠 cvsca 17412  Grpcgrp 19124  1_rcur 20387  Ringcrg 20439  LModclmod 21115

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415  df-lmod 21117

This theorem is used by:  lmodgrpd  21125  lmodbn0  21126  lmodvacl  21130  lmodass  21131  lmodlcan  21132  lmod0vcl  21146  lmod0vlid  21147  lmod0vrid  21148  lmod0vid  21149  lmodvsmmulgdi  21152  lmodfopne  21155  lmodvnegcl  21158  lmodvnegid  21159  lmodvsubcl  21162  lmodcom  21163  lmodabl  21164  lmodvpncan  21170  lmodvnpcan  21171  lmodsubeq0  21176  lmodsubid  21177  lmodvsghm  21178  lmodprop2d  21179  lsssubg  21212  islss3  21214  lssacs  21222  prdslmodd  21224  lspsnneg  21261  lspsnsub  21262  lmodindp1  21269  lmodvsinv2  21292  islmhm2  21293  0lmhm  21295  idlmhm  21296  pwsdiaglmhm  21312  pwssplit3  21316  lspexch  21387  lspsolvlem  21400  ip0l  21922  ipsubdir  21928  ipsubdi  21929  ip2eq  21939  lsmcss  21978  dsmmlss  22030  frlm0  22040  frlmsubgval  22051  frlmplusgvalb  22055  frlmup1  22084  islindf4  22124  mplind  22359  matgrp  22725  tlmtgp  24495  clmgrp  25369  ncvspi  25457  cphtcphnm  25531  ipcau2  25535  tcphcphlem1  25536  tcphcph  25538  rrxnm  25692  rrxds  25694  pjthlem2  25739  lmodvslmhm  33593  eqgvscpbl  33893  imaslmod  33896  quslmod  33901  linds2eq  33918  lbslsat  34230  lindsunlem  34238  lbsdiflsp0  34240  dimkerim  34241  lclkrlem2m  42544  mapdpglem14  42710  baerlem3lem1  42732  baerlem5amN  42741  baerlem5bmN  42742  baerlem5abmN  42743  mapdh6bN  42762  mapdh6cN  42763  hdmap1l6b  42836  hdmap1l6c  42837  hdmap11  42873  frlmsnic  43566  kercvrlsm  44043  pwssplit4  44049  pwslnmlem2  44053  mendring  44148  zlmodzxzsub  49416  lmodvsmdi  49435  lincvalsng  49472  lincvalsc0  49477  linc0scn0  49479  linc1  49481  lcoel0  49484  lindslinindimp2lem4  49517  snlindsntor  49527  lincresunit3  49537