Theorem islssfgi

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

	Ref	Expression
Hypotheses	islssfgi.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	islssfgi.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	islssfgi.x	⊢ 𝑋 = ( 𝑊 ↾s ( 𝑁 ‘ 𝐵 ) )
Assertion	islssfgi	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ⊆ 𝑉 ∧ 𝐵 ∈ Fin ) → 𝑋 ∈ LFinGen )

Proof

Step	Hyp	Ref	Expression
1		islssfgi.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
2		islssfgi.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
3		islssfgi.x	⊢ 𝑋 = ( 𝑊 ↾s ( 𝑁 ‘ 𝐵 ) )
4	2	fvexi	⊢ 𝑉 ∈ V
5	4	elpw2	⊢ ( 𝐵 ∈ 𝒫 𝑉 ↔ 𝐵 ⊆ 𝑉 )
6	5	biimpri	⊢ ( 𝐵 ⊆ 𝑉 → 𝐵 ∈ 𝒫 𝑉 )
7	6	3ad2ant2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ⊆ 𝑉 ∧ 𝐵 ∈ Fin ) → 𝐵 ∈ 𝒫 𝑉 )
8		simp3	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ⊆ 𝑉 ∧ 𝐵 ∈ Fin ) → 𝐵 ∈ Fin )
9	7 8	elind	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ⊆ 𝑉 ∧ 𝐵 ∈ Fin ) → 𝐵 ∈ ( 𝒫 𝑉 ∩ Fin ) )
10		eqid	⊢ ( 𝑁 ‘ 𝐵 ) = ( 𝑁 ‘ 𝐵 )
11		fveqeq2	⊢ ( 𝑎 = 𝐵 → ( ( 𝑁 ‘ 𝑎 ) = ( 𝑁 ‘ 𝐵 ) ↔ ( 𝑁 ‘ 𝐵 ) = ( 𝑁 ‘ 𝐵 ) ) )
12	11	rspcev	⊢ ( ( 𝐵 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ( 𝑁 ‘ 𝐵 ) = ( 𝑁 ‘ 𝐵 ) ) → ∃ 𝑎 ∈ ( 𝒫 𝑉 ∩ Fin ) ( 𝑁 ‘ 𝑎 ) = ( 𝑁 ‘ 𝐵 ) )
13	9 10 12	sylancl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ⊆ 𝑉 ∧ 𝐵 ∈ Fin ) → ∃ 𝑎 ∈ ( 𝒫 𝑉 ∩ Fin ) ( 𝑁 ‘ 𝑎 ) = ( 𝑁 ‘ 𝐵 ) )
14		simp1	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ⊆ 𝑉 ∧ 𝐵 ∈ Fin ) → 𝑊 ∈ LMod )
15		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
16	2 15 1	lspcl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝐵 ) ∈ ( LSubSp ‘ 𝑊 ) )
17	16	3adant3	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ⊆ 𝑉 ∧ 𝐵 ∈ Fin ) → ( 𝑁 ‘ 𝐵 ) ∈ ( LSubSp ‘ 𝑊 ) )
18	3 15 1 2	islssfg2	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝐵 ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑋 ∈ LFinGen ↔ ∃ 𝑎 ∈ ( 𝒫 𝑉 ∩ Fin ) ( 𝑁 ‘ 𝑎 ) = ( 𝑁 ‘ 𝐵 ) ) )
19	14 17 18	syl2anc	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ⊆ 𝑉 ∧ 𝐵 ∈ Fin ) → ( 𝑋 ∈ LFinGen ↔ ∃ 𝑎 ∈ ( 𝒫 𝑉 ∩ Fin ) ( 𝑁 ‘ 𝑎 ) = ( 𝑁 ‘ 𝐵 ) ) )
20	13 19	mpbird	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ⊆ 𝑉 ∧ 𝐵 ∈ Fin ) → 𝑋 ∈ LFinGen )