![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rspval | Structured version Visualization version GIF version |
Description: Value of the ring span function. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
Ref | Expression |
---|---|
rspval | ⊢ (RSpan‘𝑊) = (LSpan‘(ringLMod‘𝑊)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rsp 20000 | . . 3 ⊢ RSpan = (LSpan ∘ ringLMod) | |
2 | 1 | fveq1i 6652 | . 2 ⊢ (RSpan‘𝑊) = ((LSpan ∘ ringLMod)‘𝑊) |
3 | 00lsp 19806 | . . 3 ⊢ ∅ = (LSpan‘∅) | |
4 | rlmfn 20015 | . . . 4 ⊢ ringLMod Fn V | |
5 | fnfun 6427 | . . . 4 ⊢ (ringLMod Fn V → Fun ringLMod) | |
6 | 4, 5 | ax-mp 5 | . . 3 ⊢ Fun ringLMod |
7 | 3, 6 | fvco4i 6746 | . 2 ⊢ ((LSpan ∘ ringLMod)‘𝑊) = (LSpan‘(ringLMod‘𝑊)) |
8 | 2, 7 | eqtri 2782 | 1 ⊢ (RSpan‘𝑊) = (LSpan‘(ringLMod‘𝑊)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 Vcvv 3407 ∘ ccom 5521 Fun wfun 6322 Fn wfn 6323 ‘cfv 6328 LSpanclspn 19796 ringLModcrglmod 19994 RSpancrsp 19996 |
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 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-rep 5149 ax-sep 5162 ax-nul 5169 ax-pow 5227 ax-pr 5291 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2899 df-ne 2950 df-ral 3073 df-rex 3074 df-reu 3075 df-rab 3077 df-v 3409 df-sbc 3694 df-csb 3802 df-dif 3857 df-un 3859 df-in 3861 df-ss 3871 df-nul 4222 df-if 4414 df-pw 4489 df-sn 4516 df-pr 4518 df-op 4522 df-uni 4792 df-int 4832 df-iun 4878 df-br 5026 df-opab 5088 df-mpt 5106 df-id 5423 df-xp 5523 df-rel 5524 df-cnv 5525 df-co 5526 df-dm 5527 df-rn 5528 df-res 5529 df-ima 5530 df-iota 6287 df-fun 6330 df-fn 6331 df-f 6332 df-f1 6333 df-fo 6334 df-f1o 6335 df-fv 6336 df-ov 7146 df-slot 16530 df-base 16532 df-lss 19757 df-lsp 19797 df-rgmod 19998 df-rsp 20000 |
This theorem is referenced by: rspcl 20048 rspssid 20049 rsp0 20051 rspssp 20052 mrcrsp 20053 lidlrsppropd 20056 rspsn 20080 rspsnel 31073 elrsp 31075 lsmidllsp 31094 lsmidl 31095 mxidlprm 31146 idlsrgmulrss1 31162 idlsrgmulrss2 31163 rgmoddim 31199 islnr2 40416 |
Copyright terms: Public domain | W3C validator |