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 ⊢ 𝑈 = ( LSubSp ‘ 𝑊 )
mrclsp.k ⊢ 𝐾 = ( LSpan ‘ 𝑊 )
mrclsp.f ⊢ 𝐹 = ( mrCls ‘ 𝑈 )
Assertion mrclsp ( 𝑊 ∈ LMod → 𝐾 = 𝐹 )

Proof

Step Hyp Ref Expression
1 mrclsp.u ⊢ 𝑈 = ( LSubSp ‘ 𝑊 )
2 mrclsp.k ⊢ 𝐾 = ( LSpan ‘ 𝑊 )
3 mrclsp.f ⊢ 𝐹 = ( mrCls ‘ 𝑈 )
4 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
5 4 1 2 lspfval ⊢ ( 𝑊 ∈ LMod → 𝐾 = ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑊 ) ↦ ∩ { 𝑏 ∈ 𝑈 ∣ 𝑎 ⊆ 𝑏 } ) )
6 4 1 lssmre ⊢ ( 𝑊 ∈ LMod → 𝑈 ∈ ( Moore ‘ ( Base ‘ 𝑊 ) ) )
7 3 mrcfval ⊢ ( 𝑈 ∈ ( Moore ‘ ( Base ‘ 𝑊 ) ) → 𝐹 = ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑊 ) ↦ ∩ { 𝑏 ∈ 𝑈 ∣ 𝑎 ⊆ 𝑏 } ) )
8 6 7 syl ⊢ ( 𝑊 ∈ LMod → 𝐹 = ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑊 ) ↦ ∩ { 𝑏 ∈ 𝑈 ∣ 𝑎 ⊆ 𝑏 } ) )
9 5 8 eqtr4d ⊢ ( 𝑊 ∈ LMod → 𝐾 = 𝐹 )