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 ‘ 𝐵 ) )