Theorem rspval

Description: Value of the ring span function. (Contributed by Stefan O'Rear, 4-Apr-2015)

	Ref	Expression
Assertion	rspval	$$⊢\mathrm{RSpan}\left(W\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(W\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-rsp	$$⊢\mathrm{RSpan}=\mathrm{LSpan}\circ \mathrm{ringLMod}$$
2	1	fveq1i	$$⊢\mathrm{RSpan}\left(W\right)=\left(\mathrm{LSpan}\circ \mathrm{ringLMod}\right)\left(W\right)$$
3		00lsp	$$⊢\varnothing =\mathrm{LSpan}\left(\varnothing \right)$$
4		rlmfn	$$⊢\mathrm{ringLMod}Fn\mathrm{V}$$
5		fnfun	$$⊢\mathrm{ringLMod}Fn\mathrm{V}\to \mathrm{Fun}\mathrm{ringLMod}$$
6	4 5	ax-mp	$$⊢\mathrm{Fun}\mathrm{ringLMod}$$
7	3 6	fvco4i	$$⊢\left(\mathrm{LSpan}\circ \mathrm{ringLMod}\right)\left(W\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(W\right)\right)$$
8	2 7	eqtri	$$⊢\mathrm{RSpan}\left(W\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(W\right)\right)$$