lspid

Description: The span of a subspace is itself. ( spanid analog.) (Contributed by NM, 15-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Step	Hyp	Ref	Expression
1		lspid.s	$⊢ S = LSubSp (W)$
2		lspid.n	$⊢ N = LSpan (W)$
3		eqid	$⊢ {Base}_{W} = {Base}_{W}$
4	3 1	lssss	$⊢ U \in S \to U \subseteq {Base}_{W}$
5	3 1 2	lspval	$⊢ (W \in LMod \land U \subseteq {Base}_{W}) \to N (U) = ⋂ \{t \in S \| U \subseteq t\}$
6	4 5	sylan2	$⊢ (W \in LMod \land U \in S) \to N (U) = ⋂ \{t \in S \| U \subseteq t\}$
7		intmin	$⊢ U \in S \to ⋂ \{t \in S \| U \subseteq t\} = U$
8	7	adantl	$⊢ (W \in LMod \land U \in S) \to ⋂ \{t \in S \| U \subseteq t\} = U$
9	6 8	eqtrd	$⊢ (W \in LMod \land U \in S) \to N (U) = U$

Metamath Proof Explorer