dochn0nv

Description: An orthocomplement is nonzero iff the double orthocomplement is not the whole vector space. (Contributed by NM, 1-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		dochn0nv.h	$⊢ H = LHyp (K)$
2		dochn0nv.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		dochn0nv.u	$⊢ U = DVecH (K) (W)$
4		dochn0nv.v	$⊢ V = {Base}_{U}$
5		dochn0nv.z	$⊢ \underset{˙}{0} = 0_{U}$
6		dochn0nv.k	$⊢ φ \to (K \in HL \land W \in H)$
7		dochn0nv.x	$⊢ φ \to X \subseteq V$
8		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
9	1 8 3 4 2	dochcl	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)$
10	6 7 9	syl2anc	$⊢ φ \to \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)$
11	1 8 2	dochoc	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) = \underset{˙}{⊥} (X)$
12	6 10 11	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) = \underset{˙}{⊥} (X)$
13	1 3 2 4 5	doch1	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⊥} (V) = \{\underset{˙}{0}\}$
14	6 13	syl	$⊢ φ \to \underset{˙}{⊥} (V) = \{\underset{˙}{0}\}$
15	12 14	eqeq12d	$⊢ φ \to (\underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) = \underset{˙}{⊥} (V) \leftrightarrow \underset{˙}{⊥} (X) = \{\underset{˙}{0}\})$
16	1 3 4 2	dochssv	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) \subseteq V$
17	6 7 16	syl2anc	$⊢ φ \to \underset{˙}{⊥} (X) \subseteq V$
18	1 8 3 4 2	dochcl	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in ran DIsoH (K) (W)$
19	6 17 18	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in ran DIsoH (K) (W)$
20	1 8 3 4	dih1rn	$⊢ (K \in HL \land W \in H) \to V \in ran DIsoH (K) (W)$
21	6 20	syl	$⊢ φ \to V \in ran DIsoH (K) (W)$
22	1 8 2 6 19 21	doch11	$⊢ φ \to (\underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) = \underset{˙}{⊥} (V) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = V)$
23	15 22	bitr3d	$⊢ φ \to (\underset{˙}{⊥} (X) = \{\underset{˙}{0}\} \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = V)$
24	23	necon3bid	$⊢ φ \to (\underset{˙}{⊥} (X) \neq \{\underset{˙}{0}\} \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \neq V)$

Metamath Proof Explorer

Theorem dochn0nv

Proof