lshpnelb

Description: The subspace sum of a hyperplane and the span of an element equals the vector space iff the element is not in the hyperplane. (Contributed by NM, 2-Oct-2014)

	Ref	Expression
Hypotheses	lshpnelb.v	$⊢ V = {Base}_{W}$
	lshpnelb.n	$⊢ N = LSpan (W)$
	lshpnelb.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lshpnelb.h	$⊢ H = LSHyp (W)$
	lshpnelb.w	$⊢ φ \to W \in LVec$
	lshpnelb.u	$⊢ φ \to U \in H$
	lshpnelb.x	$⊢ φ \to X \in V$
Assertion	lshpnelb	$⊢ φ \to (\neg X \in U \leftrightarrow U \underset{˙}{\oplus} N (\{X\}) = V)$

Proof

Step	Hyp	Ref	Expression
1		lshpnelb.v	$⊢ V = {Base}_{W}$
2		lshpnelb.n	$⊢ N = LSpan (W)$
3		lshpnelb.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
4		lshpnelb.h	$⊢ H = LSHyp (W)$
5		lshpnelb.w	$⊢ φ \to W \in LVec$
6		lshpnelb.u	$⊢ φ \to U \in H$
7		lshpnelb.x	$⊢ φ \to X \in V$
8		eqid	$⊢ LSubSp (W) = LSubSp (W)$
9		lveclmod	$⊢ W \in LVec \to W \in LMod$
10	5 9	syl	$⊢ φ \to W \in LMod$
11	1 2 8 3 4 10	islshpsm	$⊢ φ \to (U \in H \leftrightarrow (U \in LSubSp (W) \land U \neq V \land \exists v \in V U \underset{˙}{\oplus} N (\{v\}) = V))$
12	6 11	mpbid	$⊢ φ \to (U \in LSubSp (W) \land U \neq V \land \exists v \in V U \underset{˙}{\oplus} N (\{v\}) = V)$
13	12	simp3d	$⊢ φ \to \exists v \in V U \underset{˙}{\oplus} N (\{v\}) = V$
14	13	adantr	$⊢ (φ \land \neg X \in U) \to \exists v \in V U \underset{˙}{\oplus} N (\{v\}) = V$
15		simp1l	$⊢ ((φ \land \neg X \in U) \land v \in V \land U \underset{˙}{\oplus} N (\{v\}) = V) \to φ$
16		simp2	$⊢ ((φ \land \neg X \in U) \land v \in V \land U \underset{˙}{\oplus} N (\{v\}) = V) \to v \in V$
17	8	lsssssubg	$⊢ W \in LMod \to LSubSp (W) \subseteq SubGrp (W)$
18	10 17	syl	$⊢ φ \to LSubSp (W) \subseteq SubGrp (W)$
19	8 4 10 6	lshplss	$⊢ φ \to U \in LSubSp (W)$
20	18 19	sseldd	$⊢ φ \to U \in SubGrp (W)$
21	1 8 2	lspsncl	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (W)$
22	10 7 21	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (W)$
23	18 22	sseldd	$⊢ φ \to N (\{X\}) \in SubGrp (W)$
24	3	lsmub1	$⊢ (U \in SubGrp (W) \land N (\{X\}) \in SubGrp (W)) \to U \subseteq U \underset{˙}{\oplus} N (\{X\})$
25	20 23 24	syl2anc	$⊢ φ \to U \subseteq U \underset{˙}{\oplus} N (\{X\})$
26	25	adantr	$⊢ (φ \land \neg X \in U) \to U \subseteq U \underset{˙}{\oplus} N (\{X\})$
27	3	lsmub2	$⊢ (U \in SubGrp (W) \land N (\{X\}) \in SubGrp (W)) \to N (\{X\}) \subseteq U \underset{˙}{\oplus} N (\{X\})$
28	20 23 27	syl2anc	$⊢ φ \to N (\{X\}) \subseteq U \underset{˙}{\oplus} N (\{X\})$
29	1 2	lspsnid	$⊢ (W \in LMod \land X \in V) \to X \in N (\{X\})$
30	10 7 29	syl2anc	$⊢ φ \to X \in N (\{X\})$
31	28 30	sseldd	$⊢ φ \to X \in (U \underset{˙}{\oplus} N (\{X\}))$
32		nelne1	$⊢ (X \in (U \underset{˙}{\oplus} N (\{X\})) \land \neg X \in U) \to U \underset{˙}{\oplus} N (\{X\}) \neq U$
33	31 32	sylan	$⊢ (φ \land \neg X \in U) \to U \underset{˙}{\oplus} N (\{X\}) \neq U$
34	33	necomd	$⊢ (φ \land \neg X \in U) \to U \neq U \underset{˙}{\oplus} N (\{X\})$
35		df-pss	$⊢ U \subset U \underset{˙}{\oplus} N (\{X\}) \leftrightarrow (U \subseteq U \underset{˙}{\oplus} N (\{X\}) \land U \neq U \underset{˙}{\oplus} N (\{X\}))$
36	26 34 35	sylanbrc	$⊢ (φ \land \neg X \in U) \to U \subset U \underset{˙}{\oplus} N (\{X\})$
37	36	3ad2ant1	$⊢ ((φ \land \neg X \in U) \land v \in V \land U \underset{˙}{\oplus} N (\{v\}) = V) \to U \subset U \underset{˙}{\oplus} N (\{X\})$
38	8 3	lsmcl	$⊢ (W \in LMod \land U \in LSubSp (W) \land N (\{X\}) \in LSubSp (W)) \to U \underset{˙}{\oplus} N (\{X\}) \in LSubSp (W)$
39	10 19 22 38	syl3anc	$⊢ φ \to U \underset{˙}{\oplus} N (\{X\}) \in LSubSp (W)$
40	1 8	lssss	$⊢ U \underset{˙}{\oplus} N (\{X\}) \in LSubSp (W) \to U \underset{˙}{\oplus} N (\{X\}) \subseteq V$
41	39 40	syl	$⊢ φ \to U \underset{˙}{\oplus} N (\{X\}) \subseteq V$
42	41	adantr	$⊢ (φ \land U \underset{˙}{\oplus} N (\{v\}) = V) \to U \underset{˙}{\oplus} N (\{X\}) \subseteq V$
43		simpr	$⊢ (φ \land U \underset{˙}{\oplus} N (\{v\}) = V) \to U \underset{˙}{\oplus} N (\{v\}) = V$
44	42 43	sseqtrrd	$⊢ (φ \land U \underset{˙}{\oplus} N (\{v\}) = V) \to U \underset{˙}{\oplus} N (\{X\}) \subseteq U \underset{˙}{\oplus} N (\{v\})$
45	44	adantlr	$⊢ ((φ \land \neg X \in U) \land U \underset{˙}{\oplus} N (\{v\}) = V) \to U \underset{˙}{\oplus} N (\{X\}) \subseteq U \underset{˙}{\oplus} N (\{v\})$
46	45	3adant2	$⊢ ((φ \land \neg X \in U) \land v \in V \land U \underset{˙}{\oplus} N (\{v\}) = V) \to U \underset{˙}{\oplus} N (\{X\}) \subseteq U \underset{˙}{\oplus} N (\{v\})$
47	5	adantr	$⊢ (φ \land v \in V) \to W \in LVec$
48	19	adantr	$⊢ (φ \land v \in V) \to U \in LSubSp (W)$
49	39	adantr	$⊢ (φ \land v \in V) \to U \underset{˙}{\oplus} N (\{X\}) \in LSubSp (W)$
50		simpr	$⊢ (φ \land v \in V) \to v \in V$
51	1 8 2 3 47 48 49 50	lsmcv	$⊢ ((φ \land v \in V) \land U \subset U \underset{˙}{\oplus} N (\{X\}) \land U \underset{˙}{\oplus} N (\{X\}) \subseteq U \underset{˙}{\oplus} N (\{v\})) \to U \underset{˙}{\oplus} N (\{X\}) = U \underset{˙}{\oplus} N (\{v\})$
52	15 16 37 46 51	syl211anc	$⊢ ((φ \land \neg X \in U) \land v \in V \land U \underset{˙}{\oplus} N (\{v\}) = V) \to U \underset{˙}{\oplus} N (\{X\}) = U \underset{˙}{\oplus} N (\{v\})$
53		simp3	$⊢ ((φ \land \neg X \in U) \land v \in V \land U \underset{˙}{\oplus} N (\{v\}) = V) \to U \underset{˙}{\oplus} N (\{v\}) = V$
54	52 53	eqtrd	$⊢ ((φ \land \neg X \in U) \land v \in V \land U \underset{˙}{\oplus} N (\{v\}) = V) \to U \underset{˙}{\oplus} N (\{X\}) = V$
55	54	rexlimdv3a	$⊢ (φ \land \neg X \in U) \to (\exists v \in V U \underset{˙}{\oplus} N (\{v\}) = V \to U \underset{˙}{\oplus} N (\{X\}) = V)$
56	14 55	mpd	$⊢ (φ \land \neg X \in U) \to U \underset{˙}{\oplus} N (\{X\}) = V$
57	10	adantr	$⊢ (φ \land U \underset{˙}{\oplus} N (\{X\}) = V) \to W \in LMod$
58	6	adantr	$⊢ (φ \land U \underset{˙}{\oplus} N (\{X\}) = V) \to U \in H$
59	7	adantr	$⊢ (φ \land U \underset{˙}{\oplus} N (\{X\}) = V) \to X \in V$
60		simpr	$⊢ (φ \land U \underset{˙}{\oplus} N (\{X\}) = V) \to U \underset{˙}{\oplus} N (\{X\}) = V$
61	1 2 3 4 57 58 59 60	lshpnel	$⊢ (φ \land U \underset{˙}{\oplus} N (\{X\}) = V) \to \neg X \in U$
62	56 61	impbida	$⊢ φ \to (\neg X \in U \leftrightarrow U \underset{˙}{\oplus} N (\{X\}) = V)$

Metamath Proof Explorer

Theorem lshpnelb

Proof