ocvocv

Description: A set is contained in its double orthocomplement. (Contributed by Mario Carneiro, 13-Oct-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ocvss.v	$⊢ V = {Base}_{W}$
2		ocvss.o	$⊢ \underset{˙}{⊥} = ocv (W)$
3	1 2	ocvss	$⊢ \underset{˙}{⊥} (S) \subseteq V$
4	3	a1i	$⊢ ((W \in PreHil \land S \subseteq V) \land x \in S) \to \underset{˙}{⊥} (S) \subseteq V$
5		simpr	$⊢ (W \in PreHil \land S \subseteq V) \to S \subseteq V$
6	5	sselda	$⊢ ((W \in PreHil \land S \subseteq V) \land x \in S) \to x \in V$
7		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
8		eqid	$⊢ Scalar (W) = Scalar (W)$
9		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
10	1 7 8 9 2	ocvi	$⊢ (y \in \underset{˙}{⊥} (S) \land x \in S) \to y \cdot_{𝑖} (W) x = 0_{Scalar (W)}$
11	10	ancoms	$⊢ (x \in S \land y \in \underset{˙}{⊥} (S)) \to y \cdot_{𝑖} (W) x = 0_{Scalar (W)}$
12	11	adantll	$⊢ (((W \in PreHil \land S \subseteq V) \land x \in S) \land y \in \underset{˙}{⊥} (S)) \to y \cdot_{𝑖} (W) x = 0_{Scalar (W)}$
13		simplll	$⊢ (((W \in PreHil \land S \subseteq V) \land x \in S) \land y \in \underset{˙}{⊥} (S)) \to W \in PreHil$
14	4	sselda	$⊢ (((W \in PreHil \land S \subseteq V) \land x \in S) \land y \in \underset{˙}{⊥} (S)) \to y \in V$
15	6	adantr	$⊢ (((W \in PreHil \land S \subseteq V) \land x \in S) \land y \in \underset{˙}{⊥} (S)) \to x \in V$
16	8 7 1 9	iporthcom	$⊢ (W \in PreHil \land y \in V \land x \in V) \to (y \cdot_{𝑖} (W) x = 0_{Scalar (W)} \leftrightarrow x \cdot_{𝑖} (W) y = 0_{Scalar (W)})$
17	13 14 15 16	syl3anc	$⊢ (((W \in PreHil \land S \subseteq V) \land x \in S) \land y \in \underset{˙}{⊥} (S)) \to (y \cdot_{𝑖} (W) x = 0_{Scalar (W)} \leftrightarrow x \cdot_{𝑖} (W) y = 0_{Scalar (W)})$
18	12 17	mpbid	$⊢ (((W \in PreHil \land S \subseteq V) \land x \in S) \land y \in \underset{˙}{⊥} (S)) \to x \cdot_{𝑖} (W) y = 0_{Scalar (W)}$
19	18	ralrimiva	$⊢ ((W \in PreHil \land S \subseteq V) \land x \in S) \to \forall y \in \underset{˙}{⊥} (S) x \cdot_{𝑖} (W) y = 0_{Scalar (W)}$
20	1 7 8 9 2	elocv	$⊢ x \in \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \leftrightarrow (\underset{˙}{⊥} (S) \subseteq V \land x \in V \land \forall y \in \underset{˙}{⊥} (S) x \cdot_{𝑖} (W) y = 0_{Scalar (W)})$
21	4 6 19 20	syl3anbrc	$⊢ ((W \in PreHil \land S \subseteq V) \land x \in S) \to x \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))$
22	21	ex	$⊢ (W \in PreHil \land S \subseteq V) \to (x \in S \to x \in \underset{˙}{⊥} (\underset{˙}{⊥} (S)))$
23	22	ssrdv	$⊢ (W \in PreHil \land S \subseteq V) \to S \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S))$

Metamath Proof Explorer

Theorem ocvocv

Proof