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 ∈ LMod → W ∈ LFinGen ↔ ∃ b ∈ 𝒫 B b ∈ 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 ∈ LMod | Base a ∈ LSpan ⁡ a 𝒫 Base a ∩ Fin
4 3 eleq2i ⊢ W ∈ LFinGen ↔ W ∈ a ∈ LMod | Base a ∈ LSpan ⁡ a 𝒫 Base a ∩ 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 → 𝒫 Base a = 𝒫 Base W
9 8 ineq1d ⊢ a = W → 𝒫 Base a ∩ Fin = 𝒫 Base W ∩ Fin
10 7 9 imaeq12d ⊢ a = W → LSpan ⁡ a 𝒫 Base a ∩ Fin = N 𝒫 Base W ∩ Fin
11 5 10 eleq12d ⊢ a = W → Base a ∈ LSpan ⁡ a 𝒫 Base a ∩ Fin ↔ Base W ∈ N 𝒫 Base W ∩ Fin
12 11 elrab3 ⊢ W ∈ LMod → W ∈ a ∈ LMod | Base a ∈ LSpan ⁡ a 𝒫 Base a ∩ Fin ↔ Base W ∈ N 𝒫 Base W ∩ Fin
13 4 12 bitrid ⊢ W ∈ LMod → W ∈ LFinGen ↔ Base W ∈ N 𝒫 Base W ∩ Fin
14 eqid ⊢ Base W = Base W
15 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
16 14 15 2 lspf ⊢ W ∈ LMod → N : 𝒫 Base W ⟶ LSubSp ⁡ W
17 16 ffnd ⊢ W ∈ LMod → N Fn 𝒫 Base W
18 inss1 ⊢ 𝒫 Base W ∩ Fin ⊆ 𝒫 Base W
19 fvelimab ⊢ N Fn 𝒫 Base W ∧ 𝒫 Base W ∩ Fin ⊆ 𝒫 Base W → Base W ∈ N 𝒫 Base W ∩ Fin ↔ ∃ b ∈ 𝒫 Base W ∩ Fin N ⁡ b = Base W
20 17 18 19 sylancl ⊢ W ∈ LMod → Base W ∈ N 𝒫 Base W ∩ Fin ↔ ∃ b ∈ 𝒫 Base W ∩ Fin N ⁡ b = Base W
21 elin ⊢ b ∈ 𝒫 Base W ∩ Fin ↔ b ∈ 𝒫 Base W ∧ b ∈ Fin
22 1 eqcomi ⊢ Base W = B
23 22 pweqi ⊢ 𝒫 Base W = 𝒫 B
24 23 eleq2i ⊢ b ∈ 𝒫 Base W ↔ b ∈ 𝒫 B
25 24 anbi1i ⊢ b ∈ 𝒫 Base W ∧ b ∈ Fin ↔ b ∈ 𝒫 B ∧ b ∈ Fin
26 21 25 bitri ⊢ b ∈ 𝒫 Base W ∩ Fin ↔ b ∈ 𝒫 B ∧ b ∈ Fin
27 22 eqeq2i ⊢ N ⁡ b = Base W ↔ N ⁡ b = B
28 26 27 anbi12i ⊢ b ∈ 𝒫 Base W ∩ Fin ∧ N ⁡ b = Base W ↔ 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 ∈ 𝒫 Base W ∩ Fin ∧ N ⁡ b = Base W ↔ b ∈ 𝒫 B ∧ b ∈ Fin ∧ N ⁡ b = B
31 30 rexbii2 ⊢ ∃ b ∈ 𝒫 Base W ∩ Fin N ⁡ b = Base W ↔ ∃ b ∈ 𝒫 B b ∈ Fin ∧ N ⁡ b = B
32 20 31 bitrdi ⊢ W ∈ LMod → Base W ∈ N 𝒫 Base W ∩ Fin ↔ ∃ b ∈ 𝒫 B b ∈ Fin ∧ N ⁡ b = B
33 13 32 bitrd ⊢ W ∈ LMod → W ∈ LFinGen ↔ ∃ b ∈ 𝒫 B b ∈ Fin ∧ N ⁡ b = B