dochocsp

Description: The span of an orthocomplement equals the orthocomplement of the span. (Contributed by NM, 7-Aug-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	dochocsp	$⊢ φ \to \underset{˙}{⊥} (N (X)) = \underset{˙}{⊥} (X)$

Proof

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	1 2 6	dvhlmod	$⊢ φ \to U \in LMod$
9	4 5	lspssv	$⊢ (U \in LMod \land X \subseteq V) \to N (X) \subseteq V$
10	8 7 9	syl2anc	$⊢ φ \to N (X) \subseteq V$
11	4 5	lspssid	$⊢ (U \in LMod \land X \subseteq V) \to X \subseteq N (X)$
12	8 7 11	syl2anc	$⊢ φ \to X \subseteq N (X)$
13	1 2 4 3	dochss	$⊢ ((K \in HL \land W \in H) \land N (X) \subseteq V \land X \subseteq N (X)) \to \underset{˙}{⊥} (N (X)) \subseteq \underset{˙}{⊥} (X)$
14	6 10 12 13	syl3anc	$⊢ φ \to \underset{˙}{⊥} (N (X)) \subseteq \underset{˙}{⊥} (X)$
15		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
16	1 15 2 4 3	dochcl	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)$
17	6 7 16	syl2anc	$⊢ φ \to \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)$
18	1 15 3	dochoc	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) = \underset{˙}{⊥} (X)$
19	6 17 18	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) = \underset{˙}{⊥} (X)$
20	1 2 4 3	dochssv	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) \subseteq V$
21	6 7 20	syl2anc	$⊢ φ \to \underset{˙}{⊥} (X) \subseteq V$
22	1 2 4 3	dochssv	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq V$
23	6 21 22	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq V$
24	1 2 3 4 5 6 7	dochspss	$⊢ φ \to N (X) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
25	1 2 4 3	dochss	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq V \land N (X) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) \subseteq \underset{˙}{⊥} (N (X))$
26	6 23 24 25	syl3anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) \subseteq \underset{˙}{⊥} (N (X))$
27	19 26	eqsstrrd	$⊢ φ \to \underset{˙}{⊥} (X) \subseteq \underset{˙}{⊥} (N (X))$
28	14 27	eqssd	$⊢ φ \to \underset{˙}{⊥} (N (X)) = \underset{˙}{⊥} (X)$

Metamath Proof Explorer

Theorem dochocsp

Proof