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	1	fvexi	$⊢ V \in V$
12	11	elpw2	$⊢ U \in 𝒫 V \leftrightarrow U \subseteq V$
13	12	bilanri	$⊢ (W \in LMod \land U \subseteq V) \to U \in 𝒫 V$
14	1 2	lss1	$⊢ W \in LMod \to V \in S$
15		sseq2	$⊢ t = V \to (U \subseteq t \leftrightarrow U \subseteq V)$
16	15	rspcev	$⊢ (V \in S \land U \subseteq V) \to \exists t \in S U \subseteq t$
17	14 16	sylan	$⊢ (W \in LMod \land U \subseteq V) \to \exists t \in S U \subseteq t$
18		intexrab	$⊢ \exists t \in S U \subseteq t \leftrightarrow ⋂ \{t \in S \| U \subseteq t\} \in V$
19	17 18	sylib	$⊢ (W \in LMod \land U \subseteq V) \to ⋂ \{t \in S \| U \subseteq t\} \in V$
20	7 10 13 19	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\}$
21	6 20	eqtrd	$⊢ (W \in LMod \land U \subseteq V) \to N (U) = ⋂ \{t \in S \| U \subseteq t\}$

Metamath Proof Explorer

Theorem lspval

Proof