dochshpncl

Description: If a hyperplane is not closed, its closure equals the vector space. (Contributed by NM, 29-Oct-2014)

	Ref	Expression
Hypotheses	dochshpncl.h	$⊢ H = LHyp (K)$
	dochshpncl.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	dochshpncl.u	$⊢ U = DVecH (K) (W)$
	dochshpncl.v	$⊢ V = {Base}_{U}$
	dochshpncl.y	$⊢ Y = LSHyp (U)$
	dochshpncl.k	$⊢ φ \to (K \in HL \land W \in H)$
	dochshpncl.x	$⊢ φ \to X \in Y$
Assertion	dochshpncl	$⊢ φ \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = V)$

Proof

Step	Hyp	Ref	Expression
1		dochshpncl.h	$⊢ H = LHyp (K)$
2		dochshpncl.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		dochshpncl.u	$⊢ U = DVecH (K) (W)$
4		dochshpncl.v	$⊢ V = {Base}_{U}$
5		dochshpncl.y	$⊢ Y = LSHyp (U)$
6		dochshpncl.k	$⊢ φ \to (K \in HL \land W \in H)$
7		dochshpncl.x	$⊢ φ \to X \in Y$
8		eqid	$⊢ LSpan (U) = LSpan (U)$
9		eqid	$⊢ LSubSp (U) = LSubSp (U)$
10		eqid	$⊢ LSSum (U) = LSSum (U)$
11	1 3 6	dvhlmod	$⊢ φ \to U \in LMod$
12	4 8 9 10 5 11	islshpsm	$⊢ φ \to (X \in Y \leftrightarrow (X \in LSubSp (U) \land X \neq V \land \exists v \in V X LSSum (U) LSpan (U) (\{v\}) = V))$
13	7 12	mpbid	$⊢ φ \to (X \in LSubSp (U) \land X \neq V \land \exists v \in V X LSSum (U) LSpan (U) (\{v\}) = V)$
14	13	simp3d	$⊢ φ \to \exists v \in V X LSSum (U) LSpan (U) (\{v\}) = V$
15	14	adantr	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X) \to \exists v \in V X LSSum (U) LSpan (U) (\{v\}) = V$
16		id	$⊢ (φ \land v \in V) \to (φ \land v \in V)$
17	16	adantlr	$⊢ ((φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X) \land v \in V) \to (φ \land v \in V)$
18	17	3adant3	$⊢ ((φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X) \land v \in V \land X LSSum (U) LSpan (U) (\{v\}) = V) \to (φ \land v \in V)$
19	9 5 11 7	lshplss	$⊢ φ \to X \in LSubSp (U)$
20	4 9	lssss	$⊢ X \in LSubSp (U) \to X \subseteq V$
21	19 20	syl	$⊢ φ \to X \subseteq V$
22	1 3 4 2	dochocss	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to X \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
23	6 21 22	syl2anc	$⊢ φ \to X \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
24	23	adantr	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X) \to X \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
25	24	3ad2ant1	$⊢ ((φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X) \land v \in V \land X LSSum (U) LSpan (U) (\{v\}) = V) \to X \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
26		simp1r	$⊢ ((φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X) \land v \in V \land X LSSum (U) LSpan (U) (\{v\}) = V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X$
27	26	necomd	$⊢ ((φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X) \land v \in V \land X LSSum (U) LSpan (U) (\{v\}) = V) \to X \neq \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
28		df-pss	$⊢ X \subset \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \leftrightarrow (X \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \land X \neq \underset{˙}{⊥} (\underset{˙}{⊥} (X)))$
29	25 27 28	sylanbrc	$⊢ ((φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X) \land v \in V \land X LSSum (U) LSpan (U) (\{v\}) = V) \to X \subset \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
30	1 3 4 2	dochssv	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) \subseteq V$
31	6 21 30	syl2anc	$⊢ φ \to \underset{˙}{⊥} (X) \subseteq V$
32	1 3 4 2	dochssv	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq V$
33	6 31 32	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq V$
34	33	adantr	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq V$
35	34	3ad2ant1	$⊢ ((φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X) \land v \in V \land X LSSum (U) LSpan (U) (\{v\}) = V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq V$
36		simp3	$⊢ ((φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X) \land v \in V \land X LSSum (U) LSpan (U) (\{v\}) = V) \to X LSSum (U) LSpan (U) (\{v\}) = V$
37	35 36	sseqtrrd	$⊢ ((φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X) \land v \in V \land X LSSum (U) LSpan (U) (\{v\}) = V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq X LSSum (U) LSpan (U) (\{v\})$
38	6	adantr	$⊢ (φ \land v \in V) \to (K \in HL \land W \in H)$
39	1 3 38	dvhlvec	$⊢ (φ \land v \in V) \to U \in LVec$
40	19	adantr	$⊢ (φ \land v \in V) \to X \in LSubSp (U)$
41	1 3 4 9 2	dochlss	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in LSubSp (U)$
42	6 31 41	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in LSubSp (U)$
43	42	adantr	$⊢ (φ \land v \in V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in LSubSp (U)$
44		simpr	$⊢ (φ \land v \in V) \to v \in V$
45	4 9 8 10 39 40 43 44	lsmcv	$⊢ ((φ \land v \in V) \land X \subset \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq X LSSum (U) LSpan (U) (\{v\})) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X LSSum (U) LSpan (U) (\{v\})$
46	18 29 37 45	syl3anc	$⊢ ((φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X) \land v \in V \land X LSSum (U) LSpan (U) (\{v\}) = V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X LSSum (U) LSpan (U) (\{v\})$
47	46 36	eqtrd	$⊢ ((φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X) \land v \in V \land X LSSum (U) LSpan (U) (\{v\}) = V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = V$
48	47	rexlimdv3a	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X) \to (\exists v \in V X LSSum (U) LSpan (U) (\{v\}) = V \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = V)$
49	15 48	mpd	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = V$
50		simpr	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = V$
51	4 5 11 7	lshpne	$⊢ φ \to X \neq V$
52	51	adantr	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = V) \to X \neq V$
53	52	necomd	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = V) \to V \neq X$
54	50 53	eqnetrd	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X$
55	49 54	impbida	$⊢ φ \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = V)$

Metamath Proof Explorer

Theorem dochshpncl

Proof