lssn0

Description: A subspace is not empty. (Contributed by NM, 12-Jan-2014) (Revised by Mario Carneiro, 8-Jan-2015)

		Ref	Expression
	Hypothesis	lssn0.s	$⊢ S = LSubSp (W)$
	Assertion	lssn0	$⊢ U \in S \to U \neq \emptyset$

Step	Hyp	Ref	Expression
1		lssn0.s	$⊢ S = LSubSp (W)$
2		eqid	$⊢ Scalar (W) = Scalar (W)$
3		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
4		eqid	$⊢ {Base}_{W} = {Base}_{W}$
5		eqid	$⊢ +_{W} = +_{W}$
6		eqid	$⊢ \cdot_{W} = \cdot_{W}$
7	2 3 4 5 6 1	islss	$⊢ U \in S \leftrightarrow (U \subseteq {Base}_{W} \land U \neq \emptyset \land \forall x \in {Base}_{Scalar (W)} \forall a \in U \forall b \in U (x \cdot_{W} a) +_{W} b \in U)$
8	7	simp2bi	$⊢ U \in S \to U \neq \emptyset$

Metamath Proof Explorer