mapdindp1

	Ref	Expression
Hypotheses	mapdindp1.v	$⊢ V = {Base}_{W}$
	mapdindp1.p	$⊢ \underset{˙}{+} = +_{W}$
	mapdindp1.o	$⊢ \underset{˙}{0} = 0_{W}$
	mapdindp1.n	$⊢ N = LSpan (W)$
	mapdindp1.w	$⊢ φ \to W \in LVec$
	mapdindp1.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	mapdindp1.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	mapdindp1.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
	mapdindp1.W	$⊢ φ \to w \in (V ∖ \{\underset{˙}{0}\})$
	mapdindp1.e	$⊢ φ \to N (\{Y\}) = N (\{Z\})$
	mapdindp1.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
	mapdindp1.f	$⊢ φ \to \neg w \in N (\{X, Y\})$
Assertion	mapdindp1	$⊢ φ \to N (\{X\}) \neq N (\{Y \underset{˙}{+} Z\})$

Proof

Step	Hyp	Ref	Expression
1		mapdindp1.v	$⊢ V = {Base}_{W}$
2		mapdindp1.p	$⊢ \underset{˙}{+} = +_{W}$
3		mapdindp1.o	$⊢ \underset{˙}{0} = 0_{W}$
4		mapdindp1.n	$⊢ N = LSpan (W)$
5		mapdindp1.w	$⊢ φ \to W \in LVec$
6		mapdindp1.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
7		mapdindp1.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
8		mapdindp1.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
9		mapdindp1.W	$⊢ φ \to w \in (V ∖ \{\underset{˙}{0}\})$
10		mapdindp1.e	$⊢ φ \to N (\{Y\}) = N (\{Z\})$
11		mapdindp1.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
12		mapdindp1.f	$⊢ φ \to \neg w \in N (\{X, Y\})$
13		eldifsni	$⊢ X \in (V ∖ \{\underset{˙}{0}\}) \to X \neq \underset{˙}{0}$
14	6 13	syl	$⊢ φ \to X \neq \underset{˙}{0}$
15		lveclmod	$⊢ W \in LVec \to W \in LMod$
16	5 15	syl	$⊢ φ \to W \in LMod$
17	3 4	lspsn0	$⊢ W \in LMod \to N (\{\underset{˙}{0}\}) = \{\underset{˙}{0}\}$
18	16 17	syl	$⊢ φ \to N (\{\underset{˙}{0}\}) = \{\underset{˙}{0}\}$
19	18	eqeq2d	$⊢ φ \to (N (\{X\}) = N (\{\underset{˙}{0}\}) \leftrightarrow N (\{X\}) = \{\underset{˙}{0}\})$
20	6	eldifad	$⊢ φ \to X \in V$
21	1 3 4	lspsneq0	$⊢ (W \in LMod \land X \in V) \to (N (\{X\}) = \{\underset{˙}{0}\} \leftrightarrow X = \underset{˙}{0})$
22	16 20 21	syl2anc	$⊢ φ \to (N (\{X\}) = \{\underset{˙}{0}\} \leftrightarrow X = \underset{˙}{0})$
23	19 22	bitrd	$⊢ φ \to (N (\{X\}) = N (\{\underset{˙}{0}\}) \leftrightarrow X = \underset{˙}{0})$
24	23	necon3bid	$⊢ φ \to (N (\{X\}) \neq N (\{\underset{˙}{0}\}) \leftrightarrow X \neq \underset{˙}{0})$
25	14 24	mpbird	$⊢ φ \to N (\{X\}) \neq N (\{\underset{˙}{0}\})$
26	25	adantr	$⊢ (φ \land Y \underset{˙}{+} Z = \underset{˙}{0}) \to N (\{X\}) \neq N (\{\underset{˙}{0}\})$
27		sneq	$⊢ Y \underset{˙}{+} Z = \underset{˙}{0} \to \{Y \underset{˙}{+} Z\} = \{\underset{˙}{0}\}$
28	27	fveq2d	$⊢ Y \underset{˙}{+} Z = \underset{˙}{0} \to N (\{Y \underset{˙}{+} Z\}) = N (\{\underset{˙}{0}\})$
29	28	adantl	$⊢ (φ \land Y \underset{˙}{+} Z = \underset{˙}{0}) \to N (\{Y \underset{˙}{+} Z\}) = N (\{\underset{˙}{0}\})$
30	26 29	neeqtrrd	$⊢ (φ \land Y \underset{˙}{+} Z = \underset{˙}{0}) \to N (\{X\}) \neq N (\{Y \underset{˙}{+} Z\})$
31	11	adantr	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to N (\{X\}) \neq N (\{Y\})$
32	5	adantr	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to W \in LVec$
33	6	adantr	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to X \in (V ∖ \{\underset{˙}{0}\})$
34	7	adantr	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to Y \in (V ∖ \{\underset{˙}{0}\})$
35	8	adantr	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to Z \in (V ∖ \{\underset{˙}{0}\})$
36	9	adantr	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to w \in (V ∖ \{\underset{˙}{0}\})$
37	10	adantr	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to N (\{Y\}) = N (\{Z\})$
38	12	adantr	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to \neg w \in N (\{X, Y\})$
39		simpr	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to Y \underset{˙}{+} Z \neq \underset{˙}{0}$
40	1 2 3 4 32 33 34 35 36 37 31 38 39	mapdindp0	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to N (\{Y \underset{˙}{+} Z\}) = N (\{Y\})$
41	31 40	neeqtrrd	$⊢ (φ \land Y \underset{˙}{+} Z \neq \underset{˙}{0}) \to N (\{X\}) \neq N (\{Y \underset{˙}{+} Z\})$
42	30 41	pm2.61dane	$⊢ φ \to N (\{X\}) \neq N (\{Y \underset{˙}{+} Z\})$

Metamath Proof Explorer

Theorem mapdindp1

Proof