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=BaseW
islmodfg.n ⊢N=LSpan⁡W
Assertion islmodfg ⊢W∈LMod→W∈LFinGen↔∃b∈𝒫Bb∈Fin∧N⁡b=B

Proof

Step Hyp Ref Expression
1 islmodfg.b ⊢B=BaseW
2 islmodfg.n ⊢N=LSpan⁡W
3 df-lfig ⊢LFinGen=a∈LMod|Basea∈LSpan⁡a𝒫Basea∩Fin
4 3 eleq2i ⊢W∈LFinGen↔W∈a∈LMod|Basea∈LSpan⁡a𝒫Basea∩Fin
5 fveq2 ⊢a=W→Basea=BaseW
6 fveq2 ⊢a=W→LSpan⁡a=LSpan⁡W
7 6 2 eqtr4di ⊢a=W→LSpan⁡a=N
8 5 pweqd ⊢a=W→𝒫Basea=𝒫BaseW
9 8 ineq1d ⊢a=W→𝒫Basea∩Fin=𝒫BaseW∩Fin
10 7 9 imaeq12d ⊢a=W→LSpan⁡a𝒫Basea∩Fin=N𝒫BaseW∩Fin
11 5 10 eleq12d ⊢a=W→Basea∈LSpan⁡a𝒫Basea∩Fin↔BaseW∈N𝒫BaseW∩Fin
12 11 elrab3 ⊢W∈LMod→W∈a∈LMod|Basea∈LSpan⁡a𝒫Basea∩Fin↔BaseW∈N𝒫BaseW∩Fin
13 4 12 bitrid ⊢W∈LMod→W∈LFinGen↔BaseW∈N𝒫BaseW∩Fin
14 eqid ⊢BaseW=BaseW
15 eqid ⊢LSubSp⁡W=LSubSp⁡W
16 14 15 2 lspf ⊢W∈LMod→N:𝒫BaseW⟶LSubSp⁡W
17 16 ffnd ⊢W∈LMod→NFn𝒫BaseW
18 inss1 ⊢𝒫BaseW∩Fin⊆𝒫BaseW
19 fvelimab ⊢NFn𝒫BaseW∧𝒫BaseW∩Fin⊆𝒫BaseW→BaseW∈N𝒫BaseW∩Fin↔∃b∈𝒫BaseW∩FinN⁡b=BaseW
20 17 18 19 sylancl ⊢W∈LMod→BaseW∈N𝒫BaseW∩Fin↔∃b∈𝒫BaseW∩FinN⁡b=BaseW
21 elin ⊢b∈𝒫BaseW∩Fin↔b∈𝒫BaseW∧b∈Fin
22 1 eqcomi ⊢BaseW=B
23 22 pweqi ⊢𝒫BaseW=𝒫B
24 23 eleq2i ⊢b∈𝒫BaseW↔b∈𝒫B
25 24 anbi1i ⊢b∈𝒫BaseW∧b∈Fin↔b∈𝒫B∧b∈Fin
26 21 25 bitri ⊢b∈𝒫BaseW∩Fin↔b∈𝒫B∧b∈Fin
27 22 eqeq2i ⊢N⁡b=BaseW↔N⁡b=B
28 26 27 anbi12i ⊢b∈𝒫BaseW∩Fin∧N⁡b=BaseW↔b∈𝒫B∧b∈Fin∧N⁡b=B
29 anass ⊢b∈𝒫B∧b∈Fin∧N⁡b=B↔b∈𝒫B∧b∈Fin∧N⁡b=B
30 28 29 bitri ⊢b∈𝒫BaseW∩Fin∧N⁡b=BaseW↔b∈𝒫B∧b∈Fin∧N⁡b=B
31 30 rexbii2 ⊢∃b∈𝒫BaseW∩FinN⁡b=BaseW↔∃b∈𝒫Bb∈Fin∧N⁡b=B
32 20 31 bitrdi ⊢W∈LMod→BaseW∈N𝒫BaseW∩Fin↔∃b∈𝒫Bb∈Fin∧N⁡b=B
33 13 32 bitrd ⊢W∈LMod→W∈LFinGen↔∃b∈𝒫Bb∈Fin∧N⁡b=B