ocvlsp

Description: The orthocomplement of a linear span. (Contributed by Mario Carneiro, 23-Oct-2015)

	Ref	Expression
Hypotheses	ocvlsp.v	$⊢ V = {Base}_{W}$
	ocvlsp.o	$⊢ \underset{˙}{⊥} = ocv (W)$
	ocvlsp.n	$⊢ N = LSpan (W)$
Assertion	ocvlsp	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (N (S)) = \underset{˙}{⊥} (S)$

Proof

Step	Hyp	Ref	Expression
1		ocvlsp.v	$⊢ V = {Base}_{W}$
2		ocvlsp.o	$⊢ \underset{˙}{⊥} = ocv (W)$
3		ocvlsp.n	$⊢ N = LSpan (W)$
4		phllmod	$⊢ W \in PreHil \to W \in LMod$
5	1 3	lspssid	$⊢ (W \in LMod \land S \subseteq V) \to S \subseteq N (S)$
6	4 5	sylan	$⊢ (W \in PreHil \land S \subseteq V) \to S \subseteq N (S)$
7	2	ocv2ss	$⊢ S \subseteq N (S) \to \underset{˙}{⊥} (N (S)) \subseteq \underset{˙}{⊥} (S)$
8	6 7	syl	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (N (S)) \subseteq \underset{˙}{⊥} (S)$
9	1 2	ocvss	$⊢ \underset{˙}{⊥} (S) \subseteq V$
10	9	a1i	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (S) \subseteq V$
11	1 2	ocvocv	$⊢ (W \in PreHil \land \underset{˙}{⊥} (S) \subseteq V) \to \underset{˙}{⊥} (S) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (S)))$
12	10 11	syldan	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (S) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (S)))$
13	4	adantr	$⊢ (W \in PreHil \land S \subseteq V) \to W \in LMod$
14		eqid	$⊢ LSubSp (W) = LSubSp (W)$
15	1 2 14	ocvlss	$⊢ (W \in PreHil \land \underset{˙}{⊥} (S) \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \in LSubSp (W)$
16	10 15	syldan	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \in LSubSp (W)$
17	1 2	ocvocv	$⊢ (W \in PreHil \land S \subseteq V) \to S \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S))$
18	14 3	lspssp	$⊢ (W \in LMod \land \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \in LSubSp (W) \land S \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to N (S) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S))$
19	13 16 17 18	syl3anc	$⊢ (W \in PreHil \land S \subseteq V) \to N (S) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S))$
20	2	ocv2ss	$⊢ N (S) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (S))) \subseteq \underset{˙}{⊥} (N (S))$
21	19 20	syl	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (S))) \subseteq \underset{˙}{⊥} (N (S))$
22	12 21	sstrd	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (S) \subseteq \underset{˙}{⊥} (N (S))$
23	8 22	eqssd	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (N (S)) = \underset{˙}{⊥} (S)$

Metamath Proof Explorer

Theorem ocvlsp

Proof