lsp0

Description: Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014)

	Ref	Expression
Hypotheses	lspsn0.z	$⊢ \underset{˙}{0} = 0_{W}$
	lspsn0.n	$⊢ N = LSpan (W)$
Assertion	lsp0	$⊢ W \in LMod \to N (\emptyset) = \{\underset{˙}{0}\}$

Step	Hyp	Ref	Expression
1		lspsn0.z	$⊢ \underset{˙}{0} = 0_{W}$
2		lspsn0.n	$⊢ N = LSpan (W)$
3		eqid	$⊢ LSubSp (W) = LSubSp (W)$
4	1 3	lsssn0	$⊢ W \in LMod \to \{\underset{˙}{0}\} \in LSubSp (W)$
5		0ss	$⊢ \emptyset \subseteq \{\underset{˙}{0}\}$
6	3 2	lspssp	$⊢ (W \in LMod \land \{\underset{˙}{0}\} \in LSubSp (W) \land \emptyset \subseteq \{\underset{˙}{0}\}) \to N (\emptyset) \subseteq \{\underset{˙}{0}\}$
7	5 6	mp3an3	$⊢ (W \in LMod \land \{\underset{˙}{0}\} \in LSubSp (W)) \to N (\emptyset) \subseteq \{\underset{˙}{0}\}$
8	4 7	mpdan	$⊢ W \in LMod \to N (\emptyset) \subseteq \{\underset{˙}{0}\}$
9		0ss	$⊢ \emptyset \subseteq {Base}_{W}$
10		eqid	$⊢ {Base}_{W} = {Base}_{W}$
11	10 3 2	lspcl	$⊢ (W \in LMod \land \emptyset \subseteq {Base}_{W}) \to N (\emptyset) \in LSubSp (W)$
12	9 11	mpan2	$⊢ W \in LMod \to N (\emptyset) \in LSubSp (W)$
13	1 3	lss0ss	$⊢ (W \in LMod \land N (\emptyset) \in LSubSp (W)) \to \{\underset{˙}{0}\} \subseteq N (\emptyset)$
14	12 13	mpdan	$⊢ W \in LMod \to \{\underset{˙}{0}\} \subseteq N (\emptyset)$
15	8 14	eqssd	$⊢ W \in LMod \to N (\emptyset) = \{\underset{˙}{0}\}$

Metamath Proof Explorer