Metamath Proof Explorer

Theorem lspsslco

Description: Lemma for lspeqlco . (Contributed by AV, 17-Apr-2019)

Ref Expression
Hypothesis lspeqvlco.b 
|- B = ( Base ` M )
Assertion lspsslco 
|- ( ( M e. LMod /\ V e. ~P B ) -> ( ( LSpan ` M ) ` V ) C_ ( M LinCo V ) )

Proof

Step Hyp Ref Expression
1 lspeqvlco.b 
 |-  B = ( Base ` M )
2 simpl 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> M e. LMod )
3 1 pweqi 
 |-  ~P B = ~P ( Base ` M )
4 3 eleq2i 
 |-  ( V e. ~P B <-> V e. ~P ( Base ` M ) )
5 lincolss 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( M LinCo V ) e. ( LSubSp ` M ) )
6 4 5 sylan2b 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( M LinCo V ) e. ( LSubSp ` M ) )
7 lcoss 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> V C_ ( M LinCo V ) )
8 4 7 sylan2b 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> V C_ ( M LinCo V ) )
9 eqid 
 |-  ( LSubSp ` M ) = ( LSubSp ` M )
10 eqid 
 |-  ( LSpan ` M ) = ( LSpan ` M )
11 9 10 lspssp 
 |-  ( ( M e. LMod /\ ( M LinCo V ) e. ( LSubSp ` M ) /\ V C_ ( M LinCo V ) ) -> ( ( LSpan ` M ) ` V ) C_ ( M LinCo V ) )
12 2 6 8 11 syl3anc 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( ( LSpan ` M ) ` V ) C_ ( M LinCo V ) )