lspabs2

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$
	lspabs2.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	lspabs2.e	$⊢ φ \to N (\{X\}) = N (\{X \underset{˙}{+} Y\})$
Assertion	lspabs2	$⊢ φ \to N (\{X\}) = N (\{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		lspabs2.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
8		lspabs2.e	$⊢ φ \to N (\{X\}) = N (\{X \underset{˙}{+} Y\})$
9		lveclmod	$⊢ W \in LVec \to W \in LMod$
10	5 9	syl	$⊢ φ \to W \in LMod$
11	1 4	lspsnsubg	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in SubGrp (W)$
12	10 6 11	syl2anc	$⊢ φ \to N (\{X\}) \in SubGrp (W)$
13	7	eldifad	$⊢ φ \to Y \in V$
14	1 4	lspsnsubg	$⊢ (W \in LMod \land Y \in V) \to N (\{Y\}) \in SubGrp (W)$
15	10 13 14	syl2anc	$⊢ φ \to N (\{Y\}) \in SubGrp (W)$
16		eqid	$⊢ LSSum (W) = LSSum (W)$
17	16	lsmub2	$⊢ (N (\{X\}) \in SubGrp (W) \land N (\{Y\}) \in SubGrp (W)) \to N (\{Y\}) \subseteq N (\{X\}) LSSum (W) N (\{Y\})$
18	12 15 17	syl2anc	$⊢ φ \to N (\{Y\}) \subseteq N (\{X\}) LSSum (W) N (\{Y\})$
19	8	oveq2d	$⊢ φ \to N (\{X\}) LSSum (W) N (\{X\}) = N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\})$
20	16	lsmidm	$⊢ N (\{X\}) \in SubGrp (W) \to N (\{X\}) LSSum (W) N (\{X\}) = N (\{X\})$
21	12 20	syl	$⊢ φ \to N (\{X\}) LSSum (W) N (\{X\}) = N (\{X\})$
22	1 2 4 10 6 13	lspprabs	$⊢ φ \to N (\{X, X \underset{˙}{+} Y\}) = N (\{X, Y\})$
23	1 2	lmodvacl	$⊢ (W \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{+} Y \in V$
24	10 6 13 23	syl3anc	$⊢ φ \to X \underset{˙}{+} Y \in V$
25	1 4 16 10 6 24	lsmpr	$⊢ φ \to N (\{X, X \underset{˙}{+} Y\}) = N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\})$
26	1 4 16 10 6 13	lsmpr	$⊢ φ \to N (\{X, Y\}) = N (\{X\}) LSSum (W) N (\{Y\})$
27	22 25 26	3eqtr3d	$⊢ φ \to N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\}) = N (\{X\}) LSSum (W) N (\{Y\})$
28	19 21 27	3eqtr3rd	$⊢ φ \to N (\{X\}) LSSum (W) N (\{Y\}) = N (\{X\})$
29	18 28	sseqtrd	$⊢ φ \to N (\{Y\}) \subseteq N (\{X\})$
30	1 3 4 5 7 6	lspsncmp	$⊢ φ \to (N (\{Y\}) \subseteq N (\{X\}) \leftrightarrow N (\{Y\}) = N (\{X\}))$
31	29 30	mpbid	$⊢ φ \to N (\{Y\}) = N (\{X\})$
32	31	eqcomd	$⊢ φ \to N (\{X\}) = N (\{Y\})$

Metamath Proof Explorer

Theorem lspabs2

Proof