Metamath Proof Explorer

Theorem islssfgi

Description: Finitely spanned subspaces are finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypotheses islssfgi.n 
|- N = ( LSpan ` W )
islssfgi.v 
|- V = ( Base ` W )
islssfgi.x 
|- X = ( W |`s ( N ` B ) )
Assertion islssfgi 
|- ( ( W e. LMod /\ B C_ V /\ B e. Fin ) -> X e. LFinGen )

Proof

Step Hyp Ref Expression
1 islssfgi.n 
 |-  N = ( LSpan ` W )
2 islssfgi.v 
 |-  V = ( Base ` W )
3 islssfgi.x 
 |-  X = ( W |`s ( N ` B ) )
4 2 fvexi 
 |-  V e. _V
5 4 elpw2 
 |-  ( B e. ~P V <-> B C_ V )
6 5 biimpri 
 |-  ( B C_ V -> B e. ~P V )
7 6 3ad2ant2 
 |-  ( ( W e. LMod /\ B C_ V /\ B e. Fin ) -> B e. ~P V )
8 simp3 
 |-  ( ( W e. LMod /\ B C_ V /\ B e. Fin ) -> B e. Fin )
9 7 8 elind 
 |-  ( ( W e. LMod /\ B C_ V /\ B e. Fin ) -> B e. ( ~P V i^i Fin ) )
10 eqid 
 |-  ( N ` B ) = ( N ` B )
11 fveqeq2 
 |-  ( a = B -> ( ( N ` a ) = ( N ` B ) <-> ( N ` B ) = ( N ` B ) ) )
12 11 rspcev 
 |-  ( ( B e. ( ~P V i^i Fin ) /\ ( N ` B ) = ( N ` B ) ) -> E. a e. ( ~P V i^i Fin ) ( N ` a ) = ( N ` B ) )
13 9 10 12 sylancl 
 |-  ( ( W e. LMod /\ B C_ V /\ B e. Fin ) -> E. a e. ( ~P V i^i Fin ) ( N ` a ) = ( N ` B ) )
14 simp1 
 |-  ( ( W e. LMod /\ B C_ V /\ B e. Fin ) -> W e. LMod )
15 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
16 2 15 1 lspcl 
 |-  ( ( W e. LMod /\ B C_ V ) -> ( N ` B ) e. ( LSubSp ` W ) )
17 16 3adant3 
 |-  ( ( W e. LMod /\ B C_ V /\ B e. Fin ) -> ( N ` B ) e. ( LSubSp ` W ) )
18 3 15 1 2 islssfg2 
 |-  ( ( W e. LMod /\ ( N ` B ) e. ( LSubSp ` W ) ) -> ( X e. LFinGen <-> E. a e. ( ~P V i^i Fin ) ( N ` a ) = ( N ` B ) ) )
19 14 17 18 syl2anc 
 |-  ( ( W e. LMod /\ B C_ V /\ B e. Fin ) -> ( X e. LFinGen <-> E. a e. ( ~P V i^i Fin ) ( N ` a ) = ( N ` B ) ) )
20 13 19 mpbird 
 |-  ( ( W e. LMod /\ B C_ V /\ B e. Fin ) -> X e. LFinGen )