This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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))$

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