lspval

Description: The span of a set of vectors (in a left module). ( spanval 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	lspval	$⊢ (W \in LMod \land U \subseteq V) \to N (U) = ⋂ \{t \in S \| U \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	1 2 3	lspfval	$⊢ W \in LMod \to N = (s \in 𝒫 V ⟼ ⋂ \{t \in S \| s \subseteq t\})$
5	4	fveq1d	$⊢ W \in LMod \to N (U) = (s \in 𝒫 V ⟼ ⋂ \{t \in S \| s \subseteq t\}) (U)$
6	5	adantr	$⊢ (W \in LMod \land U \subseteq V) \to N (U) = (s \in 𝒫 V ⟼ ⋂ \{t \in S \| s \subseteq t\}) (U)$
7		eqid	$⊢ (s \in 𝒫 V ⟼ ⋂ \{t \in S \| s \subseteq t\}) = (s \in 𝒫 V ⟼ ⋂ \{t \in S \| s \subseteq t\})$
8		sseq1	$⊢ s = U \to (s \subseteq t \leftrightarrow U \subseteq t)$
9	8	rabbidv	$⊢ s = U \to \{t \in S \| s \subseteq t\} = \{t \in S \| U \subseteq t\}$
10	9	inteqd	$⊢ s = U \to ⋂ \{t \in S \| s \subseteq t\} = ⋂ \{t \in S \| U \subseteq t\}$
11		simpr	$⊢ (W \in LMod \land U \subseteq V) \to U \subseteq V$
12	1	fvexi	$⊢ V \in V$
13	12	elpw2	$⊢ U \in 𝒫 V \leftrightarrow U \subseteq V$
14	11 13	sylibr	$⊢ (W \in LMod \land U \subseteq V) \to U \in 𝒫 V$
15	1 2	lss1	$⊢ W \in LMod \to V \in S$
16		sseq2	$⊢ t = V \to (U \subseteq t \leftrightarrow U \subseteq V)$
17	16	rspcev	$⊢ (V \in S \land U \subseteq V) \to \exists t \in S U \subseteq t$
18	15 17	sylan	$⊢ (W \in LMod \land U \subseteq V) \to \exists t \in S U \subseteq t$
19		intexrab	$⊢ \exists t \in S U \subseteq t \leftrightarrow ⋂ \{t \in S \| U \subseteq t\} \in V$
20	18 19	sylib	$⊢ (W \in LMod \land U \subseteq V) \to ⋂ \{t \in S \| U \subseteq t\} \in V$
21	7 10 14 20	fvmptd3	$⊢ (W \in LMod \land U \subseteq V) \to (s \in 𝒫 V ⟼ ⋂ \{t \in S \| s \subseteq t\}) (U) = ⋂ \{t \in S \| U \subseteq t\}$
22	6 21	eqtrd	$⊢ (W \in LMod \land U \subseteq V) \to N (U) = ⋂ \{t \in S \| U \subseteq t\}$

Metamath Proof Explorer

Theorem lspval

Proof