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 e. LMod -> S e. ( Moore ` B ) )

Proof

Step	Hyp	Ref	Expression
1		lssacs.b	|- B = ( Base ` W )
2		lssacs.s	|- S = ( LSubSp ` W )
3	1 2	lssss	|- ( a e. S -> a C_ B )
4		velpw	|- ( a e. ~P B <-> a C_ B )
5	3 4	sylibr	|- ( a e. S -> a e. ~P B )
6	5	a1i	|- ( W e. LMod -> ( a e. S -> a e. ~P B ) )
7	6	ssrdv	|- ( W e. LMod -> S C_ ~P B )
8	1 2	lss1	|- ( W e. LMod -> B e. S )
9	2	lssintcl	|- ( ( W e. LMod /\ a C_ S /\ a =/= (/) ) -> |^| a e. S )
10	7 8 9	ismred	|- ( W e. LMod -> S e. ( Moore ` B ) )