Theorem mrcrsp

Description: Moore closure generalizes ideal span. (Contributed by Stefan O'Rear, 4-Apr-2015)

	Ref	Expression
Hypotheses	mrcrsp.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
	mrcrsp.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
	mrcrsp.f	⊢ 𝐹 = ( mrCls ‘ 𝑈 )
Assertion	mrcrsp	⊢ ( 𝑅 ∈ Ring → 𝐾 = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		mrcrsp.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2		mrcrsp.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
3		mrcrsp.f	⊢ 𝐹 = ( mrCls ‘ 𝑈 )
4		rlmlmod	⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
5		lidlval	⊢ ( LIdeal ‘ 𝑅 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
6	1 5	eqtri	⊢ 𝑈 = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
7		rspval	⊢ ( RSpan ‘ 𝑅 ) = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
8	2 7	eqtri	⊢ 𝐾 = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
9	6 8 3	mrclsp	⊢ ( ( ringLMod ‘ 𝑅 ) ∈ LMod → 𝐾 = 𝐹 )
10	4 9	syl	⊢ ( 𝑅 ∈ Ring → 𝐾 = 𝐹 )