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

Theorem lmodlema 17043
Description: Lemma for properties of a left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
Hypotheses
Ref Expression
islmod.v
islmod.a
islmod.s
islmod.f
islmod.k
islmod.p
islmod.t
islmod.u
Assertion
Ref Expression
lmodlema

Proof of Theorem lmodlema
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 islmod.v . . . . . 6
2 islmod.a . . . . . 6
3 islmod.s . . . . . 6
4 islmod.f . . . . . 6
5 islmod.k . . . . . 6
6 islmod.p . . . . . 6
7 islmod.t . . . . . 6
8 islmod.u . . . . . 6
91, 2, 3, 4, 5, 6, 7, 8islmod 17042 . . . . 5
109simp3bi 1005 . . . 4
11 oveq1 6181 . . . . . . . . . 10
1211oveq1d 6189 . . . . . . . . 9
13 oveq1 6181 . . . . . . . . . 10
1413oveq1d 6189 . . . . . . . . 9
1512, 14eqeq12d 2471 . . . . . . . 8
16153anbi3d 1296 . . . . . . 7
17 oveq1 6181 . . . . . . . . . 10
1817oveq1d 6189 . . . . . . . . 9
19 oveq1 6181 . . . . . . . . 9
2018, 19eqeq12d 2471 . . . . . . . 8
2120anbi1d 704 . . . . . . 7
2216, 21anbi12d 710 . . . . . 6
23222ralbidv 2831 . . . . 5
24 oveq1 6181 . . . . . . . . 9
2524eleq1d 2518 . . . . . . . 8
26 oveq1 6181 . . . . . . . . 9
27 oveq1 6181 . . . . . . . . . 10
2824, 27oveq12d 6192 . . . . . . . . 9
2926, 28eqeq12d 2471 . . . . . . . 8
30 oveq2 6182 . . . . . . . . . 10
3130oveq1d 6189 . . . . . . . . 9
3224oveq2d 6190 . . . . . . . . 9
3331, 32eqeq12d 2471 . . . . . . . 8
3425, 29, 333anbi123d 1290 . . . . . . 7
35 oveq2 6182 . . . . . . . . . 10
3635oveq1d 6189 . . . . . . . . 9
3724oveq2d 6190 . . . . . . . . 9
3836, 37eqeq12d 2471 . . . . . . . 8
3938anbi1d 704 . . . . . . 7
4034, 39anbi12d 710 . . . . . 6
41402ralbidv 2831 . . . . 5
4223, 41rspc2v 3160 . . . 4
4310, 42mpan9 469 . . 3
44 oveq2 6182 . . . . . . . 8
4544oveq2d 6190 . . . . . . 7
46 oveq2 6182 . . . . . . . 8
4746oveq2d 6190 . . . . . . 7
4845, 47eqeq12d 2471 . . . . . 6
49483anbi2d 1295 . . . . 5
5049anbi1d 704 . . . 4
51 oveq2 6182 . . . . . . 7
5251eleq1d 2518 . . . . . 6
53 oveq1 6181 . . . . . . . 8
5453oveq2d 6190 . . . . . . 7
5551oveq1d 6189 . . . . . . 7
5654, 55eqeq12d 2471 . . . . . 6
57 oveq2 6182 . . . . . . 7
58 oveq2 6182 . . . . . . . 8
5958, 51oveq12d 6192 . . . . . . 7
6057, 59eqeq12d 2471 . . . . . 6
6152, 56, 603anbi123d 1290 . . . . 5
62 oveq2 6182 . . . . . . 7
6351oveq2d 6190 . . . . . . 7
6462, 63eqeq12d 2471 . . . . . 6
65 oveq2 6182 . . . . . . 7
66 id 22 . . . . . . 7
6765, 66eqeq12d 2471 . . . . . 6
6864, 67anbi12d 710 . . . . 5
6961, 68anbi12d 710 . . . 4
7050, 69rspc2v 3160 . . 3
7143, 70syl5com 30 . 2
72713impia 1185 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 965  =wceq 1370  e.wcel 1757  A.wral 2792  `cfv 5500  (class class class)co 6174   cbs 14260   cplusg 14324   cmulr 14325   csca 14327   cvsca 14328   cgrp 15496   cur 16692   crg 16735   clmod 17038
This theorem is referenced by:  lmodvscl  17055  lmodvsdi  17061  lmodvsdir  17062  lmodvsass  17063  lmodvs1  17066
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 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-nul 4503
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 1702  df-eu 2263  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3054  df-sbc 3269  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-nul 3720  df-if 3874  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4174  df-br 4375  df-iota 5463  df-fv 5508  df-ov 6177  df-lmod 17040
  Copyright terms: Public domain W3C validator