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 \in LMod \land B \subseteq V \land B \in Fin) \to X \in LFinGen$

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 \in V$
5	4	elpw2	$⊢ B \in 𝒫 V \leftrightarrow B \subseteq V$
6	5	biimpri	$⊢ B \subseteq V \to B \in 𝒫 V$
7	6	3ad2ant2	$⊢ (W \in LMod \land B \subseteq V \land B \in Fin) \to B \in 𝒫 V$
8		simp3	$⊢ (W \in LMod \land B \subseteq V \land B \in Fin) \to B \in Fin$
9	7 8	elind	$⊢ (W \in LMod \land B \subseteq V \land B \in Fin) \to B \in (𝒫 V \cap Fin)$
10		eqid	$⊢ N (B) = N (B)$
11		fveqeq2	$⊢ a = B \to (N (a) = N (B) \leftrightarrow N (B) = N (B))$
12	11	rspcev	$⊢ (B \in (𝒫 V \cap Fin) \land N (B) = N (B)) \to \exists a \in (𝒫 V \cap Fin) N (a) = N (B)$
13	9 10 12	sylancl	$⊢ (W \in LMod \land B \subseteq V \land B \in Fin) \to \exists a \in (𝒫 V \cap Fin) N (a) = N (B)$
14		simp1	$⊢ (W \in LMod \land B \subseteq V \land B \in Fin) \to W \in LMod$
15		eqid	$⊢ LSubSp (W) = LSubSp (W)$
16	2 15 1	lspcl	$⊢ (W \in LMod \land B \subseteq V) \to N (B) \in LSubSp (W)$
17	16	3adant3	$⊢ (W \in LMod \land B \subseteq V \land B \in Fin) \to N (B) \in LSubSp (W)$
18	3 15 1 2	islssfg2	$⊢ (W \in LMod \land N (B) \in LSubSp (W)) \to (X \in LFinGen \leftrightarrow \exists a \in (𝒫 V \cap Fin) N (a) = N (B))$
19	14 17 18	syl2anc	$⊢ (W \in LMod \land B \subseteq V \land B \in Fin) \to (X \in LFinGen \leftrightarrow \exists a \in (𝒫 V \cap Fin) N (a) = N (B))$
20	13 19	mpbird	$⊢ (W \in LMod \land B \subseteq V \land B \in Fin) \to X \in LFinGen$

Metamath Proof Explorer