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

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

Proof of Theorem rlmval
Dummy variable  a is distinct from all other variables.
StepHypRef Expression
1 fveq2 5877 . . . 4  |-  ( a  =  W  ->  (subringAlg  `  a )  =  (subringAlg  `  W ) )
2 fveq2 5877 . . . 4  |-  ( a  =  W  ->  ( Base `  a )  =  ( Base `  W
) )
31, 2fveq12d 5883 . . 3  |-  ( a  =  W  ->  (
(subringAlg  `  a ) `  ( Base `  a )
)  =  ( (subringAlg  `  W ) `  ( Base `  W ) ) )
4 df-rgmod 18383 . . 3  |- ringLMod  =  ( a  e.  _V  |->  ( (subringAlg  `  a ) `  ( Base `  a )
) )
5 fvex 5887 . . 3  |-  ( (subringAlg  `  W ) `  ( Base `  W ) )  e.  _V
63, 4, 5fvmpt 5960 . 2  |-  ( W  e.  _V  ->  (ringLMod `  W )  =  ( (subringAlg  `  W ) `  ( Base `  W )
) )
7 0fv 5910 . . . 4  |-  ( (/) `  ( Base `  W
) )  =  (/)
87eqcomi 2435 . . 3  |-  (/)  =  (
(/) `  ( Base `  W ) )
9 fvprc 5871 . . 3  |-  ( -.  W  e.  _V  ->  (ringLMod `  W )  =  (/) )
10 fvprc 5871 . . . 4  |-  ( -.  W  e.  _V  ->  (subringAlg  `  W )  =  (/) )
1110fveq1d 5879 . . 3  |-  ( -.  W  e.  _V  ->  ( (subringAlg  `  W ) `  ( Base `  W )
)  =  ( (/) `  ( Base `  W
) ) )
128, 9, 113eqtr4a 2489 . 2  |-  ( -.  W  e.  _V  ->  (ringLMod `  W )  =  ( (subringAlg  `  W ) `  ( Base `  W )
) )
136, 12pm2.61i 167 1  |-  (ringLMod `  W
)  =  ( (subringAlg  `  W ) `  ( Base `  W ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1437    e. wcel 1868   _Vcvv 3081   (/)c0 3761   ` cfv 5597   Basecbs 15108  subringAlg csra 18378  ringLModcrglmod 18379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-iota 5561  df-fun 5599  df-fv 5605  df-rgmod 18383
This theorem is referenced by:  rlmval2  18404  rlmbas  18405  rlmplusg  18406  rlm0  18407  rlmmulr  18409  rlmsca  18410  rlmsca2  18411  rlmvsca  18412  rlmtopn  18413  rlmds  18414  rlmlmod  18415  rlmassa  18537  frlmip  19322  rlmnlm  21677  rlmbn  22314  rrxprds  22334
  Copyright terms: Public domain W3C validator