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

Metamath Proof Explorer

Theorem mrclsp

Description: Moore closure generalizes module span. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypotheses mrclsp.u ⊢ U = LSubSp ⁡ W
mrclsp.k ⊢ K = LSpan ⁡ W
mrclsp.f ⊢ F = mrCls ⁡ U
Assertion mrclsp ⊢ W ∈ LMod → K = F

Proof

Step Hyp Ref Expression
1 mrclsp.u ⊢ U = LSubSp ⁡ W
2 mrclsp.k ⊢ K = LSpan ⁡ W
3 mrclsp.f ⊢ F = mrCls ⁡ U
4 eqid ⊢ Base W = Base W
5 4 1 2 lspfval ⊢ W ∈ LMod → K = a ∈ 𝒫 Base W ⟼ ⋂ b ∈ U | a ⊆ b
6 4 1 lssmre ⊢ W ∈ LMod → U ∈ Moore ⁡ Base W
7 3 mrcfval ⊢ U ∈ Moore ⁡ Base W → F = a ∈ 𝒫 Base W ⟼ ⋂ b ∈ U | a ⊆ b
8 6 7 syl ⊢ W ∈ LMod → F = a ∈ 𝒫 Base W ⟼ ⋂ b ∈ U | a ⊆ b
9 5 8 eqtr4d ⊢ W ∈ LMod → K = F