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 ↾ 𝑠 U
islssfg.s ⊢ S = LSubSp ⁡ W
islssfg.n ⊢ N = LSpan ⁡ W
Assertion islssfg ⊢ W ∈ LMod ∧ U ∈ S → X ∈ LFinGen ↔ ∃ b ∈ 𝒫 U b ∈ Fin ∧ N ⁡ b = U

Proof

Step Hyp Ref Expression
1 islssfg.x ⊢ X = W ↾ 𝑠 U
2 islssfg.s ⊢ S = LSubSp ⁡ W
3 islssfg.n ⊢ N = LSpan ⁡ W
4 eqid ⊢ Base W = Base W
5 4 2 lssss ⊢ U ∈ S → U ⊆ Base W
6 1 4 ressbas2 ⊢ U ⊆ Base W → U = Base X
7 5 6 syl ⊢ U ∈ S → U = Base X
8 7 pweqd ⊢ U ∈ S → 𝒫 U = 𝒫 Base X
9 8 rexeqdv ⊢ U ∈ S → ∃ b ∈ 𝒫 U b ∈ Fin ∧ LSpan ⁡ X ⁡ b = Base X ↔ ∃ b ∈ 𝒫 Base X b ∈ Fin ∧ LSpan ⁡ X ⁡ b = Base X
10 9 adantl ⊢ W ∈ LMod ∧ U ∈ S → ∃ b ∈ 𝒫 U b ∈ Fin ∧ LSpan ⁡ X ⁡ b = Base X ↔ ∃ b ∈ 𝒫 Base X b ∈ Fin ∧ LSpan ⁡ X ⁡ b = Base X
11 elpwi ⊢ b ∈ 𝒫 U → b ⊆ U
12 eqid ⊢ LSpan ⁡ X = LSpan ⁡ X
13 1 3 12 2 lsslsp ⊢ W ∈ LMod ∧ U ∈ S ∧ b ⊆ U → N ⁡ b = LSpan ⁡ X ⁡ b
14 13 3expa ⊢ W ∈ LMod ∧ U ∈ S ∧ b ⊆ U → N ⁡ b = LSpan ⁡ X ⁡ b
15 11 14 sylan2 ⊢ W ∈ LMod ∧ U ∈ S ∧ b ∈ 𝒫 U → N ⁡ b = LSpan ⁡ X ⁡ b
16 7 ad2antlr ⊢ W ∈ LMod ∧ U ∈ S ∧ b ∈ 𝒫 U → U = Base X
17 15 16 eqeq12d ⊢ W ∈ LMod ∧ U ∈ S ∧ b ∈ 𝒫 U → N ⁡ b = U ↔ LSpan ⁡ X ⁡ b = Base X
18 17 anbi2d ⊢ W ∈ LMod ∧ U ∈ S ∧ b ∈ 𝒫 U → b ∈ Fin ∧ N ⁡ b = U ↔ b ∈ Fin ∧ LSpan ⁡ X ⁡ b = Base X
19 18 rexbidva ⊢ W ∈ LMod ∧ U ∈ S → ∃ b ∈ 𝒫 U b ∈ Fin ∧ N ⁡ b = U ↔ ∃ b ∈ 𝒫 U b ∈ Fin ∧ LSpan ⁡ X ⁡ b = Base X
20 1 2 lsslmod ⊢ W ∈ LMod ∧ U ∈ S → X ∈ LMod
21 eqid ⊢ Base X = Base X
22 21 12 islmodfg ⊢ X ∈ LMod → X ∈ LFinGen ↔ ∃ b ∈ 𝒫 Base X b ∈ Fin ∧ LSpan ⁡ X ⁡ b = Base X
23 20 22 syl ⊢ W ∈ LMod ∧ U ∈ S → X ∈ LFinGen ↔ ∃ b ∈ 𝒫 Base X b ∈ Fin ∧ LSpan ⁡ X ⁡ b = Base X
24 10 19 23 3bitr4rd ⊢ W ∈ LMod ∧ U ∈ S → X ∈ LFinGen ↔ ∃ b ∈ 𝒫 U b ∈ Fin ∧ N ⁡ b = U