Theorem rsp0

Description: The span of the zero element is the zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	rspcl.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
	rsp0.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	rsp0	$$⊢R\in \mathrm{Ring}\to K\left(\left\{\underset{\dot{}}{0}\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		rspcl.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
2		rsp0.z	$$⊢\underset{\dot{}}{0}=0_R$$
3		rlmlmod	$$⊢R\in \mathrm{Ring}\to \mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}$$
4		rlm0	$$⊢0_R=0_{\mathrm{ringLMod}\left(R\right)}$$
5	2 4	eqtri	$$⊢\underset{\dot{}}{0}=0_{\mathrm{ringLMod}\left(R\right)}$$
6		rspval	$$⊢\mathrm{RSpan}\left(R\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)$$
7	1 6	eqtri	$$⊢K=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)$$
8	5 7	lspsn0	$$⊢\mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}\to K\left(\left\{\underset{\dot{}}{0}\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
9	3 8	syl	$$⊢R\in \mathrm{Ring}\to K\left(\left\{\underset{\dot{}}{0}\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$