Theorem rspval

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

	Ref	Expression
Assertion	rspval	|- ( RSpan ` W ) = ( LSpan ` ( ringLMod ` W ) )

Proof

Step	Hyp	Ref	Expression
1		df-rsp	|- RSpan = ( LSpan o. ringLMod )
2	1	fveq1i	|- ( RSpan ` W ) = ( ( LSpan o. ringLMod ) ` W )
3		00lsp	|- (/) = ( LSpan ` (/) )
4		rlmfn	|- ringLMod Fn _V
5		fnfun	|- ( ringLMod Fn _V -> Fun ringLMod )
6	4 5	ax-mp	|- Fun ringLMod
7	3 6	fvco4i	|- ( ( LSpan o. ringLMod ) ` W ) = ( LSpan ` ( ringLMod ` W ) )
8	2 7	eqtri	|- ( RSpan ` W ) = ( LSpan ` ( ringLMod ` W ) )