lspsncmp

Description: Comparable spans of nonzero singletons are equal. (Contributed by NM, 27-Apr-2015)

	Ref	Expression
Hypotheses	lspsncmp.v	$⊢ V = {Base}_{W}$
	lspsncmp.o	$⊢ \underset{˙}{0} = 0_{W}$
	lspsncmp.n	$⊢ N = LSpan (W)$
	lspsncmp.w	$⊢ φ \to W \in LVec$
	lspsncmp.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	lspsncmp.y	$⊢ φ \to Y \in V$
Assertion	lspsncmp	$⊢ φ \to (N (\{X\}) \subseteq N (\{Y\}) \leftrightarrow N (\{X\}) = N (\{Y\}))$

Step	Hyp	Ref	Expression
1		lspsncmp.v	$⊢ V = {Base}_{W}$
2		lspsncmp.o	$⊢ \underset{˙}{0} = 0_{W}$
3		lspsncmp.n	$⊢ N = LSpan (W)$
4		lspsncmp.w	$⊢ φ \to W \in LVec$
5		lspsncmp.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
6		lspsncmp.y	$⊢ φ \to Y \in V$
7	4	adantr	$⊢ (φ \land N (\{X\}) \subseteq N (\{Y\})) \to W \in LVec$
8	6	adantr	$⊢ (φ \land N (\{X\}) \subseteq N (\{Y\})) \to Y \in V$
9		eqid	$⊢ LSubSp (W) = LSubSp (W)$
10		lveclmod	$⊢ W \in LVec \to W \in LMod$
11	4 10	syl	$⊢ φ \to W \in LMod$
12	1 9 3	lspsncl	$⊢ (W \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (W)$
13	11 6 12	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (W)$
14	5	eldifad	$⊢ φ \to X \in V$
15	1 9 3 11 13 14	ellspsn5b	$⊢ φ \to (X \in N (\{Y\}) \leftrightarrow N (\{X\}) \subseteq N (\{Y\}))$
16	15	biimpar	$⊢ (φ \land N (\{X\}) \subseteq N (\{Y\})) \to X \in N (\{Y\})$
17		eldifsni	$⊢ X \in (V ∖ \{\underset{˙}{0}\}) \to X \neq \underset{˙}{0}$
18	5 17	syl	$⊢ φ \to X \neq \underset{˙}{0}$
19	18	adantr	$⊢ (φ \land N (\{X\}) \subseteq N (\{Y\})) \to X \neq \underset{˙}{0}$
20	1 2 3 7 8 16 19	lspsneleq	$⊢ (φ \land N (\{X\}) \subseteq N (\{Y\})) \to N (\{X\}) = N (\{Y\})$
21	20	ex	$⊢ φ \to (N (\{X\}) \subseteq N (\{Y\}) \to N (\{X\}) = N (\{Y\}))$
22		eqimss	$⊢ N (\{X\}) = N (\{Y\}) \to N (\{X\}) \subseteq N (\{Y\})$
23	21 22	impbid1	$⊢ φ \to (N (\{X\}) \subseteq N (\{Y\}) \leftrightarrow N (\{X\}) = N (\{Y\}))$

Metamath Proof Explorer