lspabs3

Description: Absorption law for span of vector sum. (Contributed by NM, 30-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lspabs2.v	$⊢ V = {Base}_{W}$
2		lspabs2.p	$⊢ \underset{˙}{+} = +_{W}$
3		lspabs2.o	$⊢ \underset{˙}{0} = 0_{W}$
4		lspabs2.n	$⊢ N = LSpan (W)$
5		lspabs2.w	$⊢ φ \to W \in LVec$
6		lspabs2.x	$⊢ φ \to X \in V$
7		lspabs3.y	$⊢ φ \to Y \in V$
8		lspabs3.xy	$⊢ φ \to X \underset{˙}{+} Y \neq \underset{˙}{0}$
9		lspabs3.e	$⊢ φ \to N (\{X\}) = N (\{Y\})$
10		eqid	$⊢ LSubSp (W) = LSubSp (W)$
11		lveclmod	$⊢ W \in LVec \to W \in LMod$
12	5 11	syl	$⊢ φ \to W \in LMod$
13	1 10 4	lspsncl	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (W)$
14	12 6 13	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (W)$
15	1 10 4	lspsncl	$⊢ (W \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (W)$
16	12 7 15	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (W)$
17		eqid	$⊢ LSSum (W) = LSSum (W)$
18	10 17	lsmcl	$⊢ (W \in LMod \land N (\{X\}) \in LSubSp (W) \land N (\{Y\}) \in LSubSp (W)) \to N (\{X\}) LSSum (W) N (\{Y\}) \in LSubSp (W)$
19	12 14 16 18	syl3anc	$⊢ φ \to N (\{X\}) LSSum (W) N (\{Y\}) \in LSubSp (W)$
20	1 4	lspsnsubg	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in SubGrp (W)$
21	12 6 20	syl2anc	$⊢ φ \to N (\{X\}) \in SubGrp (W)$
22	9 21	eqeltrrd	$⊢ φ \to N (\{Y\}) \in SubGrp (W)$
23	1 4	lspsnid	$⊢ (W \in LMod \land X \in V) \to X \in N (\{X\})$
24	12 6 23	syl2anc	$⊢ φ \to X \in N (\{X\})$
25	1 4	lspsnid	$⊢ (W \in LMod \land Y \in V) \to Y \in N (\{Y\})$
26	12 7 25	syl2anc	$⊢ φ \to Y \in N (\{Y\})$
27	2 17	lsmelvali	$⊢ ((N (\{X\}) \in SubGrp (W) \land N (\{Y\}) \in SubGrp (W)) \land (X \in N (\{X\}) \land Y \in N (\{Y\}))) \to X \underset{˙}{+} Y \in (N (\{X\}) LSSum (W) N (\{Y\}))$
28	21 22 24 26 27	syl22anc	$⊢ φ \to X \underset{˙}{+} Y \in (N (\{X\}) LSSum (W) N (\{Y\}))$
29	10 4 12 19 28	lspsnel5a	$⊢ φ \to N (\{X \underset{˙}{+} Y\}) \subseteq N (\{X\}) LSSum (W) N (\{Y\})$
30	9	oveq2d	$⊢ φ \to N (\{X\}) LSSum (W) N (\{X\}) = N (\{X\}) LSSum (W) N (\{Y\})$
31	17	lsmidm	$⊢ N (\{X\}) \in SubGrp (W) \to N (\{X\}) LSSum (W) N (\{X\}) = N (\{X\})$
32	21 31	syl	$⊢ φ \to N (\{X\}) LSSum (W) N (\{X\}) = N (\{X\})$
33	30 32	eqtr3d	$⊢ φ \to N (\{X\}) LSSum (W) N (\{Y\}) = N (\{X\})$
34	29 33	sseqtrd	$⊢ φ \to N (\{X \underset{˙}{+} Y\}) \subseteq N (\{X\})$
35	1 2	lmodvacl	$⊢ (W \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{+} Y \in V$
36	12 6 7 35	syl3anc	$⊢ φ \to X \underset{˙}{+} Y \in V$
37		eldifsn	$⊢ X \underset{˙}{+} Y \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (X \underset{˙}{+} Y \in V \land X \underset{˙}{+} Y \neq \underset{˙}{0})$
38	36 8 37	sylanbrc	$⊢ φ \to X \underset{˙}{+} Y \in (V ∖ \{\underset{˙}{0}\})$
39	1 3 4 5 38 6	lspsncmp	$⊢ φ \to (N (\{X \underset{˙}{+} Y\}) \subseteq N (\{X\}) \leftrightarrow N (\{X \underset{˙}{+} Y\}) = N (\{X\}))$
40	34 39	mpbid	$⊢ φ \to N (\{X \underset{˙}{+} Y\}) = N (\{X\})$
41	40	eqcomd	$⊢ φ \to N (\{X\}) = N (\{X \underset{˙}{+} Y\})$

Metamath Proof Explorer

Theorem lspabs3

Proof