Metamath Proof Explorer

Theorem islssfgi

Description: Finitely spanned subspaces are finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypotheses islssfgi.n ⊢ N = LSpan ⁡ W
islssfgi.v ⊢ V = Base W
islssfgi.x ⊢ X = W ↾ 𝑠 N ⁡ B
Assertion islssfgi ⊢ W ∈ LMod ∧ B ⊆ V ∧ B ∈ Fin → X ∈ LFinGen

Proof

Step Hyp Ref Expression
1 islssfgi.n ⊢ N = LSpan ⁡ W
2 islssfgi.v ⊢ V = Base W
3 islssfgi.x ⊢ X = W ↾ 𝑠 N ⁡ B
4 2 fvexi ⊢ V ∈ V
5 4 elpw2 ⊢ B ∈ 𝒫 V ↔ B ⊆ V
6 5 biimpri ⊢ B ⊆ V → B ∈ 𝒫 V
7 6 3ad2ant2 ⊢ W ∈ LMod ∧ B ⊆ V ∧ B ∈ Fin → B ∈ 𝒫 V
8 simp3 ⊢ W ∈ LMod ∧ B ⊆ V ∧ B ∈ Fin → B ∈ Fin
9 7 8 elind ⊢ W ∈ LMod ∧ B ⊆ V ∧ B ∈ Fin → B ∈ 𝒫 V ∩ Fin
10 eqid ⊢ N ⁡ B = N ⁡ B
11 fveqeq2 ⊢ a = B → N ⁡ a = N ⁡ B ↔ N ⁡ B = N ⁡ B
12 11 rspcev ⊢ B ∈ 𝒫 V ∩ Fin ∧ N ⁡ B = N ⁡ B → ∃ a ∈ 𝒫 V ∩ Fin N ⁡ a = N ⁡ B
13 9 10 12 sylancl ⊢ W ∈ LMod ∧ B ⊆ V ∧ B ∈ Fin → ∃ a ∈ 𝒫 V ∩ Fin N ⁡ a = N ⁡ B
14 simp1 ⊢ W ∈ LMod ∧ B ⊆ V ∧ B ∈ Fin → W ∈ LMod
15 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
16 2 15 1 lspcl ⊢ W ∈ LMod ∧ B ⊆ V → N ⁡ B ∈ LSubSp ⁡ W
17 16 3adant3 ⊢ W ∈ LMod ∧ B ⊆ V ∧ B ∈ Fin → N ⁡ B ∈ LSubSp ⁡ W
18 3 15 1 2 islssfg2 ⊢ W ∈ LMod ∧ N ⁡ B ∈ LSubSp ⁡ W → X ∈ LFinGen ↔ ∃ a ∈ 𝒫 V ∩ Fin N ⁡ a = N ⁡ B
19 14 17 18 syl2anc ⊢ W ∈ LMod ∧ B ⊆ V ∧ B ∈ Fin → X ∈ LFinGen ↔ ∃ a ∈ 𝒫 V ∩ Fin N ⁡ a = N ⁡ B
20 13 19 mpbird ⊢ W ∈ LMod ∧ B ⊆ V ∧ B ∈ Fin → X ∈ LFinGen