Metamath Proof Explorer

Theorem cmt3N

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	cmt3N	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \leftrightarrow \underset{˙}{⊥} (X) C 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 Y \in B \land X \in B) \to (Y C X \leftrightarrow Y C \underset{˙}{⊥} (X))$
5	4	3com23	$⊢ (K \in OML \land X \in B \land Y \in B) \to (Y C X \leftrightarrow Y C \underset{˙}{⊥} (X))$
6	1 3	cmtcomN	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \leftrightarrow Y C X)$
7		omlop	$⊢ K \in OML \to K \in OP$
8	7	3ad2ant1	$⊢ (K \in OML \land X \in B \land Y \in B) \to K \in OP$
9		simp2	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \in B$
10	1 2	opoccl	$⊢ (K \in OP \land X \in B) \to \underset{˙}{⊥} (X) \in B$
11	8 9 10	syl2anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \in B$
12	1 3	cmtcomN	$⊢ (K \in OML \land \underset{˙}{⊥} (X) \in B \land Y \in B) \to (\underset{˙}{⊥} (X) C Y \leftrightarrow Y C \underset{˙}{⊥} (X))$
13	11 12	syld3an2	$⊢ (K \in OML \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (X) C Y \leftrightarrow Y C \underset{˙}{⊥} (X))$
14	5 6 13	3bitr4d	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \leftrightarrow \underset{˙}{⊥} (X) C Y)$