opoccl

Description: Closure of orthocomplement operation. ( choccl analog.) (Contributed by NM, 20-Oct-2011)

	Ref	Expression
Hypotheses	opoccl.b	$⊢ B = {Base}_{K}$
	opoccl.o	$⊢ \underset{˙}{⊥} = oc (K)$
Assertion	opoccl	$⊢ (K \in OP \land X \in B) \to \underset{˙}{⊥} (X) \in B$

Step	Hyp	Ref	Expression
1		opoccl.b	$⊢ B = {Base}_{K}$
2		opoccl.o	$⊢ \underset{˙}{⊥} = oc (K)$
3		eqid	$⊢ \leq_{K} = \leq_{K}$
4		eqid	$⊢ join (K) = join (K)$
5		eqid	$⊢ meet (K) = meet (K)$
6		eqid	$⊢ 0. (K) = 0. (K)$
7		eqid	$⊢ 1. (K) = 1. (K)$
8	1 3 2 4 5 6 7	oposlem	$⊢ (K \in OP \land X \in B \land X \in B) \to ((\underset{˙}{⊥} (X) \in B \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land (X \leq_{K} X \to \underset{˙}{⊥} (X) \leq_{K} \underset{˙}{⊥} (X))) \land X join (K) \underset{˙}{⊥} (X) = 1. (K) \land X meet (K) \underset{˙}{⊥} (X) = 0. (K))$
9	8	3anidm23	$⊢ (K \in OP \land X \in B) \to ((\underset{˙}{⊥} (X) \in B \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land (X \leq_{K} X \to \underset{˙}{⊥} (X) \leq_{K} \underset{˙}{⊥} (X))) \land X join (K) \underset{˙}{⊥} (X) = 1. (K) \land X meet (K) \underset{˙}{⊥} (X) = 0. (K))$
10	9	simp1d	$⊢ (K \in OP \land X \in B) \to (\underset{˙}{⊥} (X) \in B \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land (X \leq_{K} X \to \underset{˙}{⊥} (X) \leq_{K} \underset{˙}{⊥} (X)))$
11	10	simp1d	$⊢ (K \in OP \land X \in B) \to \underset{˙}{⊥} (X) \in B$

Metamath Proof Explorer