ocv1

Description: The orthocomplement of the base set. (Contributed by Mario Carneiro, 23-Oct-2015)

	Ref	Expression
Hypotheses	ocvz.v	$⊢ V = {Base}_{W}$
	ocvz.o	$⊢ \underset{˙}{⊥} = ocv (W)$
	ocvz.z	$⊢ \underset{˙}{0} = 0_{W}$
Assertion	ocv1	$⊢ W \in PreHil \to \underset{˙}{⊥} (V) = \{\underset{˙}{0}\}$

Step	Hyp	Ref	Expression
1		ocvz.v	$⊢ V = {Base}_{W}$
2		ocvz.o	$⊢ \underset{˙}{⊥} = ocv (W)$
3		ocvz.z	$⊢ \underset{˙}{0} = 0_{W}$
4	1 2	ocvss	$⊢ \underset{˙}{⊥} (V) \subseteq V$
5		sseqin2	$⊢ \underset{˙}{⊥} (V) \subseteq V \leftrightarrow V \cap \underset{˙}{⊥} (V) = \underset{˙}{⊥} (V)$
6	4 5	mpbi	$⊢ V \cap \underset{˙}{⊥} (V) = \underset{˙}{⊥} (V)$
7		phllmod	$⊢ W \in PreHil \to W \in LMod$
8		eqid	$⊢ LSubSp (W) = LSubSp (W)$
9	1 8	lss1	$⊢ W \in LMod \to V \in LSubSp (W)$
10	7 9	syl	$⊢ W \in PreHil \to V \in LSubSp (W)$
11	2 8 3	ocvin	$⊢ (W \in PreHil \land V \in LSubSp (W)) \to V \cap \underset{˙}{⊥} (V) = \{\underset{˙}{0}\}$
12	10 11	mpdan	$⊢ W \in PreHil \to V \cap \underset{˙}{⊥} (V) = \{\underset{˙}{0}\}$
13	6 12	eqtr3id	$⊢ W \in PreHil \to \underset{˙}{⊥} (V) = \{\underset{˙}{0}\}$

Metamath Proof Explorer