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

Metamath Proof Explorer

Theorem lssmre

Description: The subspaces of a module comprise a Moore system on the vectors of the module. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypotheses lssacs.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
lssacs.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion lssmre ( 𝑊 ∈ LMod → 𝑆 ∈ ( Moore ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 lssacs.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 lssacs.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 1 2 lssss ⊢ ( 𝑎 ∈ 𝑆 → 𝑎 ⊆ 𝐵 )
4 velpw ⊢ ( 𝑎 ∈ 𝒫 𝐵 ↔ 𝑎 ⊆ 𝐵 )
5 3 4 sylibr ⊢ ( 𝑎 ∈ 𝑆 → 𝑎 ∈ 𝒫 𝐵 )
6 5 a1i ⊢ ( 𝑊 ∈ LMod → ( 𝑎 ∈ 𝑆 → 𝑎 ∈ 𝒫 𝐵 ) )
7 6 ssrdv ⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ 𝒫 𝐵 )
8 1 2 lss1 ⊢ ( 𝑊 ∈ LMod → 𝐵 ∈ 𝑆 )
9 2 lssintcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ⊆ 𝑆 ∧ 𝑎 ≠ ∅ ) → ∩ 𝑎 ∈ 𝑆 )
10 7 8 9 ismred ⊢ ( 𝑊 ∈ LMod → 𝑆 ∈ ( Moore ‘ 𝐵 ) )