cmtbr4N

Description: Alternate definition for the commutes relation. ( cmbr4i analog.) (Contributed by NM, 10-Nov-2011) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cmtbr4.b	$⊢ B = {Base}_{K}$
2		cmtbr4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cmtbr4.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cmtbr4.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cmtbr4.o	$⊢ \underset{˙}{⊥} = oc (K)$
6		cmtbr4.c	$⊢ C = cm (K)$
7	1 3 4 5 6	cmtbr3N	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \leftrightarrow X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) = X \underset{˙}{\land} Y)$
8		omllat	$⊢ K \in OML \to K \in Lat$
9	1 2 4	latmle2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y$
10	8 9	syl3an1	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y$
11		breq1	$⊢ X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) = X \underset{˙}{\land} Y \to ((X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} Y \leftrightarrow (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y)$
12	10 11	syl5ibrcom	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) = X \underset{˙}{\land} Y \to (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} Y)$
13	8	3ad2ant1	$⊢ (K \in OML \land X \in B \land Y \in B) \to K \in Lat$
14		simp2	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \in B$
15		omlop	$⊢ K \in OML \to K \in OP$
16	15	3ad2ant1	$⊢ (K \in OML \land X \in B \land Y \in B) \to K \in OP$
17	1 5	opoccl	$⊢ (K \in OP \land X \in B) \to \underset{˙}{⊥} (X) \in B$
18	16 14 17	syl2anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \in B$
19		simp3	$⊢ (K \in OML \land X \in B \land Y \in B) \to Y \in B$
20	1 3	latjcl	$⊢ (K \in Lat \land \underset{˙}{⊥} (X) \in B \land Y \in B) \to \underset{˙}{⊥} (X) \underset{˙}{\lor} Y \in B$
21	13 18 19 20	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \underset{˙}{\lor} Y \in B$
22	1 2 4	latmle1	$⊢ (K \in Lat \land X \in B \land \underset{˙}{⊥} (X) \underset{˙}{\lor} Y \in B) \to (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} X$
23	13 14 21 22	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} X$
24	23	anim1i	$⊢ ((K \in OML \land X \in B \land Y \in B) \land (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} Y) \to ((X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} X \land (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} Y)$
25	24	ex	$⊢ (K \in OML \land X \in B \land Y \in B) \to ((X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} Y \to ((X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} X \land (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} Y))$
26	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land \underset{˙}{⊥} (X) \underset{˙}{\lor} Y \in B) \to X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) \in B$
27	13 14 21 26	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) \in B$
28	1 2 4	latlem12	$⊢ (K \in Lat \land (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) \in B \land X \in B \land Y \in B)) \to (((X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} X \land (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} Y) \leftrightarrow (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
29	13 27 14 19 28	syl13anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to (((X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} X \land (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} Y) \leftrightarrow (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
30	25 29	sylibd	$⊢ (K \in OML \land X \in B \land Y \in B) \to ((X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} Y \to (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
31	1 2 3	latlej2	$⊢ (K \in Lat \land \underset{˙}{⊥} (X) \in B \land Y \in B) \to Y \underset{˙}{\leq} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)$
32	13 18 19 31	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to Y \underset{˙}{\leq} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)$
33	1 2 4	latmlem2	$⊢ (K \in Lat \land (Y \in B \land \underset{˙}{⊥} (X) \underset{˙}{\lor} Y \in B \land X \in B)) \to (Y \underset{˙}{\leq} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)))$
34	13 19 21 14 33	syl13anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to (Y \underset{˙}{\leq} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)))$
35	32 34	mpd	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y))$
36	30 35	jctird	$⊢ (K \in OML \land X \in B \land Y \in B) \to ((X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} Y \to ((X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} (X \underset{˙}{\land} Y) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y))))$
37	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
38	8 37	syl3an1	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
39	1 2	latasymb	$⊢ (K \in Lat \land X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) \in B \land X \underset{˙}{\land} Y \in B) \to (((X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} (X \underset{˙}{\land} Y) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y))) \leftrightarrow X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) = X \underset{˙}{\land} Y)$
40	13 27 38 39	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to (((X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} (X \underset{˙}{\land} Y) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y))) \leftrightarrow X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) = X \underset{˙}{\land} Y)$
41	36 40	sylibd	$⊢ (K \in OML \land X \in B \land Y \in B) \to ((X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} Y \to X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) = X \underset{˙}{\land} Y)$
42	12 41	impbid	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) = X \underset{˙}{\land} Y \leftrightarrow (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} Y)$
43	7 42	bitrd	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \leftrightarrow (X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)) \underset{˙}{\leq} Y)$

Metamath Proof Explorer

Theorem cmtbr4N

Proof