lss0cl

Description: The zero vector belongs to every subspace. (Contributed by NM, 12-Jan-2014) (Proof shortened by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lss0cl.z	$⊢ \underset{˙}{0} = 0_{W}$
	lss0cl.s	$⊢ S = LSubSp (W)$
Assertion	lss0cl	$⊢ (W \in LMod \land U \in S) \to \underset{˙}{0} \in U$

Step	Hyp	Ref	Expression
1		lss0cl.z	$⊢ \underset{˙}{0} = 0_{W}$
2		lss0cl.s	$⊢ S = LSubSp (W)$
3	2	lssn0	$⊢ U \in S \to U \neq \emptyset$
4		n0	$⊢ U \neq \emptyset \leftrightarrow \exists x x \in U$
5	3 4	sylib	$⊢ U \in S \to \exists x x \in U$
6	5	adantl	$⊢ (W \in LMod \land U \in S) \to \exists x x \in U$
7		simp1	$⊢ (W \in LMod \land U \in S \land x \in U) \to W \in LMod$
8		eqid	$⊢ {Base}_{W} = {Base}_{W}$
9	8 2	lssel	$⊢ (U \in S \land x \in U) \to x \in {Base}_{W}$
10	9	3adant1	$⊢ (W \in LMod \land U \in S \land x \in U) \to x \in {Base}_{W}$
11		eqid	$⊢ -_{W} = -_{W}$
12	8 1 11	lmodsubid	$⊢ (W \in LMod \land x \in {Base}_{W}) \to x -_{W} x = \underset{˙}{0}$
13	7 10 12	syl2anc	$⊢ (W \in LMod \land U \in S \land x \in U) \to x -_{W} x = \underset{˙}{0}$
14	11 2	lssvsubcl	$⊢ ((W \in LMod \land U \in S) \land (x \in U \land x \in U)) \to x -_{W} x \in U$
15	14	anabsan2	$⊢ ((W \in LMod \land U \in S) \land x \in U) \to x -_{W} x \in U$
16	15	3impa	$⊢ (W \in LMod \land U \in S \land x \in U) \to x -_{W} x \in U$
17	13 16	eqeltrrd	$⊢ (W \in LMod \land U \in S \land x \in U) \to \underset{˙}{0} \in U$
18	17	3expia	$⊢ (W \in LMod \land U \in S) \to (x \in U \to \underset{˙}{0} \in U)$
19	18	exlimdv	$⊢ (W \in LMod \land U \in S) \to (\exists x x \in U \to \underset{˙}{0} \in U)$
20	6 19	mpd	$⊢ (W \in LMod \land U \in S) \to \underset{˙}{0} \in U$

Metamath Proof Explorer