Metamath Proof Explorer

Theorem lspfval

Description: The span function for a left vector space (or a left module). ( df-span analog.) (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

		Ref	Expression
	Hypotheses	lspval.v	$⊢ V = {Base}_{W}$
		lspval.s	$⊢ S = LSubSp (W)$
		lspval.n	$⊢ N = LSpan (W)$
	Assertion	lspfval	$⊢ W \in X \to N = (s \in 𝒫 V ⟼ ⋂ \{t \in S \| s \subseteq t\})$

Proof

Step	Hyp	Ref	Expression
1		lspval.v	$⊢ V = {Base}_{W}$
2		lspval.s	$⊢ S = LSubSp (W)$
3		lspval.n	$⊢ N = LSpan (W)$
4		elex	$⊢ W \in X \to W \in V$
5		fveq2	$⊢ w = W \to {Base}_{w} = {Base}_{W}$
6	5 1	eqtr4di	$⊢ w = W \to {Base}_{w} = V$
7	6	pweqd	$⊢ w = W \to 𝒫 {Base}_{w} = 𝒫 V$
8		fveq2	$⊢ w = W \to LSubSp (w) = LSubSp (W)$
9	8 2	eqtr4di	$⊢ w = W \to LSubSp (w) = S$
10	9	rabeqdv	$⊢ w = W \to \{t \in LSubSp (w) \| s \subseteq t\} = \{t \in S \| s \subseteq t\}$
11	10	inteqd	$⊢ w = W \to ⋂ \{t \in LSubSp (w) \| s \subseteq t\} = ⋂ \{t \in S \| s \subseteq t\}$
12	7 11	mpteq12dv	$⊢ w = W \to (s \in 𝒫 {Base}_{w} ⟼ ⋂ \{t \in LSubSp (w) \| s \subseteq t\}) = (s \in 𝒫 V ⟼ ⋂ \{t \in S \| s \subseteq t\})$
13		df-lsp	$⊢ LSpan = (w \in V ⟼ (s \in 𝒫 {Base}_{w} ⟼ ⋂ \{t \in LSubSp (w) \| s \subseteq t\}))$
14	1	fvexi	$⊢ V \in V$
15	14	pwex	$⊢ 𝒫 V \in V$
16	15	mptex	$⊢ (s \in 𝒫 V ⟼ ⋂ \{t \in S \| s \subseteq t\}) \in V$
17	12 13 16	fvmpt	$⊢ W \in V \to LSpan (W) = (s \in 𝒫 V ⟼ ⋂ \{t \in S \| s \subseteq t\})$
18	4 17	syl	$⊢ W \in X \to LSpan (W) = (s \in 𝒫 V ⟼ ⋂ \{t \in S \| s \subseteq t\})$
19	3 18	syl5eq	$⊢ W \in X \to N = (s \in 𝒫 V ⟼ ⋂ \{t \in S \| s \subseteq t\})$