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={\mathrm{Base}}_W$$
	lssacs.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
Assertion	lssmre	$$⊢W\in \mathrm{LMod}\to S\in \mathrm{Moore}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		lssacs.b	$$⊢B={\mathrm{Base}}_W$$
2		lssacs.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
3	1 2	lssss	$$⊢a\in S\to a\subseteq B$$
4		velpw	$$⊢a\in 𝒫B\leftrightarrow a\subseteq B$$
5	3 4	sylibr	$$⊢a\in S\to a\in 𝒫B$$
6	5	a1i	$$⊢W\in \mathrm{LMod}\to \left(a\in S\to a\in 𝒫B\right)$$
7	6	ssrdv	$$⊢W\in \mathrm{LMod}\to S\subseteq 𝒫B$$
8	1 2	lss1	$$⊢W\in \mathrm{LMod}\to B\in S$$
9	2	lssintcl	$$⊢\left(W\in \mathrm{LMod}\wedge a\subseteq S\wedge a\ne \varnothing \right)\to \bigcap a\in S$$
10	7 8 9	ismred	$$⊢W\in \mathrm{LMod}\to S\in \mathrm{Moore}\left(B\right)$$