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

Metamath Proof Explorer

Theorem mrcrsp

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

Ref Expression
Hypotheses mrcrsp.u ⊢ U = LIdeal ⁡ R
mrcrsp.k ⊢ K = RSpan ⁡ R
mrcrsp.f ⊢ F = mrCls ⁡ U
Assertion mrcrsp ⊢ R ∈ Ring → K = F

Proof

Step Hyp Ref Expression
1 mrcrsp.u ⊢ U = LIdeal ⁡ R
2 mrcrsp.k ⊢ K = RSpan ⁡ R
3 mrcrsp.f ⊢ F = mrCls ⁡ U
4 rlmlmod ⊢ R ∈ Ring → ringLMod ⁡ R ∈ LMod
5 lidlval ⊢ LIdeal ⁡ R = LSubSp ⁡ ringLMod ⁡ R
6 1 5 eqtri ⊢ U = LSubSp ⁡ ringLMod ⁡ R
7 rspval ⊢ RSpan ⁡ R = LSpan ⁡ ringLMod ⁡ R
8 2 7 eqtri ⊢ K = LSpan ⁡ ringLMod ⁡ R
9 6 8 3 mrclsp ⊢ ringLMod ⁡ R ∈ LMod → K = F
10 4 9 syl ⊢ R ∈ Ring → K = F