lshpnel2N

Description: Condition that determines a hyperplane. (Contributed by NM, 3-Oct-2014) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		lshpnel2.v	$⊢ V = {Base}_{W}$
2		lshpnel2.s	$⊢ S = LSubSp (W)$
3		lshpnel2.n	$⊢ N = LSpan (W)$
4		lshpnel2.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
5		lshpnel2.h	$⊢ H = LSHyp (W)$
6		lshpnel2.w	$⊢ φ \to W \in LVec$
7		lshpnel2.u	$⊢ φ \to U \in S$
8		lshpnel2.t	$⊢ φ \to U \neq V$
9		lshpnel2.x	$⊢ φ \to X \in V$
10		lshpnel2.e	$⊢ φ \to \neg X \in U$
11	10	adantr	$⊢ (φ \land U \in H) \to \neg X \in U$
12	6	adantr	$⊢ (φ \land U \in H) \to W \in LVec$
13		simpr	$⊢ (φ \land U \in H) \to U \in H$
14	9	adantr	$⊢ (φ \land U \in H) \to X \in V$
15	1 3 4 5 12 13 14	lshpnelb	$⊢ (φ \land U \in H) \to (\neg X \in U \leftrightarrow U \underset{˙}{\oplus} N (\{X\}) = V)$
16	11 15	mpbid	$⊢ (φ \land U \in H) \to U \underset{˙}{\oplus} N (\{X\}) = V$
17	7	adantr	$⊢ (φ \land U \underset{˙}{\oplus} N (\{X\}) = V) \to U \in S$
18	8	adantr	$⊢ (φ \land U \underset{˙}{\oplus} N (\{X\}) = V) \to U \neq V$
19	9	adantr	$⊢ (φ \land U \underset{˙}{\oplus} N (\{X\}) = V) \to X \in V$
20		lveclmod	$⊢ W \in LVec \to W \in LMod$
21	6 20	syl	$⊢ φ \to W \in LMod$
22	2 3	lspid	$⊢ (W \in LMod \land U \in S) \to N (U) = U$
23	21 7 22	syl2anc	$⊢ φ \to N (U) = U$
24	23	uneq1d	$⊢ φ \to N (U) \cup N (\{X\}) = U \cup N (\{X\})$
25	24	fveq2d	$⊢ φ \to N (N (U) \cup N (\{X\})) = N (U \cup N (\{X\}))$
26	1 2	lssss	$⊢ U \in S \to U \subseteq V$
27	7 26	syl	$⊢ φ \to U \subseteq V$
28	9	snssd	$⊢ φ \to \{X\} \subseteq V$
29	1 3	lspun	$⊢ (W \in LMod \land U \subseteq V \land \{X\} \subseteq V) \to N (U \cup \{X\}) = N (N (U) \cup N (\{X\}))$
30	21 27 28 29	syl3anc	$⊢ φ \to N (U \cup \{X\}) = N (N (U) \cup N (\{X\}))$
31	1 2 3	lspsncl	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in S$
32	21 9 31	syl2anc	$⊢ φ \to N (\{X\}) \in S$
33	2 3 4	lsmsp	$⊢ (W \in LMod \land U \in S \land N (\{X\}) \in S) \to U \underset{˙}{\oplus} N (\{X\}) = N (U \cup N (\{X\}))$
34	21 7 32 33	syl3anc	$⊢ φ \to U \underset{˙}{\oplus} N (\{X\}) = N (U \cup N (\{X\}))$
35	25 30 34	3eqtr4rd	$⊢ φ \to U \underset{˙}{\oplus} N (\{X\}) = N (U \cup \{X\})$
36	35	eqeq1d	$⊢ φ \to (U \underset{˙}{\oplus} N (\{X\}) = V \leftrightarrow N (U \cup \{X\}) = V)$
37	36	biimpa	$⊢ (φ \land U \underset{˙}{\oplus} N (\{X\}) = V) \to N (U \cup \{X\}) = V$
38		sneq	$⊢ v = X \to \{v\} = \{X\}$
39	38	uneq2d	$⊢ v = X \to U \cup \{v\} = U \cup \{X\}$
40	39	fveqeq2d	$⊢ v = X \to (N (U \cup \{v\}) = V \leftrightarrow N (U \cup \{X\}) = V)$
41	40	rspcev	$⊢ (X \in V \land N (U \cup \{X\}) = V) \to \exists v \in V N (U \cup \{v\}) = V$
42	19 37 41	syl2anc	$⊢ (φ \land U \underset{˙}{\oplus} N (\{X\}) = V) \to \exists v \in V N (U \cup \{v\}) = V$
43	6	adantr	$⊢ (φ \land U \underset{˙}{\oplus} N (\{X\}) = V) \to W \in LVec$
44	1 3 2 5	islshp	$⊢ W \in LVec \to (U \in H \leftrightarrow (U \in S \land U \neq V \land \exists v \in V N (U \cup \{v\}) = V))$
45	43 44	syl	$⊢ (φ \land U \underset{˙}{\oplus} N (\{X\}) = V) \to (U \in H \leftrightarrow (U \in S \land U \neq V \land \exists v \in V N (U \cup \{v\}) = V))$
46	17 18 42 45	mpbir3and	$⊢ (φ \land U \underset{˙}{\oplus} N (\{X\}) = V) \to U \in H$
47	16 46	impbida	$⊢ φ \to (U \in H \leftrightarrow U \underset{˙}{\oplus} N (\{X\}) = V)$

Metamath Proof Explorer

Theorem lshpnel2N

Proof