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 ⊢ B = Base W
lssacs.s ⊢ S = LSubSp ⁡ W
Assertion lssmre ⊢ W ∈ LMod → S ∈ Moore ⁡ B

Proof

Step Hyp Ref Expression
1 lssacs.b ⊢ B = Base W
2 lssacs.s ⊢ S = LSubSp ⁡ W
3 1 2 lssss ⊢ a ∈ S → a ⊆ B
4 velpw ⊢ a ∈ 𝒫 B ↔ a ⊆ B
5 3 4 sylibr ⊢ a ∈ S → a ∈ 𝒫 B
6 5 a1i ⊢ W ∈ LMod → a ∈ S → a ∈ 𝒫 B
7 6 ssrdv ⊢ W ∈ LMod → S ⊆ 𝒫 B
8 1 2 lss1 ⊢ W ∈ LMod → B ∈ S
9 2 lssintcl ⊢ W ∈ LMod ∧ a ⊆ S ∧ a ≠ ∅ → ⋂ a ∈ S
10 7 8 9 ismred ⊢ W ∈ LMod → S ∈ Moore ⁡ B