MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmodgrp Structured version   Visualization version   GIF version

Theorem lmodgrp 20343
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.
StepHypRef Expression
1 eqid 2733 . . 3 (Baseβ€˜π‘Š) = (Baseβ€˜π‘Š)
2 eqid 2733 . . 3 (+gβ€˜π‘Š) = (+gβ€˜π‘Š)
3 eqid 2733 . . 3 ( ·𝑠 β€˜π‘Š) = ( ·𝑠 β€˜π‘Š)
4 eqid 2733 . . 3 (Scalarβ€˜π‘Š) = (Scalarβ€˜π‘Š)
5 eqid 2733 . . 3 (Baseβ€˜(Scalarβ€˜π‘Š)) = (Baseβ€˜(Scalarβ€˜π‘Š))
6 eqid 2733 . . 3 (+gβ€˜(Scalarβ€˜π‘Š)) = (+gβ€˜(Scalarβ€˜π‘Š))
7 eqid 2733 . . 3 (.rβ€˜(Scalarβ€˜π‘Š)) = (.rβ€˜(Scalarβ€˜π‘Š))
8 eqid 2733 . . 3 (1rβ€˜(Scalarβ€˜π‘Š)) = (1rβ€˜(Scalarβ€˜π‘Š))
91, 2, 3, 4, 5, 6, 7, 8islmod 20340 . 2 (π‘Š ∈ LMod ↔ (π‘Š ∈ Grp ∧ (Scalarβ€˜π‘Š) ∈ Ring ∧ βˆ€π‘ž ∈ (Baseβ€˜(Scalarβ€˜π‘Š))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘Š))βˆ€π‘₯ ∈ (Baseβ€˜π‘Š)βˆ€π‘€ ∈ (Baseβ€˜π‘Š)(((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘ž( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘Š))π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘ž( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘Š))( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))))
109simp1bi 1146 1 (π‘Š ∈ LMod β†’ π‘Š ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3061  β€˜cfv 6497  (class class class)co 7358  Basecbs 17088  +gcplusg 17138  .rcmulr 17139  Scalarcsca 17141   ·𝑠 cvsca 17142  Grpcgrp 18753  1rcur 19918  Ringcrg 19969  LModclmod 20336
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5264
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2941  df-ral 3062  df-rab 3407  df-v 3446  df-sbc 3741  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361  df-lmod 20338
This theorem is referenced by:  lmodgrpd  20346  lmodbn0  20347  lmodvacl  20351  lmodass  20352  lmodlcan  20353  lmod0vcl  20366  lmod0vlid  20367  lmod0vrid  20368  lmod0vid  20369  lmodvsmmulgdi  20372  lmodfopne  20375  lmodvnegcl  20378  lmodvnegid  20379  lmodvsubcl  20382  lmodcom  20383  lmodabl  20384  lmodvpncan  20390  lmodvnpcan  20391  lmodsubeq0  20396  lmodsubid  20397  lmodvsghm  20398  lmodprop2d  20399  lsssubg  20433  islss3  20435  lssacs  20443  prdslmodd  20445  lspsnneg  20482  lspsnsub  20483  lmodindp1  20490  lmodvsinv2  20513  islmhm2  20514  0lmhm  20516  idlmhm  20517  pwsdiaglmhm  20533  pwssplit3  20537  lspexch  20606  lspsolvlem  20619  ip0l  21056  ipsubdir  21062  ipsubdi  21063  ip2eq  21073  lsmcss  21112  dsmmlss  21166  frlm0  21176  frlmsubgval  21187  frlmplusgvalb  21191  frlmup1  21220  islindf4  21260  mplind  21494  matgrp  21795  tlmtgp  23563  clmgrp  24447  ncvspi  24536  cphtcphnm  24610  ipcau2  24614  tcphcphlem1  24615  tcphcph  24617  rrxnm  24771  rrxds  24773  pjthlem2  24818  lmodvslmhm  31941  eqgvscpbl  32189  imaslmod  32192  quslmod  32193  linds2eq  32216  lbslsat  32368  lindsunlem  32376  lbsdiflsp0  32378  dimkerim  32379  lclkrlem2m  40028  mapdpglem14  40194  baerlem3lem1  40216  baerlem5amN  40225  baerlem5bmN  40226  baerlem5abmN  40227  mapdh6bN  40246  mapdh6cN  40247  hdmap1l6b  40320  hdmap1l6c  40321  hdmap11  40357  frlmsnic  40771  kercvrlsm  41453  pwssplit4  41459  pwslnmlem2  41463  mendring  41562  zlmodzxzsub  46522  lmodvsmdi  46544  lincvalsng  46583  lincvalsc0  46588  linc0scn0  46590  linc1  46592  lcoel0  46595  lindslinindimp2lem4  46628  snlindsntor  46638  lincresunit3  46648
  Copyright terms: Public domain W3C validator