Metamath Proof Explorer

Theorem lcosslsp

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

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

Proof

Step Hyp Ref Expression
1 lspeqvlco.b 
 |-  B = ( Base ` M )
2 ellcoellss 
 |-  ( ( M e. LMod /\ s e. ( LSubSp ` M ) /\ V C_ s ) -> A. y e. ( M LinCo V ) y e. s )
3 2 3exp 
 |-  ( M e. LMod -> ( s e. ( LSubSp ` M ) -> ( V C_ s -> A. y e. ( M LinCo V ) y e. s ) ) )
4 3 ad2antrr 
 |-  ( ( ( M e. LMod /\ V e. ~P B ) /\ x e. ( M LinCo V ) ) -> ( s e. ( LSubSp ` M ) -> ( V C_ s -> A. y e. ( M LinCo V ) y e. s ) ) )
5 4 imp 
 |-  ( ( ( ( M e. LMod /\ V e. ~P B ) /\ x e. ( M LinCo V ) ) /\ s e. ( LSubSp ` M ) ) -> ( V C_ s -> A. y e. ( M LinCo V ) y e. s ) )
6 elequ1 
 |-  ( y = x -> ( y e. s <-> x e. s ) )
7 6 rspcv 
 |-  ( x e. ( M LinCo V ) -> ( A. y e. ( M LinCo V ) y e. s -> x e. s ) )
8 7 ad2antlr 
 |-  ( ( ( ( M e. LMod /\ V e. ~P B ) /\ x e. ( M LinCo V ) ) /\ s e. ( LSubSp ` M ) ) -> ( A. y e. ( M LinCo V ) y e. s -> x e. s ) )
9 5 8 syld 
 |-  ( ( ( ( M e. LMod /\ V e. ~P B ) /\ x e. ( M LinCo V ) ) /\ s e. ( LSubSp ` M ) ) -> ( V C_ s -> x e. s ) )
10 9 ralrimiva 
 |-  ( ( ( M e. LMod /\ V e. ~P B ) /\ x e. ( M LinCo V ) ) -> A. s e. ( LSubSp ` M ) ( V C_ s -> x e. s ) )
11 vex 
 |-  x e. _V
12 11 elintrab 
 |-  ( x e. |^| { s e. ( LSubSp ` M ) | V C_ s } <-> A. s e. ( LSubSp ` M ) ( V C_ s -> x e. s ) )
13 10 12 sylibr 
 |-  ( ( ( M e. LMod /\ V e. ~P B ) /\ x e. ( M LinCo V ) ) -> x e. |^| { s e. ( LSubSp ` M ) | V C_ s } )
14 simpll 
 |-  ( ( ( M e. LMod /\ V e. ~P B ) /\ x e. ( M LinCo V ) ) -> M e. LMod )
15 elpwi 
 |-  ( V e. ~P B -> V C_ B )
16 15 ad2antlr 
 |-  ( ( ( M e. LMod /\ V e. ~P B ) /\ x e. ( M LinCo V ) ) -> V C_ B )
17 eqid 
 |-  ( LSubSp ` M ) = ( LSubSp ` M )
18 eqid 
 |-  ( LSpan ` M ) = ( LSpan ` M )
19 1 17 18 lspval 
 |-  ( ( M e. LMod /\ V C_ B ) -> ( ( LSpan ` M ) ` V ) = |^| { s e. ( LSubSp ` M ) | V C_ s } )
20 14 16 19 syl2anc 
 |-  ( ( ( M e. LMod /\ V e. ~P B ) /\ x e. ( M LinCo V ) ) -> ( ( LSpan ` M ) ` V ) = |^| { s e. ( LSubSp ` M ) | V C_ s } )
21 13 20 eleqtrrd 
 |-  ( ( ( M e. LMod /\ V e. ~P B ) /\ x e. ( M LinCo V ) ) -> x e. ( ( LSpan ` M ) ` V ) )
22 21 ex 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( x e. ( M LinCo V ) -> x e. ( ( LSpan ` M ) ` V ) ) )
23 22 ssrdv 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( M LinCo V ) C_ ( ( LSpan ` M ) ` V ) )