lsmcv2

Description: Subspace sum has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of Kalmbach p. 153. ( spansncv2 analog.) (Contributed by NM, 10-Jan-2015)

	Ref	Expression
Hypotheses	lsmcv2.v	$⊢ V = {Base}_{W}$
	lsmcv2.s	$⊢ S = LSubSp (W)$
	lsmcv2.n	$⊢ N = LSpan (W)$
	lsmcv2.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lsmcv2.c	$⊢ C = ⋖_{L} (W)$
	lsmcv2.w	$⊢ φ \to W \in LVec$
	lsmcv2.u	$⊢ φ \to U \in S$
	lsmcv2.x	$⊢ φ \to X \in V$
	lsmcv2.l	$⊢ φ \to \neg N (\{X\}) \subseteq U$
Assertion	lsmcv2	$⊢ φ \to U C (U \underset{˙}{\oplus} N (\{X\}))$

Proof

Step	Hyp	Ref	Expression
1		lsmcv2.v	$⊢ V = {Base}_{W}$
2		lsmcv2.s	$⊢ S = LSubSp (W)$
3		lsmcv2.n	$⊢ N = LSpan (W)$
4		lsmcv2.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
5		lsmcv2.c	$⊢ C = ⋖_{L} (W)$
6		lsmcv2.w	$⊢ φ \to W \in LVec$
7		lsmcv2.u	$⊢ φ \to U \in S$
8		lsmcv2.x	$⊢ φ \to X \in V$
9		lsmcv2.l	$⊢ φ \to \neg N (\{X\}) \subseteq U$
10		lveclmod	$⊢ W \in LVec \to W \in LMod$
11	6 10	syl	$⊢ φ \to W \in LMod$
12	2	lsssssubg	$⊢ W \in LMod \to S \subseteq SubGrp (W)$
13	11 12	syl	$⊢ φ \to S \subseteq SubGrp (W)$
14	13 7	sseldd	$⊢ φ \to U \in SubGrp (W)$
15	1 2 3	lspsncl	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in S$
16	11 8 15	syl2anc	$⊢ φ \to N (\{X\}) \in S$
17	13 16	sseldd	$⊢ φ \to N (\{X\}) \in SubGrp (W)$
18	4 14 17	lssnle	$⊢ φ \to (\neg N (\{X\}) \subseteq U \leftrightarrow U \subset U \underset{˙}{\oplus} N (\{X\}))$
19	9 18	mpbid	$⊢ φ \to U \subset U \underset{˙}{\oplus} N (\{X\})$
20		3simpa	$⊢ (φ \land x \in S \land (U \subset x \land x \subseteq U \underset{˙}{\oplus} N (\{X\}))) \to (φ \land x \in S)$
21		simp3l	$⊢ (φ \land x \in S \land (U \subset x \land x \subseteq U \underset{˙}{\oplus} N (\{X\}))) \to U \subset x$
22		simp3r	$⊢ (φ \land x \in S \land (U \subset x \land x \subseteq U \underset{˙}{\oplus} N (\{X\}))) \to x \subseteq U \underset{˙}{\oplus} N (\{X\})$
23	6	adantr	$⊢ (φ \land x \in S) \to W \in LVec$
24	7	adantr	$⊢ (φ \land x \in S) \to U \in S$
25		simpr	$⊢ (φ \land x \in S) \to x \in S$
26	8	adantr	$⊢ (φ \land x \in S) \to X \in V$
27	1 2 3 4 23 24 25 26	lsmcv	$⊢ ((φ \land x \in S) \land U \subset x \land x \subseteq U \underset{˙}{\oplus} N (\{X\})) \to x = U \underset{˙}{\oplus} N (\{X\})$
28	20 21 22 27	syl3anc	$⊢ (φ \land x \in S \land (U \subset x \land x \subseteq U \underset{˙}{\oplus} N (\{X\}))) \to x = U \underset{˙}{\oplus} N (\{X\})$
29	28	3exp	$⊢ φ \to (x \in S \to ((U \subset x \land x \subseteq U \underset{˙}{\oplus} N (\{X\})) \to x = U \underset{˙}{\oplus} N (\{X\})))$
30	29	ralrimiv	$⊢ φ \to \forall x \in S ((U \subset x \land x \subseteq U \underset{˙}{\oplus} N (\{X\})) \to x = U \underset{˙}{\oplus} N (\{X\}))$
31	2 4	lsmcl	$⊢ (W \in LMod \land U \in S \land N (\{X\}) \in S) \to U \underset{˙}{\oplus} N (\{X\}) \in S$
32	11 7 16 31	syl3anc	$⊢ φ \to U \underset{˙}{\oplus} N (\{X\}) \in S$
33	2 5 6 7 32	lcvbr2	$⊢ φ \to (U C (U \underset{˙}{\oplus} N (\{X\})) \leftrightarrow (U \subset U \underset{˙}{\oplus} N (\{X\}) \land \forall x \in S ((U \subset x \land x \subseteq U \underset{˙}{\oplus} N (\{X\})) \to x = U \underset{˙}{\oplus} N (\{X\}))))$
34	19 30 33	mpbir2and	$⊢ φ \to U C (U \underset{˙}{\oplus} N (\{X\}))$

Metamath Proof Explorer

Theorem lsmcv2

Proof