Metamath Proof Explorer

Theorem lsatlspsn2

Description: The span of a nonzero singleton is an atom. TODO: make this obsolete and use lsatlspsn instead? (Contributed by NM, 9-Apr-2014) (Revised by Mario Carneiro, 24-Jun-2014)

		Ref	Expression
	Hypotheses	lsatset.v	$⊢ V = {Base}_{W}$
		lsatset.n	$⊢ N = LSpan (W)$
		lsatset.z	$⊢ \underset{˙}{0} = 0_{W}$
		lsatset.a	$⊢ A = LSAtoms (W)$
	Assertion	lsatlspsn2	$⊢ (W \in LMod \land X \in V \land X \neq \underset{˙}{0}) \to N (\{X\}) \in A$

Proof

Step	Hyp	Ref	Expression
1		lsatset.v	$⊢ V = {Base}_{W}$
2		lsatset.n	$⊢ N = LSpan (W)$
3		lsatset.z	$⊢ \underset{˙}{0} = 0_{W}$
4		lsatset.a	$⊢ A = LSAtoms (W)$
5		3simpc	$⊢ (W \in LMod \land X \in V \land X \neq \underset{˙}{0}) \to (X \in V \land X \neq \underset{˙}{0})$
6		eldifsn	$⊢ X \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (X \in V \land X \neq \underset{˙}{0})$
7	5 6	sylibr	$⊢ (W \in LMod \land X \in V \land X \neq \underset{˙}{0}) \to X \in (V ∖ \{\underset{˙}{0}\})$
8		eqid	$⊢ N (\{X\}) = N (\{X\})$
9		sneq	$⊢ v = X \to \{v\} = \{X\}$
10	9	fveq2d	$⊢ v = X \to N (\{v\}) = N (\{X\})$
11	10	rspceeqv	$⊢ (X \in (V ∖ \{\underset{˙}{0}\}) \land N (\{X\}) = N (\{X\})) \to \exists v \in (V ∖ \{\underset{˙}{0}\}) N (\{X\}) = N (\{v\})$
12	7 8 11	sylancl	$⊢ (W \in LMod \land X \in V \land X \neq \underset{˙}{0}) \to \exists v \in (V ∖ \{\underset{˙}{0}\}) N (\{X\}) = N (\{v\})$
13	1 2 3 4	islsat	$⊢ W \in LMod \to (N (\{X\}) \in A \leftrightarrow \exists v \in (V ∖ \{\underset{˙}{0}\}) N (\{X\}) = N (\{v\}))$
14	13	3ad2ant1	$⊢ (W \in LMod \land X \in V \land X \neq \underset{˙}{0}) \to (N (\{X\}) \in A \leftrightarrow \exists v \in (V ∖ \{\underset{˙}{0}\}) N (\{X\}) = N (\{v\}))$
15	12 14	mpbird	$⊢ (W \in LMod \land X \in V \land X \neq \underset{˙}{0}) \to N (\{X\}) \in A$