MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lsmelval Unicode version

Theorem lsmelval 16309
Description: Subgroup sum membership (for a left module or left vector space). (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
Hypotheses
Ref Expression
lsmelval.a
lsmelval.p
Assertion
Ref Expression
lsmelval
Distinct variable groups:   , ,   , ,   , ,   , ,   , ,

Proof of Theorem lsmelval
StepHypRef Expression
1 subgrcl 15845 . . 3
21adantr 465 . 2
3 eqid 2454 . . . 4
43subgss 15841 . . 3
54adantr 465 . 2
63subgss 15841 . . 3
76adantl 466 . 2
8 lsmelval.a . . 3
9 lsmelval.p . . 3
103, 8, 9lsmelvalx 16300 . 2
112, 5, 7, 10syl3anc 1219 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1370  e.wcel 1758  E.wrex 2801  C_wss 3442  `cfv 5537  (class class class)co 6222   cbs 14332   cplusg 14397   cgrp 15569   csubg 15834   clsm 16294
This theorem is referenced by:  lsmelvalm  16311  lsmsubg  16314  lsmcom2  16315  lsmmod  16333  lsmdisj2  16340  pj1eu  16354  lsmcl  17340  lsmspsn  17341  lsmelval2  17342  lsmcv  17398  lsmsat  33504  lshpsmreu  33605  dvhopellsm  35613  diblsmopel  35667  cdlemn11c  35705  dihord11c  35720  hdmapglem7a  36426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4520  ax-sep 4530  ax-nul 4538  ax-pow 4587  ax-pr 4648  ax-un 6505
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2805  df-rex 2806  df-reu 2807  df-rab 2809  df-v 3083  df-sbc 3298  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4209  df-iun 4290  df-br 4410  df-opab 4468  df-mpt 4469  df-id 4753  df-xp 4963  df-rel 4964  df-cnv 4965  df-co 4966  df-dm 4967  df-rn 4968  df-res 4969  df-ima 4970  df-iota 5500  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-ov 6225  df-oprab 6226  df-mpt2 6227  df-1st 6710  df-2nd 6711  df-subg 15837  df-lsm 16296
  Copyright terms: Public domain W3C validator