dochspss

Description: The span of a set of vectors is included in their double orthocomplement. (Contributed by NM, 26-Jul-2014)

	Ref	Expression
Hypotheses	dochsp.h	$⊢ H = LHyp (K)$
	dochsp.u	$⊢ U = DVecH (K) (W)$
	dochsp.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	dochsp.v	$⊢ V = {Base}_{U}$
	dochsp.n	$⊢ N = LSpan (U)$
	dochsp.k	$⊢ φ \to (K \in HL \land W \in H)$
	dochsp.x	$⊢ φ \to X \subseteq V$
Assertion	dochspss	$⊢ φ \to N (X) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))$

Step	Hyp	Ref	Expression
1		dochsp.h	$⊢ H = LHyp (K)$
2		dochsp.u	$⊢ U = DVecH (K) (W)$
3		dochsp.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
4		dochsp.v	$⊢ V = {Base}_{U}$
5		dochsp.n	$⊢ N = LSpan (U)$
6		dochsp.k	$⊢ φ \to (K \in HL \land W \in H)$
7		dochsp.x	$⊢ φ \to X \subseteq V$
8		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
9		eqid	$⊢ LSubSp (U) = LSubSp (U)$
10	1 2 8 9	dihsslss	$⊢ (K \in HL \land W \in H) \to ran DIsoH (K) (W) \subseteq LSubSp (U)$
11		rabss2	$⊢ ran DIsoH (K) (W) \subseteq LSubSp (U) \to \{z \in ran DIsoH (K) (W) \| X \subseteq z\} \subseteq \{z \in LSubSp (U) \| X \subseteq z\}$
12		intss	$⊢ \{z \in ran DIsoH (K) (W) \| X \subseteq z\} \subseteq \{z \in LSubSp (U) \| X \subseteq z\} \to ⋂ \{z \in LSubSp (U) \| X \subseteq z\} \subseteq ⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\}$
13	6 10 11 12	4syl	$⊢ φ \to ⋂ \{z \in LSubSp (U) \| X \subseteq z\} \subseteq ⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\}$
14	1 2 6	dvhlmod	$⊢ φ \to U \in LMod$
15	4 9 5	lspval	$⊢ (U \in LMod \land X \subseteq V) \to N (X) = ⋂ \{z \in LSubSp (U) \| X \subseteq z\}$
16	14 7 15	syl2anc	$⊢ φ \to N (X) = ⋂ \{z \in LSubSp (U) \| X \subseteq z\}$
17	1 8 2 4 3 6 7	doch2val2	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = ⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\}$
18	13 16 17	3sstr4d	$⊢ φ \to N (X) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))$

Metamath Proof Explorer