lsmcv

Description: Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of Kalmbach p. 153. ( spansncvi analog.) TODO: ugly proof; can it be shortened? (Contributed by NM, 2-Oct-2014)

	Ref	Expression
Hypotheses	lsmcv.v	$⊢ V = {Base}_{W}$
	lsmcv.s	$⊢ S = LSubSp (W)$
	lsmcv.n	$⊢ N = LSpan (W)$
	lsmcv.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lsmcv.w	$⊢ φ \to W \in LVec$
	lsmcv.t	$⊢ φ \to T \in S$
	lsmcv.u	$⊢ φ \to U \in S$
	lsmcv.x	$⊢ φ \to X \in V$
Assertion	lsmcv	$⊢ (φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \to U = T \underset{˙}{\oplus} N (\{X\})$

Proof

Step	Hyp	Ref	Expression
1		lsmcv.v	$⊢ V = {Base}_{W}$
2		lsmcv.s	$⊢ S = LSubSp (W)$
3		lsmcv.n	$⊢ N = LSpan (W)$
4		lsmcv.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
5		lsmcv.w	$⊢ φ \to W \in LVec$
6		lsmcv.t	$⊢ φ \to T \in S$
7		lsmcv.u	$⊢ φ \to U \in S$
8		lsmcv.x	$⊢ φ \to X \in V$
9		simp3	$⊢ (φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \to U \subseteq T \underset{˙}{\oplus} N (\{X\})$
10		simp2	$⊢ (φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \to T \subset U$
11		pssss	$⊢ T \subset U \to T \subseteq U$
12	10 11	syl	$⊢ (φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \to T \subseteq U$
13		pssnel	$⊢ T \subset U \to \exists x (x \in U \land \neg x \in T)$
14	10 13	syl	$⊢ (φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \to \exists x (x \in U \land \neg x \in T)$
15		simpl3	$⊢ ((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \to U \subseteq T \underset{˙}{\oplus} N (\{X\})$
16		simprl	$⊢ ((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \to x \in U$
17	15 16	sseldd	$⊢ ((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \to x \in (T \underset{˙}{\oplus} N (\{X\}))$
18		lveclmod	$⊢ W \in LVec \to W \in LMod$
19	5 18	syl	$⊢ φ \to W \in LMod$
20	2	lsssssubg	$⊢ W \in LMod \to S \subseteq SubGrp (W)$
21	19 20	syl	$⊢ φ \to S \subseteq SubGrp (W)$
22	21 6	sseldd	$⊢ φ \to T \in SubGrp (W)$
23	1 2 3	lspsncl	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in S$
24	19 8 23	syl2anc	$⊢ φ \to N (\{X\}) \in S$
25	21 24	sseldd	$⊢ φ \to N (\{X\}) \in SubGrp (W)$
26		eqid	$⊢ +_{W} = +_{W}$
27	26 4	lsmelval	$⊢ (T \in SubGrp (W) \land N (\{X\}) \in SubGrp (W)) \to (x \in (T \underset{˙}{\oplus} N (\{X\})) \leftrightarrow \exists y \in T \exists z \in N (\{X\}) x = y +_{W} z)$
28	22 25 27	syl2anc	$⊢ φ \to (x \in (T \underset{˙}{\oplus} N (\{X\})) \leftrightarrow \exists y \in T \exists z \in N (\{X\}) x = y +_{W} z)$
29	28	3ad2ant1	$⊢ (φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \to (x \in (T \underset{˙}{\oplus} N (\{X\})) \leftrightarrow \exists y \in T \exists z \in N (\{X\}) x = y +_{W} z)$
30	29	adantr	$⊢ ((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \to (x \in (T \underset{˙}{\oplus} N (\{X\})) \leftrightarrow \exists y \in T \exists z \in N (\{X\}) x = y +_{W} z)$
31	17 30	mpbid	$⊢ ((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \to \exists y \in T \exists z \in N (\{X\}) x = y +_{W} z$
32		simp1rr	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to \neg x \in T$
33		simp2l	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to y \in T$
34		oveq2	$⊢ z = 0_{W} \to y +_{W} z = y +_{W} 0_{W}$
35	34	eqeq2d	$⊢ z = 0_{W} \to (x = y +_{W} z \leftrightarrow x = y +_{W} 0_{W})$
36	35	biimpac	$⊢ (x = y +_{W} z \land z = 0_{W}) \to x = y +_{W} 0_{W}$
37	19	3ad2ant1	$⊢ (φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \to W \in LMod$
38	37	ad2antrr	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\}))) \to W \in LMod$
39	6	3ad2ant1	$⊢ (φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \to T \in S$
40	39	ad2antrr	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\}))) \to T \in S$
41		simprl	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\}))) \to y \in T$
42	1 2	lssel	$⊢ (T \in S \land y \in T) \to y \in V$
43	40 41 42	syl2anc	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\}))) \to y \in V$
44		eqid	$⊢ 0_{W} = 0_{W}$
45	1 26 44	lmod0vrid	$⊢ (W \in LMod \land y \in V) \to y +_{W} 0_{W} = y$
46	38 43 45	syl2anc	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\}))) \to y +_{W} 0_{W} = y$
47	46	eqeq2d	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\}))) \to (x = y +_{W} 0_{W} \leftrightarrow x = y)$
48	47	biimpd	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\}))) \to (x = y +_{W} 0_{W} \to x = y)$
49	48	ex	$⊢ ((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \to ((y \in T \land z \in N (\{X\})) \to (x = y +_{W} 0_{W} \to x = y))$
50	36 49	syl7	$⊢ ((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \to ((y \in T \land z \in N (\{X\})) \to ((x = y +_{W} z \land z = 0_{W}) \to x = y))$
51	50	exp4a	$⊢ ((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \to ((y \in T \land z \in N (\{X\})) \to (x = y +_{W} z \to (z = 0_{W} \to x = y)))$
52	51	3imp	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to (z = 0_{W} \to x = y)$
53		eleq1	$⊢ x = y \to (x \in T \leftrightarrow y \in T)$
54	53	biimparc	$⊢ (y \in T \land x = y) \to x \in T$
55	33 52 54	syl6an	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to (z = 0_{W} \to x \in T)$
56	55	necon3bd	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to (\neg x \in T \to z \neq 0_{W})$
57	32 56	mpd	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to z \neq 0_{W}$
58	5	3ad2ant1	$⊢ (φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \to W \in LVec$
59	58	adantr	$⊢ ((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \to W \in LVec$
60	59	3ad2ant1	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to W \in LVec$
61		lmodabl	$⊢ W \in LMod \to W \in Abel$
62	18 61	syl	$⊢ W \in LVec \to W \in Abel$
63	60 62	syl	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to W \in Abel$
64		simp1l1	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to φ$
65	64 6	syl	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to T \in S$
66	65 33 42	syl2anc	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to y \in V$
67	60 18	syl	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to W \in LMod$
68	64 8	syl	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to X \in V$
69	67 68 23	syl2anc	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to N (\{X\}) \in S$
70		simp2r	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to z \in N (\{X\})$
71	1 2	lssel	$⊢ (N (\{X\}) \in S \land z \in N (\{X\})) \to z \in V$
72	69 70 71	syl2anc	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to z \in V$
73		eqid	$⊢ -_{W} = -_{W}$
74	1 26 73	ablpncan2	$⊢ (W \in Abel \land y \in V \land z \in V) \to (y +_{W} z) -_{W} y = z$
75	63 66 72 74	syl3anc	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to (y +_{W} z) -_{W} y = z$
76	64 7	syl	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to U \in S$
77		simp3	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to x = y +_{W} z$
78		simp1rl	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to x \in U$
79	77 78	eqeltrrd	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to y +_{W} z \in U$
80		simp1l2	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to T \subset U$
81	11	sselda	$⊢ (T \subset U \land y \in T) \to y \in U$
82	80 33 81	syl2anc	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to y \in U$
83	73 2	lssvsubcl	$⊢ ((W \in LMod \land U \in S) \land (y +_{W} z \in U \land y \in U)) \to (y +_{W} z) -_{W} y \in U$
84	67 76 79 82 83	syl22anc	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to (y +_{W} z) -_{W} y \in U$
85	75 84	eqeltrrd	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to z \in U$
86	60	3ad2ant1	$⊢ ((((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \land z \neq 0_{W} \land z \in U) \to W \in LVec$
87	64	3ad2ant1	$⊢ ((((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \land z \neq 0_{W} \land z \in U) \to φ$
88	87 8	syl	$⊢ ((((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \land z \neq 0_{W} \land z \in U) \to X \in V$
89		simp12r	$⊢ ((((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \land z \neq 0_{W} \land z \in U) \to z \in N (\{X\})$
90		simp2	$⊢ ((((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \land z \neq 0_{W} \land z \in U) \to z \neq 0_{W}$
91	1 44 3 86 88 89 90	lspsneleq	$⊢ ((((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \land z \neq 0_{W} \land z \in U) \to N (\{z\}) = N (\{X\})$
92	86 18	syl	$⊢ ((((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \land z \neq 0_{W} \land z \in U) \to W \in LMod$
93	87 7	syl	$⊢ ((((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \land z \neq 0_{W} \land z \in U) \to U \in S$
94		simp3	$⊢ ((((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \land z \neq 0_{W} \land z \in U) \to z \in U$
95	2 3 92 93 94	ellspsn5	$⊢ ((((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \land z \neq 0_{W} \land z \in U) \to N (\{z\}) \subseteq U$
96	91 95	eqsstrrd	$⊢ ((((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \land z \neq 0_{W} \land z \in U) \to N (\{X\}) \subseteq U$
97	57 85 96	mpd3an23	$⊢ (((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \land (y \in T \land z \in N (\{X\})) \land x = y +_{W} z) \to N (\{X\}) \subseteq U$
98	97	3exp	$⊢ ((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \to ((y \in T \land z \in N (\{X\})) \to (x = y +_{W} z \to N (\{X\}) \subseteq U))$
99	98	rexlimdvv	$⊢ ((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \to (\exists y \in T \exists z \in N (\{X\}) x = y +_{W} z \to N (\{X\}) \subseteq U)$
100	31 99	mpd	$⊢ ((φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \land (x \in U \land \neg x \in T)) \to N (\{X\}) \subseteq U$
101	14 100	exlimddv	$⊢ (φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \to N (\{X\}) \subseteq U$
102	21 7	sseldd	$⊢ φ \to U \in SubGrp (W)$
103	4	lsmlub	$⊢ (T \in SubGrp (W) \land N (\{X\}) \in SubGrp (W) \land U \in SubGrp (W)) \to ((T \subseteq U \land N (\{X\}) \subseteq U) \leftrightarrow T \underset{˙}{\oplus} N (\{X\}) \subseteq U)$
104	22 25 102 103	syl3anc	$⊢ φ \to ((T \subseteq U \land N (\{X\}) \subseteq U) \leftrightarrow T \underset{˙}{\oplus} N (\{X\}) \subseteq U)$
105	104	3ad2ant1	$⊢ (φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \to ((T \subseteq U \land N (\{X\}) \subseteq U) \leftrightarrow T \underset{˙}{\oplus} N (\{X\}) \subseteq U)$
106	12 101 105	mpbi2and	$⊢ (φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \to T \underset{˙}{\oplus} N (\{X\}) \subseteq U$
107	9 106	eqssd	$⊢ (φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} N (\{X\})) \to U = T \underset{˙}{\oplus} N (\{X\})$

Metamath Proof Explorer

Theorem lsmcv

Proof