lsatssn0

Description: A subspace (or any class) including an atom is nonzero. (Contributed by NM, 3-Feb-2015)

Step	Hyp	Ref	Expression
1		lsatssn0.o	$⊢ \underset{˙}{0} = 0_{W}$
2		lsatssn0.a	$⊢ A = LSAtoms (W)$
3		lsatssn0.w	$⊢ φ \to W \in LMod$
4		lsatssn0.q	$⊢ φ \to Q \in A$
5		lsatssn0.u	$⊢ φ \to Q \subseteq U$
6		eqid	$⊢ LSubSp (W) = LSubSp (W)$
7	6 2 3 4	lsatlssel	$⊢ φ \to Q \in LSubSp (W)$
8	1 6	lss0ss	$⊢ (W \in LMod \land Q \in LSubSp (W)) \to \{\underset{˙}{0}\} \subseteq Q$
9	3 7 8	syl2anc	$⊢ φ \to \{\underset{˙}{0}\} \subseteq Q$
10	1 2 3 4	lsatn0	$⊢ φ \to Q \neq \{\underset{˙}{0}\}$
11	10	necomd	$⊢ φ \to \{\underset{˙}{0}\} \neq Q$
12		df-pss	$⊢ \{\underset{˙}{0}\} \subset Q \leftrightarrow (\{\underset{˙}{0}\} \subseteq Q \land \{\underset{˙}{0}\} \neq Q)$
13	9 11 12	sylanbrc	$⊢ φ \to \{\underset{˙}{0}\} \subset Q$
14	13 5	psssstrd	$⊢ φ \to \{\underset{˙}{0}\} \subset U$
15	14	pssned	$⊢ φ \to \{\underset{˙}{0}\} \neq U$
16	15	necomd	$⊢ φ \to U \neq \{\underset{˙}{0}\}$

Metamath Proof Explorer