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 = RSpan (R)$
	rsp0.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	rsp0	$⊢ R \in Ring \to K (\{\underset{˙}{0}\}) = \{\underset{˙}{0}\}$

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

Metamath Proof Explorer