Metamath Proof Explorer

Theorem islmodfg

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

Ref Expression
Hypotheses islmodfg.b 
|- B = ( Base ` W )
islmodfg.n 
|- N = ( LSpan ` W )
Assertion islmodfg 
|- ( W e. LMod -> ( W e. LFinGen <-> E. b e. ~P B ( b e. Fin /\ ( N ` b ) = B ) ) )

Proof

Step Hyp Ref Expression
1 islmodfg.b 
 |-  B = ( Base ` W )
2 islmodfg.n 
 |-  N = ( LSpan ` W )
3 df-lfig 
 |-  LFinGen = { a e. LMod | ( Base ` a ) e. ( ( LSpan ` a ) " ( ~P ( Base ` a ) i^i Fin ) ) }
4 3 eleq2i 
 |-  ( W e. LFinGen <-> W e. { a e. LMod | ( Base ` a ) e. ( ( LSpan ` a ) " ( ~P ( Base ` a ) i^i Fin ) ) } )
5 fveq2 
 |-  ( a = W -> ( Base ` a ) = ( Base ` W ) )
6 fveq2 
 |-  ( a = W -> ( LSpan ` a ) = ( LSpan ` W ) )
7 6 2 eqtr4di 
 |-  ( a = W -> ( LSpan ` a ) = N )
8 5 pweqd 
 |-  ( a = W -> ~P ( Base ` a ) = ~P ( Base ` W ) )
9 8 ineq1d 
 |-  ( a = W -> ( ~P ( Base ` a ) i^i Fin ) = ( ~P ( Base ` W ) i^i Fin ) )
10 7 9 imaeq12d 
 |-  ( a = W -> ( ( LSpan ` a ) " ( ~P ( Base ` a ) i^i Fin ) ) = ( N " ( ~P ( Base ` W ) i^i Fin ) ) )
11 5 10 eleq12d 
 |-  ( a = W -> ( ( Base ` a ) e. ( ( LSpan ` a ) " ( ~P ( Base ` a ) i^i Fin ) ) <-> ( Base ` W ) e. ( N " ( ~P ( Base ` W ) i^i Fin ) ) ) )
12 11 elrab3 
 |-  ( W e. LMod -> ( W e. { a e. LMod | ( Base ` a ) e. ( ( LSpan ` a ) " ( ~P ( Base ` a ) i^i Fin ) ) } <-> ( Base ` W ) e. ( N " ( ~P ( Base ` W ) i^i Fin ) ) ) )
13 4 12 syl5bb 
 |-  ( W e. LMod -> ( W e. LFinGen <-> ( Base ` W ) e. ( N " ( ~P ( Base ` W ) i^i Fin ) ) ) )
14 eqid 
 |-  ( Base ` W ) = ( Base ` W )
15 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
16 14 15 2 lspf 
 |-  ( W e. LMod -> N : ~P ( Base ` W ) --> ( LSubSp ` W ) )
17 16 ffnd 
 |-  ( W e. LMod -> N Fn ~P ( Base ` W ) )
18 inss1 
 |-  ( ~P ( Base ` W ) i^i Fin ) C_ ~P ( Base ` W )
19 fvelimab 
 |-  ( ( N Fn ~P ( Base ` W ) /\ ( ~P ( Base ` W ) i^i Fin ) C_ ~P ( Base ` W ) ) -> ( ( Base ` W ) e. ( N " ( ~P ( Base ` W ) i^i Fin ) ) <-> E. b e. ( ~P ( Base ` W ) i^i Fin ) ( N ` b ) = ( Base ` W ) ) )
20 17 18 19 sylancl 
 |-  ( W e. LMod -> ( ( Base ` W ) e. ( N " ( ~P ( Base ` W ) i^i Fin ) ) <-> E. b e. ( ~P ( Base ` W ) i^i Fin ) ( N ` b ) = ( Base ` W ) ) )
21 elin 
 |-  ( b e. ( ~P ( Base ` W ) i^i Fin ) <-> ( b e. ~P ( Base ` W ) /\ b e. Fin ) )
22 1 eqcomi 
 |-  ( Base ` W ) = B
23 22 pweqi 
 |-  ~P ( Base ` W ) = ~P B
24 23 eleq2i 
 |-  ( b e. ~P ( Base ` W ) <-> b e. ~P B )
25 24 anbi1i 
 |-  ( ( b e. ~P ( Base ` W ) /\ b e. Fin ) <-> ( b e. ~P B /\ b e. Fin ) )
26 21 25 bitri 
 |-  ( b e. ( ~P ( Base ` W ) i^i Fin ) <-> ( b e. ~P B /\ b e. Fin ) )
27 22 eqeq2i 
 |-  ( ( N ` b ) = ( Base ` W ) <-> ( N ` b ) = B )
28 26 27 anbi12i 
 |-  ( ( b e. ( ~P ( Base ` W ) i^i Fin ) /\ ( N ` b ) = ( Base ` W ) ) <-> ( ( b e. ~P B /\ b e. Fin ) /\ ( N ` b ) = B ) )
29 anass 
 |-  ( ( ( b e. ~P B /\ b e. Fin ) /\ ( N ` b ) = B ) <-> ( b e. ~P B /\ ( b e. Fin /\ ( N ` b ) = B ) ) )
30 28 29 bitri 
 |-  ( ( b e. ( ~P ( Base ` W ) i^i Fin ) /\ ( N ` b ) = ( Base ` W ) ) <-> ( b e. ~P B /\ ( b e. Fin /\ ( N ` b ) = B ) ) )
31 30 rexbii2 
 |-  ( E. b e. ( ~P ( Base ` W ) i^i Fin ) ( N ` b ) = ( Base ` W ) <-> E. b e. ~P B ( b e. Fin /\ ( N ` b ) = B ) )
32 20 31 bitrdi 
 |-  ( W e. LMod -> ( ( Base ` W ) e. ( N " ( ~P ( Base ` W ) i^i Fin ) ) <-> E. b e. ~P B ( b e. Fin /\ ( N ` b ) = B ) ) )
33 13 32 bitrd 
 |-  ( W e. LMod -> ( W e. LFinGen <-> E. b e. ~P B ( b e. Fin /\ ( N ` b ) = B ) ) )