Theorem lmodgrp 21025

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 2766	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2766	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2766	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		eqid 2766	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2766	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6		eqid 2766	. . 3 ⊢ (+g‘(Scalar‘𝑊)) = (+g‘(Scalar‘𝑊))
7		eqid 2766	. . 3 ⊢ (.r‘(Scalar‘𝑊)) = (.r‘(Scalar‘𝑊))
8		eqid 2766	. . 3 ⊢ (1r‘(Scalar‘𝑊)) = (1r‘(Scalar‘𝑊))
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 21022	. 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 2146  ∀wral 3082  ‘cfv 6543  (class class class)co 7423  Basecbs 17294  +_gcplusg 17335  ._rcmulr 17336  Scalarcsca 17338   ·_𝑠 cvsca 17339  Grpcgrp 19031  1_rcur 20294  Ringcrg 20346  LModclmod 21018

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 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

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 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426  df-lmod 21020

This theorem is used by:  lmodgrpd  21028  lmodbn0  21029  lmodvacl  21033  lmodass  21034  lmodlcan  21035  lmod0vcl  21049  lmod0vlid  21050  lmod0vrid  21051  lmod0vid  21052  lmodvsmmulgdi  21055  lmodfopne  21058  lmodvnegcl  21061  lmodvnegid  21062  lmodvsubcl  21065  lmodcom  21066  lmodabl  21067  lmodvpncan  21073  lmodvnpcan  21074  lmodsubeq0  21079  lmodsubid  21080  lmodvsghm  21081  lmodprop2d  21082  lsssubg  21115  islss3  21117  lssacs  21125  prdslmodd  21127  lspsnneg  21164  lspsnsub  21165  lmodindp1  21172  lmodvsinv2  21195  islmhm2  21196  0lmhm  21198  idlmhm  21199  pwsdiaglmhm  21215  pwssplit3  21219  lspexch  21290  lspsolvlem  21303  ip0l  21823  ipsubdir  21829  ipsubdi  21830  ip2eq  21840  lsmcss  21879  dsmmlss  21931  frlm0  21941  frlmsubgval  21952  frlmplusgvalb  21956  frlmup1  21985  islindf4  22025  mplind  22258  matgrp  22624  tlmtgp  24390  clmgrp  25264  ncvspi  25352  cphtcphnm  25426  ipcau2  25430  tcphcphlem1  25431  tcphcph  25433  rrxnm  25587  rrxds  25589  pjthlem2  25634  lmodvslmhm  33401  eqgvscpbl  33701  imaslmod  33704  quslmod  33709  linds2eq  33725  lbslsat  34037  lindsunlem  34045  lbsdiflsp0  34047  dimkerim  34048  lclkrlem2m  42334  mapdpglem14  42500  baerlem3lem1  42522  baerlem5amN  42531  baerlem5bmN  42532  baerlem5abmN  42533  mapdh6bN  42552  mapdh6cN  42553  hdmap1l6b  42626  hdmap1l6c  42627  hdmap11  42663  frlmsnic  43349  kercvrlsm  43851  pwssplit4  43857  pwslnmlem2  43861  mendring  43956  zlmodzxzsub  49181  lmodvsmdi  49200  lincvalsng  49237  lincvalsc0  49242  linc0scn0  49244  linc1  49246  lcoel0  49249  lindslinindimp2lem4  49282  snlindsntor  49292  lincresunit3  49302