mapdindp0

	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\})$
	mapdindp1.yz	$⊢ φ \to Y \underset{˙}{+} Z \neq \underset{˙}{0}$
Assertion	mapdindp0	$⊢ φ \to N (\{Y \underset{˙}{+} Z\}) = N (\{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		mapdindp1.yz	$⊢ φ \to Y \underset{˙}{+} Z \neq \underset{˙}{0}$
14		eqid	$⊢ LSubSp (W) = LSubSp (W)$
15		lveclmod	$⊢ W \in LVec \to W \in LMod$
16	5 15	syl	$⊢ φ \to W \in LMod$
17	7	eldifad	$⊢ φ \to Y \in V$
18	1 14 4	lspsncl	$⊢ (W \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (W)$
19	16 17 18	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (W)$
20	10 19	eqeltrrd	$⊢ φ \to N (\{Z\}) \in LSubSp (W)$
21		eqid	$⊢ LSSum (W) = LSSum (W)$
22	14 21	lsmcl	$⊢ (W \in LMod \land N (\{Y\}) \in LSubSp (W) \land N (\{Z\}) \in LSubSp (W)) \to N (\{Y\}) LSSum (W) N (\{Z\}) \in LSubSp (W)$
23	16 19 20 22	syl3anc	$⊢ φ \to N (\{Y\}) LSSum (W) N (\{Z\}) \in LSubSp (W)$
24	14	lsssssubg	$⊢ W \in LMod \to LSubSp (W) \subseteq SubGrp (W)$
25	16 24	syl	$⊢ φ \to LSubSp (W) \subseteq SubGrp (W)$
26	25 19	sseldd	$⊢ φ \to N (\{Y\}) \in SubGrp (W)$
27	10 26	eqeltrrd	$⊢ φ \to N (\{Z\}) \in SubGrp (W)$
28	1 4	lspsnid	$⊢ (W \in LMod \land Y \in V) \to Y \in N (\{Y\})$
29	16 17 28	syl2anc	$⊢ φ \to Y \in N (\{Y\})$
30	8	eldifad	$⊢ φ \to Z \in V$
31	1 4	lspsnid	$⊢ (W \in LMod \land Z \in V) \to Z \in N (\{Z\})$
32	16 30 31	syl2anc	$⊢ φ \to Z \in N (\{Z\})$
33	2 21	lsmelvali	$⊢ ((N (\{Y\}) \in SubGrp (W) \land N (\{Z\}) \in SubGrp (W)) \land (Y \in N (\{Y\}) \land Z \in N (\{Z\}))) \to Y \underset{˙}{+} Z \in (N (\{Y\}) LSSum (W) N (\{Z\}))$
34	26 27 29 32 33	syl22anc	$⊢ φ \to Y \underset{˙}{+} Z \in (N (\{Y\}) LSSum (W) N (\{Z\}))$
35	14 4 16 23 34	ellspsn5	$⊢ φ \to N (\{Y \underset{˙}{+} Z\}) \subseteq N (\{Y\}) LSSum (W) N (\{Z\})$
36	10	oveq2d	$⊢ φ \to N (\{Y\}) LSSum (W) N (\{Y\}) = N (\{Y\}) LSSum (W) N (\{Z\})$
37	21	lsmidm	$⊢ N (\{Y\}) \in SubGrp (W) \to N (\{Y\}) LSSum (W) N (\{Y\}) = N (\{Y\})$
38	26 37	syl	$⊢ φ \to N (\{Y\}) LSSum (W) N (\{Y\}) = N (\{Y\})$
39	36 38	eqtr3d	$⊢ φ \to N (\{Y\}) LSSum (W) N (\{Z\}) = N (\{Y\})$
40	35 39	sseqtrd	$⊢ φ \to N (\{Y \underset{˙}{+} Z\}) \subseteq N (\{Y\})$
41	1 2	lmodvacl	$⊢ (W \in LMod \land Y \in V \land Z \in V) \to Y \underset{˙}{+} Z \in V$
42	16 17 30 41	syl3anc	$⊢ φ \to Y \underset{˙}{+} Z \in V$
43		eldifsn	$⊢ Y \underset{˙}{+} Z \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (Y \underset{˙}{+} Z \in V \land Y \underset{˙}{+} Z \neq \underset{˙}{0})$
44	42 13 43	sylanbrc	$⊢ φ \to Y \underset{˙}{+} Z \in (V ∖ \{\underset{˙}{0}\})$
45	1 3 4 5 44 17	lspsncmp	$⊢ φ \to (N (\{Y \underset{˙}{+} Z\}) \subseteq N (\{Y\}) \leftrightarrow N (\{Y \underset{˙}{+} Z\}) = N (\{Y\}))$
46	40 45	mpbid	$⊢ φ \to N (\{Y \underset{˙}{+} Z\}) = N (\{Y\})$

Metamath Proof Explorer

Theorem mapdindp0

Proof