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 → LSpan ⁡ X ⁡ b = N ⁡ b
14 13 3expa ⊢ W ∈ LMod ∧ U ∈ S ∧ b ⊆ U → LSpan ⁡ X ⁡ b = N ⁡ b
15 11 14 sylan2 ⊢ W ∈ LMod ∧ U ∈ S ∧ b ∈ 𝒫 U → LSpan ⁡ X ⁡ b = N ⁡ b
16 15 eqcomd ⊢ W ∈ LMod ∧ U ∈ S ∧ b ∈ 𝒫 U → N ⁡ b = LSpan ⁡ X ⁡ b
17 7 ad2antlr ⊢ W ∈ LMod ∧ U ∈ S ∧ b ∈ 𝒫 U → U = Base X
18 16 17 eqeq12d ⊢ W ∈ LMod ∧ U ∈ S ∧ b ∈ 𝒫 U → N ⁡ b = U ↔ LSpan ⁡ X ⁡ b = Base X
19 18 anbi2d ⊢ W ∈ LMod ∧ U ∈ S ∧ b ∈ 𝒫 U → b ∈ Fin ∧ N ⁡ b = U ↔ b ∈ Fin ∧ LSpan ⁡ X ⁡ b = Base X
20 19 rexbidva ⊢ W ∈ LMod ∧ U ∈ S → ∃ b ∈ 𝒫 U b ∈ Fin ∧ N ⁡ b = U ↔ ∃ b ∈ 𝒫 U b ∈ Fin ∧ LSpan ⁡ X ⁡ b = Base X
21 1 2 lsslmod ⊢ W ∈ LMod ∧ U ∈ S → X ∈ LMod
22 eqid ⊢ Base X = Base X
23 22 12 islmodfg ⊢ X ∈ LMod → X ∈ LFinGen ↔ ∃ b ∈ 𝒫 Base X b ∈ Fin ∧ LSpan ⁡ X ⁡ b = Base X
24 21 23 syl ⊢ W ∈ LMod ∧ U ∈ S → X ∈ LFinGen ↔ ∃ b ∈ 𝒫 Base X b ∈ Fin ∧ LSpan ⁡ X ⁡ b = Base X
25 10 20 24 3bitr4rd ⊢ W ∈ LMod ∧ U ∈ S → X ∈ LFinGen ↔ ∃ b ∈ 𝒫 U b ∈ Fin ∧ N ⁡ b = U