Metamath Proof Explorer

Theorem lspf

Description: The span function on a left module maps subsets to subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014)

Ref Expression
Hypotheses lspval.v 
|- V = ( Base ` W )
lspval.s 
|- S = ( LSubSp ` W )
lspval.n 
|- N = ( LSpan ` W )
Assertion lspf 
|- ( W e. LMod -> N : ~P V --> S )

Proof

Step Hyp Ref Expression
1 lspval.v 
 |-  V = ( Base ` W )
2 lspval.s 
 |-  S = ( LSubSp ` W )
3 lspval.n 
 |-  N = ( LSpan ` W )
4 1 2 3 lspfval 
 |-  ( W e. LMod -> N = ( s e. ~P V |-> |^| { p e. S | s C_ p } ) )
5 simpl 
 |-  ( ( W e. LMod /\ s e. ~P V ) -> W e. LMod )
6 ssrab2 
 |-  { p e. S | s C_ p } C_ S
7 6 a1i 
 |-  ( ( W e. LMod /\ s e. ~P V ) -> { p e. S | s C_ p } C_ S )
8 1 2 lss1 
 |-  ( W e. LMod -> V e. S )
9 elpwi 
 |-  ( s e. ~P V -> s C_ V )
10 sseq2 
 |-  ( p = V -> ( s C_ p <-> s C_ V ) )
11 10 rspcev 
 |-  ( ( V e. S /\ s C_ V ) -> E. p e. S s C_ p )
12 8 9 11 syl2an 
 |-  ( ( W e. LMod /\ s e. ~P V ) -> E. p e. S s C_ p )
13 rabn0 
 |-  ( { p e. S | s C_ p } =/= (/) <-> E. p e. S s C_ p )
14 12 13 sylibr 
 |-  ( ( W e. LMod /\ s e. ~P V ) -> { p e. S | s C_ p } =/= (/) )
15 2 lssintcl 
 |-  ( ( W e. LMod /\ { p e. S | s C_ p } C_ S /\ { p e. S | s C_ p } =/= (/) ) -> |^| { p e. S | s C_ p } e. S )
16 5 7 14 15 syl3anc 
 |-  ( ( W e. LMod /\ s e. ~P V ) -> |^| { p e. S | s C_ p } e. S )
17 4 16 fmpt3d 
 |-  ( W e. LMod -> N : ~P V --> S )