cmtbr2N

Description: Alternate definition of the commutes relation. Remark in Kalmbach p. 23. ( cmbr2i analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cmtbr2.b	$⊢ B = {Base}_{K}$
	cmtbr2.j	$⊢ \underset{˙}{\lor} = join (K)$
	cmtbr2.m	$⊢ \underset{˙}{\land} = meet (K)$
	cmtbr2.o	$⊢ \underset{˙}{⊥} = oc (K)$
	cmtbr2.c	$⊢ C = cm (K)$
Assertion	cmtbr2N	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \leftrightarrow X = (X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)))$

Proof

Step	Hyp	Ref	Expression
1		cmtbr2.b	$⊢ B = {Base}_{K}$
2		cmtbr2.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cmtbr2.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cmtbr2.o	$⊢ \underset{˙}{⊥} = oc (K)$
5		cmtbr2.c	$⊢ C = cm (K)$
6	1 4 5	cmt4N	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \leftrightarrow \underset{˙}{⊥} (X) C \underset{˙}{⊥} (Y))$
7		simp1	$⊢ (K \in OML \land X \in B \land Y \in B) \to K \in OML$
8		omlop	$⊢ K \in OML \to K \in OP$
9	8	3ad2ant1	$⊢ (K \in OML \land X \in B \land Y \in B) \to K \in OP$
10		simp2	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \in B$
11	1 4	opoccl	$⊢ (K \in OP \land X \in B) \to \underset{˙}{⊥} (X) \in B$
12	9 10 11	syl2anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \in B$
13		simp3	$⊢ (K \in OML \land X \in B \land Y \in B) \to Y \in B$
14	1 4	opoccl	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
15	9 13 14	syl2anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
16	1 2 3 4 5	cmtvalN	$⊢ (K \in OML \land \underset{˙}{⊥} (X) \in B \land \underset{˙}{⊥} (Y) \in B) \to (\underset{˙}{⊥} (X) C \underset{˙}{⊥} (Y) \leftrightarrow \underset{˙}{⊥} (X) = (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\lor} (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y))))$
17	7 12 15 16	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (X) C \underset{˙}{⊥} (Y) \leftrightarrow \underset{˙}{⊥} (X) = (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\lor} (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y))))$
18		eqcom	$⊢ X = (X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leftrightarrow (X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) = X$
19	18	a1i	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X = (X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \leftrightarrow (X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) = X)$
20		omllat	$⊢ K \in OML \to K \in Lat$
21	20	3ad2ant1	$⊢ (K \in OML \land X \in B \land Y \in B) \to K \in Lat$
22	1 2	latjcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
23	20 22	syl3an1	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
24	1 2	latjcl	$⊢ (K \in Lat \land X \in B \land \underset{˙}{⊥} (Y) \in B) \to X \underset{˙}{\lor} \underset{˙}{⊥} (Y) \in B$
25	21 10 15 24	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \underset{˙}{\lor} \underset{˙}{⊥} (Y) \in B$
26	1 3	latmcl	$⊢ (K \in Lat \land X \underset{˙}{\lor} Y \in B \land X \underset{˙}{\lor} \underset{˙}{⊥} (Y) \in B) \to (X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \in B$
27	21 23 25 26	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \in B$
28	1 4	opcon3b	$⊢ (K \in OP \land (X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) \in B \land X \in B) \to ((X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) = X \leftrightarrow \underset{˙}{⊥} (X) = \underset{˙}{⊥} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y))))$
29	9 27 10 28	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to ((X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) = X \leftrightarrow \underset{˙}{⊥} (X) = \underset{˙}{⊥} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y))))$
30		omlol	$⊢ K \in OML \to K \in OL$
31	30	3ad2ant1	$⊢ (K \in OML \land X \in B \land Y \in B) \to K \in OL$
32	1 2 3 4	oldmm1	$⊢ (K \in OL \land X \underset{˙}{\lor} Y \in B \land X \underset{˙}{\lor} \underset{˙}{⊥} (Y) \in B) \to \underset{˙}{⊥} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y))) = \underset{˙}{⊥} (X \underset{˙}{\lor} Y) \underset{˙}{\lor} \underset{˙}{⊥} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y))$
33	31 23 25 32	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y))) = \underset{˙}{⊥} (X \underset{˙}{\lor} Y) \underset{˙}{\lor} \underset{˙}{⊥} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y))$
34	1 2 3 4	oldmj1	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\lor} Y) = \underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y)$
35	30 34	syl3an1	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\lor} Y) = \underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y)$
36	1 2 3 4	oldmj1	$⊢ (K \in OL \land X \in B \land \underset{˙}{⊥} (Y) \in B) \to \underset{˙}{⊥} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) = \underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
37	31 10 15 36	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) = \underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
38	35 37	oveq12d	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\lor} Y) \underset{˙}{\lor} \underset{˙}{⊥} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)) = (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\lor} (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y)))$
39	33 38	eqtrd	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y))) = (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\lor} (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y)))$
40	39	eqeq2d	$⊢ (K \in OML \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (X) = \underset{˙}{⊥} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y))) \leftrightarrow \underset{˙}{⊥} (X) = (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\lor} (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y))))$
41	19 29 40	3bitrrd	$⊢ (K \in OML \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (X) = (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\lor} (\underset{˙}{⊥} (X) \underset{˙}{\land} \underset{˙}{⊥} (\underset{˙}{⊥} (Y))) \leftrightarrow X = (X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)))$
42	6 17 41	3bitrd	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \leftrightarrow X = (X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} \underset{˙}{⊥} (Y)))$

Metamath Proof Explorer

Theorem cmtbr2N

Proof