lspsneleq

Description: Membership relation that implies equality of spans. ( spansneleq analog.) (Contributed by NM, 4-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		lspsneleq.v	$⊢ V = {Base}_{W}$
2		lspsneleq.o	$⊢ \underset{˙}{0} = 0_{W}$
3		lspsneleq.n	$⊢ N = LSpan (W)$
4		lspsneleq.w	$⊢ φ \to W \in LVec$
5		lspsneleq.x	$⊢ φ \to X \in V$
6		lspsneleq.y	$⊢ φ \to Y \in N (\{X\})$
7		lspsneleq.z	$⊢ φ \to Y \neq \underset{˙}{0}$
8		lveclmod	$⊢ W \in LVec \to W \in LMod$
9	4 8	syl	$⊢ φ \to W \in LMod$
10		eqid	$⊢ Scalar (W) = Scalar (W)$
11		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
12		eqid	$⊢ \cdot_{W} = \cdot_{W}$
13	10 11 1 12 3	ellspsn	$⊢ (W \in LMod \land X \in V) \to (Y \in N (\{X\}) \leftrightarrow \exists k \in {Base}_{Scalar (W)} Y = k \cdot_{W} X)$
14	9 5 13	syl2anc	$⊢ φ \to (Y \in N (\{X\}) \leftrightarrow \exists k \in {Base}_{Scalar (W)} Y = k \cdot_{W} X)$
15		simpr	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land Y = k \cdot_{W} X) \to Y = k \cdot_{W} X$
16	15	sneqd	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land Y = k \cdot_{W} X) \to \{Y\} = \{k \cdot_{W} X\}$
17	16	fveq2d	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land Y = k \cdot_{W} X) \to N (\{Y\}) = N (\{k \cdot_{W} X\})$
18	4	ad2antrr	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land Y = k \cdot_{W} X) \to W \in LVec$
19		simplr	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land Y = k \cdot_{W} X) \to k \in {Base}_{Scalar (W)}$
20	7	ad2antrr	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land Y = k \cdot_{W} X) \to Y \neq \underset{˙}{0}$
21		simplr	$⊢ (((φ \land k \in {Base}_{Scalar (W)}) \land Y = k \cdot_{W} X) \land k = 0_{Scalar (W)}) \to Y = k \cdot_{W} X$
22		simpr	$⊢ (((φ \land k \in {Base}_{Scalar (W)}) \land Y = k \cdot_{W} X) \land k = 0_{Scalar (W)}) \to k = 0_{Scalar (W)}$
23	22	oveq1d	$⊢ (((φ \land k \in {Base}_{Scalar (W)}) \land Y = k \cdot_{W} X) \land k = 0_{Scalar (W)}) \to k \cdot_{W} X = 0_{Scalar (W)} \cdot_{W} X$
24		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
25	1 10 12 24 2	lmod0vs	$⊢ (W \in LMod \land X \in V) \to 0_{Scalar (W)} \cdot_{W} X = \underset{˙}{0}$
26	9 5 25	syl2anc	$⊢ φ \to 0_{Scalar (W)} \cdot_{W} X = \underset{˙}{0}$
27	26	ad3antrrr	$⊢ (((φ \land k \in {Base}_{Scalar (W)}) \land Y = k \cdot_{W} X) \land k = 0_{Scalar (W)}) \to 0_{Scalar (W)} \cdot_{W} X = \underset{˙}{0}$
28	21 23 27	3eqtrd	$⊢ (((φ \land k \in {Base}_{Scalar (W)}) \land Y = k \cdot_{W} X) \land k = 0_{Scalar (W)}) \to Y = \underset{˙}{0}$
29	28	ex	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land Y = k \cdot_{W} X) \to (k = 0_{Scalar (W)} \to Y = \underset{˙}{0})$
30	29	necon3d	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land Y = k \cdot_{W} X) \to (Y \neq \underset{˙}{0} \to k \neq 0_{Scalar (W)})$
31	20 30	mpd	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land Y = k \cdot_{W} X) \to k \neq 0_{Scalar (W)}$
32	5	ad2antrr	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land Y = k \cdot_{W} X) \to X \in V$
33	1 10 12 11 24 3	lspsnvs	$⊢ (W \in LVec \land (k \in {Base}_{Scalar (W)} \land k \neq 0_{Scalar (W)}) \land X \in V) \to N (\{k \cdot_{W} X\}) = N (\{X\})$
34	18 19 31 32 33	syl121anc	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land Y = k \cdot_{W} X) \to N (\{k \cdot_{W} X\}) = N (\{X\})$
35	17 34	eqtrd	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land Y = k \cdot_{W} X) \to N (\{Y\}) = N (\{X\})$
36	35	rexlimdva2	$⊢ φ \to (\exists k \in {Base}_{Scalar (W)} Y = k \cdot_{W} X \to N (\{Y\}) = N (\{X\}))$
37	14 36	sylbid	$⊢ φ \to (Y \in N (\{X\}) \to N (\{Y\}) = N (\{X\}))$
38	6 37	mpd	$⊢ φ \to N (\{Y\}) = N (\{X\})$

Metamath Proof Explorer

Theorem lspsneleq

Proof