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