lspprabs

Description: Absorption of vector sum into span of pair. (Contributed by NM, 27-Apr-2015)

	Ref	Expression
Hypotheses	lspprabs.v	$⊢ V = {Base}_{W}$
	lspprabs.p	$⊢ \underset{˙}{+} = +_{W}$
	lspprabs.n	$⊢ N = LSpan (W)$
	lspprabs.w	$⊢ φ \to W \in LMod$
	lspprabs.x	$⊢ φ \to X \in V$
	lspprabs.y	$⊢ φ \to Y \in V$
Assertion	lspprabs	$⊢ φ \to N (\{X, X \underset{˙}{+} Y\}) = N (\{X, Y\})$

Proof

Step	Hyp	Ref	Expression
1		lspprabs.v	$⊢ V = {Base}_{W}$
2		lspprabs.p	$⊢ \underset{˙}{+} = +_{W}$
3		lspprabs.n	$⊢ N = LSpan (W)$
4		lspprabs.w	$⊢ φ \to W \in LMod$
5		lspprabs.x	$⊢ φ \to X \in V$
6		lspprabs.y	$⊢ φ \to Y \in V$
7		eqid	$⊢ LSubSp (W) = LSubSp (W)$
8	7	lsssssubg	$⊢ W \in LMod \to LSubSp (W) \subseteq SubGrp (W)$
9	4 8	syl	$⊢ φ \to LSubSp (W) \subseteq SubGrp (W)$
10	1 7 3	lspsncl	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (W)$
11	4 5 10	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (W)$
12	9 11	sseldd	$⊢ φ \to N (\{X\}) \in SubGrp (W)$
13	1 7 3	lspsncl	$⊢ (W \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (W)$
14	4 6 13	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (W)$
15	9 14	sseldd	$⊢ φ \to N (\{Y\}) \in SubGrp (W)$
16		eqid	$⊢ LSSum (W) = LSSum (W)$
17	16	lsmub1	$⊢ (N (\{X\}) \in SubGrp (W) \land N (\{Y\}) \in SubGrp (W)) \to N (\{X\}) \subseteq N (\{X\}) LSSum (W) N (\{Y\})$
18	12 15 17	syl2anc	$⊢ φ \to N (\{X\}) \subseteq N (\{X\}) LSSum (W) N (\{Y\})$
19	7 16	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)$
20	4 11 14 19	syl3anc	$⊢ φ \to N (\{X\}) LSSum (W) N (\{Y\}) \in LSubSp (W)$
21	1 3	lspsnid	$⊢ (W \in LMod \land X \in V) \to X \in N (\{X\})$
22	4 5 21	syl2anc	$⊢ φ \to X \in N (\{X\})$
23	1 3	lspsnid	$⊢ (W \in LMod \land Y \in V) \to Y \in N (\{Y\})$
24	4 6 23	syl2anc	$⊢ φ \to Y \in N (\{Y\})$
25	2 16	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\}))$
26	12 15 22 24 25	syl22anc	$⊢ φ \to X \underset{˙}{+} Y \in (N (\{X\}) LSSum (W) N (\{Y\}))$
27	7 3 4 20 26	ellspsn5	$⊢ φ \to N (\{X \underset{˙}{+} Y\}) \subseteq N (\{X\}) LSSum (W) N (\{Y\})$
28	1 2	lmodvacl	$⊢ (W \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{+} Y \in V$
29	4 5 6 28	syl3anc	$⊢ φ \to X \underset{˙}{+} Y \in V$
30	1 7 3	lspsncl	$⊢ (W \in LMod \land X \underset{˙}{+} Y \in V) \to N (\{X \underset{˙}{+} Y\}) \in LSubSp (W)$
31	4 29 30	syl2anc	$⊢ φ \to N (\{X \underset{˙}{+} Y\}) \in LSubSp (W)$
32	9 31	sseldd	$⊢ φ \to N (\{X \underset{˙}{+} Y\}) \in SubGrp (W)$
33	9 20	sseldd	$⊢ φ \to N (\{X\}) LSSum (W) N (\{Y\}) \in SubGrp (W)$
34	16	lsmlub	$⊢ (N (\{X\}) \in SubGrp (W) \land N (\{X \underset{˙}{+} Y\}) \in SubGrp (W) \land N (\{X\}) LSSum (W) N (\{Y\}) \in SubGrp (W)) \to ((N (\{X\}) \subseteq N (\{X\}) LSSum (W) N (\{Y\}) \land N (\{X \underset{˙}{+} Y\}) \subseteq N (\{X\}) LSSum (W) N (\{Y\})) \leftrightarrow N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\}) \subseteq N (\{X\}) LSSum (W) N (\{Y\}))$
35	12 32 33 34	syl3anc	$⊢ φ \to ((N (\{X\}) \subseteq N (\{X\}) LSSum (W) N (\{Y\}) \land N (\{X \underset{˙}{+} Y\}) \subseteq N (\{X\}) LSSum (W) N (\{Y\})) \leftrightarrow N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\}) \subseteq N (\{X\}) LSSum (W) N (\{Y\}))$
36	18 27 35	mpbi2and	$⊢ φ \to N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\}) \subseteq N (\{X\}) LSSum (W) N (\{Y\})$
37	16	lsmub1	$⊢ (N (\{X\}) \in SubGrp (W) \land N (\{X \underset{˙}{+} Y\}) \in SubGrp (W)) \to N (\{X\}) \subseteq N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\})$
38	12 32 37	syl2anc	$⊢ φ \to N (\{X\}) \subseteq N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\})$
39	7 16	lsmcl	$⊢ (W \in LMod \land N (\{X\}) \in LSubSp (W) \land N (\{X \underset{˙}{+} Y\}) \in LSubSp (W)) \to N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\}) \in LSubSp (W)$
40	4 11 31 39	syl3anc	$⊢ φ \to N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\}) \in LSubSp (W)$
41		eqid	$⊢ -_{W} = -_{W}$
42	1 3	lspsnid	$⊢ (W \in LMod \land X \underset{˙}{+} Y \in V) \to X \underset{˙}{+} Y \in N (\{X \underset{˙}{+} Y\})$
43	4 29 42	syl2anc	$⊢ φ \to X \underset{˙}{+} Y \in N (\{X \underset{˙}{+} Y\})$
44	41 16 32 12 43 22	lsmelvalmi	$⊢ φ \to (X \underset{˙}{+} Y) -_{W} X \in (N (\{X \underset{˙}{+} Y\}) LSSum (W) N (\{X\}))$
45		lmodabl	$⊢ W \in LMod \to W \in Abel$
46	4 45	syl	$⊢ φ \to W \in Abel$
47	1 2 41	ablpncan2	$⊢ (W \in Abel \land X \in V \land Y \in V) \to (X \underset{˙}{+} Y) -_{W} X = Y$
48	46 5 6 47	syl3anc	$⊢ φ \to (X \underset{˙}{+} Y) -_{W} X = Y$
49	16	lsmcom	$⊢ (W \in Abel \land N (\{X \underset{˙}{+} Y\}) \in SubGrp (W) \land N (\{X\}) \in SubGrp (W)) \to N (\{X \underset{˙}{+} Y\}) LSSum (W) N (\{X\}) = N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\})$
50	46 32 12 49	syl3anc	$⊢ φ \to N (\{X \underset{˙}{+} Y\}) LSSum (W) N (\{X\}) = N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\})$
51	44 48 50	3eltr3d	$⊢ φ \to Y \in (N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\}))$
52	7 3 4 40 51	ellspsn5	$⊢ φ \to N (\{Y\}) \subseteq N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\})$
53	9 40	sseldd	$⊢ φ \to N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\}) \in SubGrp (W)$
54	16	lsmlub	$⊢ (N (\{X\}) \in SubGrp (W) \land N (\{Y\}) \in SubGrp (W) \land N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\}) \in SubGrp (W)) \to ((N (\{X\}) \subseteq N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\}) \land N (\{Y\}) \subseteq N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\})) \leftrightarrow N (\{X\}) LSSum (W) N (\{Y\}) \subseteq N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\}))$
55	12 15 53 54	syl3anc	$⊢ φ \to ((N (\{X\}) \subseteq N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\}) \land N (\{Y\}) \subseteq N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\})) \leftrightarrow N (\{X\}) LSSum (W) N (\{Y\}) \subseteq N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\}))$
56	38 52 55	mpbi2and	$⊢ φ \to N (\{X\}) LSSum (W) N (\{Y\}) \subseteq N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\})$
57	36 56	eqssd	$⊢ φ \to N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\}) = N (\{X\}) LSSum (W) N (\{Y\})$
58	1 3 16 4 5 29	lsmpr	$⊢ φ \to N (\{X, X \underset{˙}{+} Y\}) = N (\{X\}) LSSum (W) N (\{X \underset{˙}{+} Y\})$
59	1 3 16 4 5 6	lsmpr	$⊢ φ \to N (\{X, Y\}) = N (\{X\}) LSSum (W) N (\{Y\})$
60	57 58 59	3eqtr4d	$⊢ φ \to N (\{X, X \underset{˙}{+} Y\}) = N (\{X, Y\})$

Metamath Proof Explorer

Theorem lspprabs

Proof