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