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

Theorem rlmval 19685
Description: Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
Assertion
Ref Expression
rlmval (ringLMod‘𝑊) = ((subringAlg ‘𝑊)‘(Base‘𝑊))

Proof of Theorem rlmval
Dummy variable 𝑎 is distinct from all other variables.
StepHypRef Expression
1 fveq2 6499 . . . 4 (𝑎 = 𝑊 → (subringAlg ‘𝑎) = (subringAlg ‘𝑊))
2 fveq2 6499 . . . 4 (𝑎 = 𝑊 → (Base‘𝑎) = (Base‘𝑊))
31, 2fveq12d 6506 . . 3 (𝑎 = 𝑊 → ((subringAlg ‘𝑎)‘(Base‘𝑎)) = ((subringAlg ‘𝑊)‘(Base‘𝑊)))
4 df-rgmod 19667 . . 3 ringLMod = (𝑎 ∈ V ↦ ((subringAlg ‘𝑎)‘(Base‘𝑎)))
5 fvex 6512 . . 3 ((subringAlg ‘𝑊)‘(Base‘𝑊)) ∈ V
63, 4, 5fvmpt 6595 . 2 (𝑊 ∈ V → (ringLMod‘𝑊) = ((subringAlg ‘𝑊)‘(Base‘𝑊)))
7 0fv 6539 . . . 4 (∅‘(Base‘𝑊)) = ∅
87eqcomi 2787 . . 3 ∅ = (∅‘(Base‘𝑊))
9 fvprc 6492 . . 3 𝑊 ∈ V → (ringLMod‘𝑊) = ∅)
10 fvprc 6492 . . . 4 𝑊 ∈ V → (subringAlg ‘𝑊) = ∅)
1110fveq1d 6501 . . 3 𝑊 ∈ V → ((subringAlg ‘𝑊)‘(Base‘𝑊)) = (∅‘(Base‘𝑊)))
128, 9, 113eqtr4a 2840 . 2 𝑊 ∈ V → (ringLMod‘𝑊) = ((subringAlg ‘𝑊)‘(Base‘𝑊)))
136, 12pm2.61i 177 1 (ringLMod‘𝑊) = ((subringAlg ‘𝑊)‘(Base‘𝑊))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1507  wcel 2050  Vcvv 3415  c0 4178  cfv 6188  Basecbs 16339  subringAlg csra 19662  ringLModcrglmod 19663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3682  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-mpt 5009  df-id 5312  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-iota 6152  df-fun 6190  df-fv 6196  df-rgmod 19667
This theorem is referenced by:  rlmval2  19688  rlmbas  19689  rlmplusg  19690  rlm0  19691  rlmmulr  19693  rlmsca  19694  rlmsca2  19695  rlmvsca  19696  rlmtopn  19697  rlmds  19698  rlmlmod  19699  rlmassa  19820  frlmip  20624  rlmnlm  23000  rlmbn  23667  rrxprds  23695  rgmoddim  30643  extdgid  30685
  Copyright terms: Public domain W3C validator