Theorem rspval

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

	Ref	Expression
Assertion	rspval	⊢ ( RSpan ‘ 𝑊 ) = ( LSpan ‘ ( ringLMod ‘ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		df-rsp	⊢ RSpan = ( LSpan ∘ ringLMod )
2	1	fveq1i	⊢ ( RSpan ‘ 𝑊 ) = ( ( LSpan ∘ ringLMod ) ‘ 𝑊 )
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 ∘ ringLMod ) ‘ 𝑊 ) = ( LSpan ‘ ( ringLMod ‘ 𝑊 ) )
8	2 7	eqtri	⊢ ( RSpan ‘ 𝑊 ) = ( LSpan ‘ ( ringLMod ‘ 𝑊 ) )