lspf

Description: The span function on a left module maps subsets to subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014)

Step	Hyp	Ref	Expression
1		lspval.v	$⊢ V = {Base}_{W}$
2		lspval.s	$⊢ S = LSubSp (W)$
3		lspval.n	$⊢ N = LSpan (W)$
4	1 2 3	lspfval	$⊢ W \in LMod \to N = (s \in 𝒫 V ⟼ ⋂ \{p \in S \| s \subseteq p\})$
5		simpl	$⊢ (W \in LMod \land s \in 𝒫 V) \to W \in LMod$
6		ssrab2	$⊢ \{p \in S \| s \subseteq p\} \subseteq S$
7	6	a1i	$⊢ (W \in LMod \land s \in 𝒫 V) \to \{p \in S \| s \subseteq p\} \subseteq S$
8	1 2	lss1	$⊢ W \in LMod \to V \in S$
9		elpwi	$⊢ s \in 𝒫 V \to s \subseteq V$
10		sseq2	$⊢ p = V \to (s \subseteq p \leftrightarrow s \subseteq V)$
11	10	rspcev	$⊢ (V \in S \land s \subseteq V) \to \exists p \in S s \subseteq p$
12	8 9 11	syl2an	$⊢ (W \in LMod \land s \in 𝒫 V) \to \exists p \in S s \subseteq p$
13		rabn0	$⊢ \{p \in S \| s \subseteq p\} \neq \emptyset \leftrightarrow \exists p \in S s \subseteq p$
14	12 13	sylibr	$⊢ (W \in LMod \land s \in 𝒫 V) \to \{p \in S \| s \subseteq p\} \neq \emptyset$
15	2	lssintcl	$⊢ (W \in LMod \land \{p \in S \| s \subseteq p\} \subseteq S \land \{p \in S \| s \subseteq p\} \neq \emptyset) \to ⋂ \{p \in S \| s \subseteq p\} \in S$
16	5 7 14 15	syl3anc	$⊢ (W \in LMod \land s \in 𝒫 V) \to ⋂ \{p \in S \| s \subseteq p\} \in S$
17	4 16	fmpt3d	$⊢ W \in LMod \to N : 𝒫 V ⟶ S$

Metamath Proof Explorer