mapdindp4

	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	mapdindp4	$⊢ φ \to \neg Z \in N (\{X, w \underset{˙}{+} Y\})$

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		lveclmod	$⊢ W \in LVec \to W \in LMod$
14	5 13	syl	$⊢ φ \to W \in LMod$
15	9	eldifad	$⊢ φ \to w \in V$
16	7	eldifad	$⊢ φ \to Y \in V$
17	1 2	lmodvacl	$⊢ (W \in LMod \land w \in V \land Y \in V) \to w \underset{˙}{+} Y \in V$
18	14 15 16 17	syl3anc	$⊢ φ \to w \underset{˙}{+} Y \in V$
19	6	eldifad	$⊢ φ \to X \in V$
20	1 4 5 15 19 16 12	lspindpi	$⊢ φ \to (N (\{w\}) \neq N (\{X\}) \land N (\{w\}) \neq N (\{Y\}))$
21	20	simprd	$⊢ φ \to N (\{w\}) \neq N (\{Y\})$
22	21	necomd	$⊢ φ \to N (\{Y\}) \neq N (\{w\})$
23	1 2 3 4 5 16 9 22	lspindp3	$⊢ φ \to N (\{Y\}) \neq N (\{Y \underset{˙}{+} w\})$
24	1 2	lmodcom	$⊢ (W \in LMod \land w \in V \land Y \in V) \to w \underset{˙}{+} Y = Y \underset{˙}{+} w$
25	14 15 16 24	syl3anc	$⊢ φ \to w \underset{˙}{+} Y = Y \underset{˙}{+} w$
26	25	sneqd	$⊢ φ \to \{w \underset{˙}{+} Y\} = \{Y \underset{˙}{+} w\}$
27	26	fveq2d	$⊢ φ \to N (\{w \underset{˙}{+} Y\}) = N (\{Y \underset{˙}{+} w\})$
28	23 27	neeqtrrd	$⊢ φ \to N (\{Y\}) \neq N (\{w \underset{˙}{+} Y\})$
29	10 28	eqnetrrd	$⊢ φ \to N (\{Z\}) \neq N (\{w \underset{˙}{+} Y\})$
30	1 3 4 5 6 16 15 11 12	lspindp1	$⊢ φ \to (N (\{w\}) \neq N (\{Y\}) \land \neg X \in N (\{w, Y\}))$
31	30	simprd	$⊢ φ \to \neg X \in N (\{w, Y\})$
32		eqid	$⊢ LSSum (W) = LSSum (W)$
33	8	eldifad	$⊢ φ \to Z \in V$
34	1 4 32 14 33 18	lsmpr	$⊢ φ \to N (\{Z, w \underset{˙}{+} Y\}) = N (\{Z\}) LSSum (W) N (\{w \underset{˙}{+} Y\})$
35	1 2	lmodcom	$⊢ (W \in LMod \land Y \in V \land w \in V) \to Y \underset{˙}{+} w = w \underset{˙}{+} Y$
36	14 16 15 35	syl3anc	$⊢ φ \to Y \underset{˙}{+} w = w \underset{˙}{+} Y$
37	36	preq2d	$⊢ φ \to \{Y, Y \underset{˙}{+} w\} = \{Y, w \underset{˙}{+} Y\}$
38	37	fveq2d	$⊢ φ \to N (\{Y, Y \underset{˙}{+} w\}) = N (\{Y, w \underset{˙}{+} Y\})$
39	1 2 4 14 16 15	lspprabs	$⊢ φ \to N (\{Y, Y \underset{˙}{+} w\}) = N (\{Y, w\})$
40	1 4 32 14 16 18	lsmpr	$⊢ φ \to N (\{Y, w \underset{˙}{+} Y\}) = N (\{Y\}) LSSum (W) N (\{w \underset{˙}{+} Y\})$
41	38 39 40	3eqtr3rd	$⊢ φ \to N (\{Y\}) LSSum (W) N (\{w \underset{˙}{+} Y\}) = N (\{Y, w\})$
42	10	oveq1d	$⊢ φ \to N (\{Y\}) LSSum (W) N (\{w \underset{˙}{+} Y\}) = N (\{Z\}) LSSum (W) N (\{w \underset{˙}{+} Y\})$
43		prcom	$⊢ \{Y, w\} = \{w, Y\}$
44	43	fveq2i	$⊢ N (\{Y, w\}) = N (\{w, Y\})$
45	44	a1i	$⊢ φ \to N (\{Y, w\}) = N (\{w, Y\})$
46	41 42 45	3eqtr3d	$⊢ φ \to N (\{Z\}) LSSum (W) N (\{w \underset{˙}{+} Y\}) = N (\{w, Y\})$
47	34 46	eqtrd	$⊢ φ \to N (\{Z, w \underset{˙}{+} Y\}) = N (\{w, Y\})$
48	31 47	neleqtrrd	$⊢ φ \to \neg X \in N (\{Z, w \underset{˙}{+} Y\})$
49	1 3 4 5 8 18 19 29 48	lspindp1	$⊢ φ \to (N (\{X\}) \neq N (\{w \underset{˙}{+} Y\}) \land \neg Z \in N (\{X, w \underset{˙}{+} Y\}))$
50	49	simprd	$⊢ φ \to \neg Z \in N (\{X, w \underset{˙}{+} Y\})$

Metamath Proof Explorer

Theorem mapdindp4

Proof