dochshpsat

Description: A hyperplane is closed iff its orthocomplement is an atom. (Contributed by NM, 29-Oct-2014)

	Ref	Expression
Hypotheses	dochshpsat.h	$⊢ H = LHyp (K)$
	dochshpsat.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	dochshpsat.u	$⊢ U = DVecH (K) (W)$
	dochshpsat.a	$⊢ A = LSAtoms (U)$
	dochshpsat.y	$⊢ Y = LSHyp (U)$
	dochshpsat.k	$⊢ φ \to (K \in HL \land W \in H)$
	dochshpsat.x	$⊢ φ \to X \in Y$
Assertion	dochshpsat	$⊢ φ \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \leftrightarrow \underset{˙}{⊥} (X) \in A)$

Proof

Step	Hyp	Ref	Expression
1		dochshpsat.h	$⊢ H = LHyp (K)$
2		dochshpsat.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		dochshpsat.u	$⊢ U = DVecH (K) (W)$
4		dochshpsat.a	$⊢ A = LSAtoms (U)$
5		dochshpsat.y	$⊢ Y = LSHyp (U)$
6		dochshpsat.k	$⊢ φ \to (K \in HL \land W \in H)$
7		dochshpsat.x	$⊢ φ \to X \in Y$
8		simpr	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
9	7	adantr	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to X \in Y$
10	8 9	eqeltrd	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in Y$
11		eqid	$⊢ LSubSp (U) = LSubSp (U)$
12	1 3 6	dvhlmod	$⊢ φ \to U \in LMod$
13	11 5 12 7	lshplss	$⊢ φ \to X \in LSubSp (U)$
14		eqid	$⊢ {Base}_{U} = {Base}_{U}$
15	14 11	lssss	$⊢ X \in LSubSp (U) \to X \subseteq {Base}_{U}$
16	13 15	syl	$⊢ φ \to X \subseteq {Base}_{U}$
17	1 3 14 11 2	dochlss	$⊢ ((K \in HL \land W \in H) \land X \subseteq {Base}_{U}) \to \underset{˙}{⊥} (X) \in LSubSp (U)$
18	6 16 17	syl2anc	$⊢ φ \to \underset{˙}{⊥} (X) \in LSubSp (U)$
19	1 2 3 11 4 5 6 18	dochsatshpb	$⊢ φ \to (\underset{˙}{⊥} (X) \in A \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in Y)$
20	19	adantr	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to (\underset{˙}{⊥} (X) \in A \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in Y)$
21	10 20	mpbird	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to \underset{˙}{⊥} (X) \in A$
22		eqid	$⊢ 0_{U} = 0_{U}$
23	12	adantr	$⊢ (φ \land \underset{˙}{⊥} (X) \in A) \to U \in LMod$
24		simpr	$⊢ (φ \land \underset{˙}{⊥} (X) \in A) \to \underset{˙}{⊥} (X) \in A$
25	22 4 23 24	lsatn0	$⊢ (φ \land \underset{˙}{⊥} (X) \in A) \to \underset{˙}{⊥} (X) \neq \{0_{U}\}$
26	25	neneqd	$⊢ (φ \land \underset{˙}{⊥} (X) \in A) \to \neg \underset{˙}{⊥} (X) = \{0_{U}\}$
27	6	adantr	$⊢ (φ \land \underset{˙}{⊥} (X) \in A) \to (K \in HL \land W \in H)$
28	1 3 2 14 22	doch0	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⊥} (\{0_{U}\}) = {Base}_{U}$
29	27 28	syl	$⊢ (φ \land \underset{˙}{⊥} (X) \in A) \to \underset{˙}{⊥} (\{0_{U}\}) = {Base}_{U}$
30	29	eqeq2d	$⊢ (φ \land \underset{˙}{⊥} (X) \in A) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = \underset{˙}{⊥} (\{0_{U}\}) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = {Base}_{U})$
31		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
32	1 31 3 14 2	dochcl	$⊢ ((K \in HL \land W \in H) \land X \subseteq {Base}_{U}) \to \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)$
33	6 16 32	syl2anc	$⊢ φ \to \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)$
34	1 31 3 22	dih0rn	$⊢ (K \in HL \land W \in H) \to \{0_{U}\} \in ran DIsoH (K) (W)$
35	6 34	syl	$⊢ φ \to \{0_{U}\} \in ran DIsoH (K) (W)$
36	1 31 2 6 33 35	doch11	$⊢ φ \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = \underset{˙}{⊥} (\{0_{U}\}) \leftrightarrow \underset{˙}{⊥} (X) = \{0_{U}\})$
37	36	adantr	$⊢ (φ \land \underset{˙}{⊥} (X) \in A) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = \underset{˙}{⊥} (\{0_{U}\}) \leftrightarrow \underset{˙}{⊥} (X) = \{0_{U}\})$
38	30 37	bitr3d	$⊢ (φ \land \underset{˙}{⊥} (X) \in A) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = {Base}_{U} \leftrightarrow \underset{˙}{⊥} (X) = \{0_{U}\})$
39	26 38	mtbird	$⊢ (φ \land \underset{˙}{⊥} (X) \in A) \to \neg \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = {Base}_{U}$
40	1 2 3 14 5 6 7	dochshpncl	$⊢ φ \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq X \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = {Base}_{U})$
41	40	necon1bbid	$⊢ φ \to (\neg \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = {Base}_{U} \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X)$
42	41	adantr	$⊢ (φ \land \underset{˙}{⊥} (X) \in A) \to (\neg \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = {Base}_{U} \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X)$
43	39 42	mpbid	$⊢ (φ \land \underset{˙}{⊥} (X) \in A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
44	21 43	impbida	$⊢ φ \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \leftrightarrow \underset{˙}{⊥} (X) \in A)$

Metamath Proof Explorer

Theorem dochshpsat

Proof