Metamath Proof Explorer


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 = RSpan R
rsp0.z 0 ˙ = 0 R
Assertion rsp0 R Ring K 0 ˙ = 0 ˙

Proof

Step Hyp Ref Expression
1 rspcl.k K = RSpan R
2 rsp0.z 0 ˙ = 0 R
3 rlmlmod R Ring ringLMod R LMod
4 rlm0 0 R = 0 ringLMod R
5 2 4 eqtri 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 LMod K 0 ˙ = 0 ˙
9 3 8 syl R Ring K 0 ˙ = 0 ˙