Metamath Proof Explorer

Theorem cmt4N

Description: Commutation with orthocomplement. Remark in Kalmbach p. 23. ( cmcm4i analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	cmt2.b	$⊢ B = {Base}_{K}$
		cmt2.o	$⊢ \underset{˙}{⊥} = oc (K)$
		cmt2.c	$⊢ C = cm (K)$
	Assertion	cmt4N	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \leftrightarrow \underset{˙}{⊥} (X) C \underset{˙}{⊥} (Y))$

Proof

Step	Hyp	Ref	Expression
1		cmt2.b	$⊢ B = {Base}_{K}$
2		cmt2.o	$⊢ \underset{˙}{⊥} = oc (K)$
3		cmt2.c	$⊢ C = cm (K)$
4	1 2 3	cmt2N	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \leftrightarrow X C \underset{˙}{⊥} (Y))$
5		omlop	$⊢ K \in OML \to K \in OP$
6	5	3ad2ant1	$⊢ (K \in OML \land X \in B \land Y \in B) \to K \in OP$
7		simp3	$⊢ (K \in OML \land X \in B \land Y \in B) \to Y \in B$
8	1 2	opoccl	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
9	6 7 8	syl2anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
10	1 2 3	cmt3N	$⊢ (K \in OML \land X \in B \land \underset{˙}{⊥} (Y) \in B) \to (X C \underset{˙}{⊥} (Y) \leftrightarrow \underset{˙}{⊥} (X) C \underset{˙}{⊥} (Y))$
11	9 10	syld3an3	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C \underset{˙}{⊥} (Y) \leftrightarrow \underset{˙}{⊥} (X) C \underset{˙}{⊥} (Y))$
12	4 11	bitrd	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \leftrightarrow \underset{˙}{⊥} (X) C \underset{˙}{⊥} (Y))$