Metamath Proof Explorer

Theorem islssfg

Description: Property of a finitely generated left (sub)module. (Contributed by Stefan O'Rear, 1-Jan-2015)

Ref Expression
Hypotheses islssfg.x 
|- X = ( W |`s U )
islssfg.s 
|- S = ( LSubSp ` W )
islssfg.n 
|- N = ( LSpan ` W )
Assertion islssfg 
|- ( ( W e. LMod /\ U e. S ) -> ( X e. LFinGen <-> E. b e. ~P U ( b e. Fin /\ ( N ` b ) = U ) ) )

Proof

Step Hyp Ref Expression
1 islssfg.x 
 |-  X = ( W |`s U )
2 islssfg.s 
 |-  S = ( LSubSp ` W )
3 islssfg.n 
 |-  N = ( LSpan ` W )
4 eqid 
 |-  ( Base ` W ) = ( Base ` W )
5 4 2 lssss 
 |-  ( U e. S -> U C_ ( Base ` W ) )
6 1 4 ressbas2 
 |-  ( U C_ ( Base ` W ) -> U = ( Base ` X ) )
7 5 6 syl 
 |-  ( U e. S -> U = ( Base ` X ) )
8 7 pweqd 
 |-  ( U e. S -> ~P U = ~P ( Base ` X ) )
9 8 rexeqdv 
 |-  ( U e. S -> ( E. b e. ~P U ( b e. Fin /\ ( ( LSpan ` X ) ` b ) = ( Base ` X ) ) <-> E. b e. ~P ( Base ` X ) ( b e. Fin /\ ( ( LSpan ` X ) ` b ) = ( Base ` X ) ) ) )
10 9 adantl 
 |-  ( ( W e. LMod /\ U e. S ) -> ( E. b e. ~P U ( b e. Fin /\ ( ( LSpan ` X ) ` b ) = ( Base ` X ) ) <-> E. b e. ~P ( Base ` X ) ( b e. Fin /\ ( ( LSpan ` X ) ` b ) = ( Base ` X ) ) ) )
11 elpwi 
 |-  ( b e. ~P U -> b C_ U )
12 eqid 
 |-  ( LSpan ` X ) = ( LSpan ` X )
13 1 3 12 2 lsslsp 
 |-  ( ( W e. LMod /\ U e. S /\ b C_ U ) -> ( ( LSpan ` X ) ` b ) = ( N ` b ) )
14 13 3expa 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ b C_ U ) -> ( ( LSpan ` X ) ` b ) = ( N ` b ) )
15 11 14 sylan2 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ b e. ~P U ) -> ( ( LSpan ` X ) ` b ) = ( N ` b ) )
16 15 eqcomd 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ b e. ~P U ) -> ( N ` b ) = ( ( LSpan ` X ) ` b ) )
17 7 ad2antlr 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ b e. ~P U ) -> U = ( Base ` X ) )
18 16 17 eqeq12d 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ b e. ~P U ) -> ( ( N ` b ) = U <-> ( ( LSpan ` X ) ` b ) = ( Base ` X ) ) )
19 18 anbi2d 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ b e. ~P U ) -> ( ( b e. Fin /\ ( N ` b ) = U ) <-> ( b e. Fin /\ ( ( LSpan ` X ) ` b ) = ( Base ` X ) ) ) )
20 19 rexbidva 
 |-  ( ( W e. LMod /\ U e. S ) -> ( E. b e. ~P U ( b e. Fin /\ ( N ` b ) = U ) <-> E. b e. ~P U ( b e. Fin /\ ( ( LSpan ` X ) ` b ) = ( Base ` X ) ) ) )
21 1 2 lsslmod 
 |-  ( ( W e. LMod /\ U e. S ) -> X e. LMod )
22 eqid 
 |-  ( Base ` X ) = ( Base ` X )
23 22 12 islmodfg 
 |-  ( X e. LMod -> ( X e. LFinGen <-> E. b e. ~P ( Base ` X ) ( b e. Fin /\ ( ( LSpan ` X ) ` b ) = ( Base ` X ) ) ) )
24 21 23 syl 
 |-  ( ( W e. LMod /\ U e. S ) -> ( X e. LFinGen <-> E. b e. ~P ( Base ` X ) ( b e. Fin /\ ( ( LSpan ` X ) ` b ) = ( Base ` X ) ) ) )
25 10 20 24 3bitr4rd 
 |-  ( ( W e. LMod /\ U e. S ) -> ( X e. LFinGen <-> E. b e. ~P U ( b e. Fin /\ ( N ` b ) = U ) ) )