cmtbr3N

Description: Alternate definition for the commutes relation. Lemma 3 of Kalmbach p. 23. ( cmbr3 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	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)$

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 5	cmtcomN	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \leftrightarrow Y C X)$
7	1 2 3 4 5	cmtbr2N	$⊢ (K \in OML \land Y \in B \land X \in B) \to (Y C X \leftrightarrow Y = (Y \underset{˙}{\lor} X) \underset{˙}{\land} (Y \underset{˙}{\lor} \underset{˙}{⊥} (X)))$
8	7	3com23	$⊢ (K \in OML \land X \in B \land Y \in B) \to (Y C X \leftrightarrow Y = (Y \underset{˙}{\lor} X) \underset{˙}{\land} (Y \underset{˙}{\lor} \underset{˙}{⊥} (X)))$
9	6 8	bitrd	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \leftrightarrow Y = (Y \underset{˙}{\lor} X) \underset{˙}{\land} (Y \underset{˙}{\lor} \underset{˙}{⊥} (X)))$
10		oveq2	$⊢ Y = (Y \underset{˙}{\lor} X) \underset{˙}{\land} (Y \underset{˙}{\lor} \underset{˙}{⊥} (X)) \to X \underset{˙}{\land} Y = X \underset{˙}{\land} ((Y \underset{˙}{\lor} X) \underset{˙}{\land} (Y \underset{˙}{\lor} \underset{˙}{⊥} (X)))$
11	10	adantl	$⊢ ((K \in OML \land X \in B \land Y \in B) \land Y = (Y \underset{˙}{\lor} X) \underset{˙}{\land} (Y \underset{˙}{\lor} \underset{˙}{⊥} (X))) \to X \underset{˙}{\land} Y = X \underset{˙}{\land} ((Y \underset{˙}{\lor} X) \underset{˙}{\land} (Y \underset{˙}{\lor} \underset{˙}{⊥} (X)))$
12		omlol	$⊢ K \in OML \to K \in OL$
13	12	3ad2ant1	$⊢ (K \in OML \land X \in B \land Y \in B) \to K \in OL$
14		simp2	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \in B$
15		omllat	$⊢ K \in OML \to K \in Lat$
16	15	3ad2ant1	$⊢ (K \in OML \land X \in B \land Y \in B) \to K \in Lat$
17		simp3	$⊢ (K \in OML \land X \in B \land Y \in B) \to Y \in B$
18	1 2	latjcl	$⊢ (K \in Lat \land Y \in B \land X \in B) \to Y \underset{˙}{\lor} X \in B$
19	16 17 14 18	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to Y \underset{˙}{\lor} X \in B$
20		omlop	$⊢ K \in OML \to K \in OP$
21	20	3ad2ant1	$⊢ (K \in OML \land X \in B \land Y \in B) \to K \in OP$
22	1 4	opoccl	$⊢ (K \in OP \land X \in B) \to \underset{˙}{⊥} (X) \in B$
23	21 14 22	syl2anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \in B$
24	1 2	latjcl	$⊢ (K \in Lat \land Y \in B \land \underset{˙}{⊥} (X) \in B) \to Y \underset{˙}{\lor} \underset{˙}{⊥} (X) \in B$
25	16 17 23 24	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to Y \underset{˙}{\lor} \underset{˙}{⊥} (X) \in B$
26	1 3	latmassOLD	$⊢ (K \in OL \land (X \in B \land Y \underset{˙}{\lor} X \in B \land Y \underset{˙}{\lor} \underset{˙}{⊥} (X) \in B)) \to (X \underset{˙}{\land} (Y \underset{˙}{\lor} X)) \underset{˙}{\land} (Y \underset{˙}{\lor} \underset{˙}{⊥} (X)) = X \underset{˙}{\land} ((Y \underset{˙}{\lor} X) \underset{˙}{\land} (Y \underset{˙}{\lor} \underset{˙}{⊥} (X)))$
27	13 14 19 25 26	syl13anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\land} (Y \underset{˙}{\lor} X)) \underset{˙}{\land} (Y \underset{˙}{\lor} \underset{˙}{⊥} (X)) = X \underset{˙}{\land} ((Y \underset{˙}{\lor} X) \underset{˙}{\land} (Y \underset{˙}{\lor} \underset{˙}{⊥} (X)))$
28	1 2	latjcom	$⊢ (K \in Lat \land Y \in B \land X \in B) \to Y \underset{˙}{\lor} X = X \underset{˙}{\lor} Y$
29	16 17 14 28	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to Y \underset{˙}{\lor} X = X \underset{˙}{\lor} Y$
30	29	oveq2d	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \underset{˙}{\land} (Y \underset{˙}{\lor} X) = X \underset{˙}{\land} (X \underset{˙}{\lor} Y)$
31	1 2 3	latabs2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} (X \underset{˙}{\lor} Y) = X$
32	15 31	syl3an1	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \underset{˙}{\land} (X \underset{˙}{\lor} Y) = X$
33	30 32	eqtrd	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \underset{˙}{\land} (Y \underset{˙}{\lor} X) = X$
34	1 2	latjcom	$⊢ (K \in Lat \land Y \in B \land \underset{˙}{⊥} (X) \in B) \to Y \underset{˙}{\lor} \underset{˙}{⊥} (X) = \underset{˙}{⊥} (X) \underset{˙}{\lor} Y$
35	16 17 23 34	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to Y \underset{˙}{\lor} \underset{˙}{⊥} (X) = \underset{˙}{⊥} (X) \underset{˙}{\lor} Y$
36	33 35	oveq12d	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\land} (Y \underset{˙}{\lor} X)) \underset{˙}{\land} (Y \underset{˙}{\lor} \underset{˙}{⊥} (X)) = X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)$
37	27 36	eqtr3d	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \underset{˙}{\land} ((Y \underset{˙}{\lor} X) \underset{˙}{\land} (Y \underset{˙}{\lor} \underset{˙}{⊥} (X))) = X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)$
38	37	adantr	$⊢ ((K \in OML \land X \in B \land Y \in B) \land Y = (Y \underset{˙}{\lor} X) \underset{˙}{\land} (Y \underset{˙}{\lor} \underset{˙}{⊥} (X))) \to X \underset{˙}{\land} ((Y \underset{˙}{\lor} X) \underset{˙}{\land} (Y \underset{˙}{\lor} \underset{˙}{⊥} (X))) = X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)$
39	11 38	eqtr2d	$⊢ ((K \in OML \land X \in B \land Y \in B) \land Y = (Y \underset{˙}{\lor} X) \underset{˙}{\land} (Y \underset{˙}{\lor} \underset{˙}{⊥} (X))) \to X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) = X \underset{˙}{\land} Y$
40	39	ex	$⊢ (K \in OML \land X \in B \land Y \in B) \to (Y = (Y \underset{˙}{\lor} X) \underset{˙}{\land} (Y \underset{˙}{\lor} \underset{˙}{⊥} (X)) \to X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) = X \underset{˙}{\land} Y)$
41	9 40	sylbid	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \to X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) = X \underset{˙}{\land} Y)$
42		simp1	$⊢ (K \in OML \land X \in B \land Y \in B) \to K \in OML$
43	1 4	opoccl	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
44	21 17 43	syl2anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
45	1 3	latmcl	$⊢ (K \in Lat \land X \in B \land \underset{˙}{⊥} (Y) \in B) \to X \underset{˙}{\land} \underset{˙}{⊥} (Y) \in B$
46	16 14 44 45	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \underset{˙}{\land} \underset{˙}{⊥} (Y) \in B$
47	42 46 14	3jca	$⊢ (K \in OML \land X \in B \land Y \in B) \to (K \in OML \land X \underset{˙}{\land} \underset{˙}{⊥} (Y) \in B \land X \in B)$
48		eqid	$⊢ \leq_{K} = \leq_{K}$
49	1 48 3	latmle1	$⊢ (K \in Lat \land X \in B \land \underset{˙}{⊥} (Y) \in B) \to (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \leq_{K} X$
50	16 14 44 49	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \leq_{K} X$
51	1 48 2 3 4	omllaw2N	$⊢ (K \in OML \land X \underset{˙}{\land} \underset{˙}{⊥} (Y) \in B \land X \in B) \to ((X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \leq_{K} X \to (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\lor} (\underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X) = X)$
52	47 50 51	sylc	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\lor} (\underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X) = X$
53	1 4	opoccl	$⊢ (K \in OP \land X \underset{˙}{\land} \underset{˙}{⊥} (Y) \in B) \to \underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \in B$
54	21 46 53	syl2anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \in B$
55	1 3	latmcl	$⊢ (K \in Lat \land \underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \in B \land X \in B) \to \underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X \in B$
56	16 54 14 55	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X \in B$
57	1 2	latjcom	$⊢ (K \in Lat \land X \underset{˙}{\land} \underset{˙}{⊥} (Y) \in B \land \underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X \in B) \to (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\lor} (\underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X) = (\underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X) \underset{˙}{\lor} (X \underset{˙}{\land} \underset{˙}{⊥} (Y))$
58	16 46 56 57	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\lor} (\underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X) = (\underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X) \underset{˙}{\lor} (X \underset{˙}{\land} \underset{˙}{⊥} (Y))$
59	52 58	eqtr3d	$⊢ (K \in OML \land X \in B \land Y \in B) \to X = (\underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X) \underset{˙}{\lor} (X \underset{˙}{\land} \underset{˙}{⊥} (Y))$
60	59	adantr	$⊢ ((K \in OML \land X \in B \land Y \in B) \land X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) = X \underset{˙}{\land} Y) \to X = (\underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X) \underset{˙}{\lor} (X \underset{˙}{\land} \underset{˙}{⊥} (Y))$
61	1 2 3 4	oldmm3N	$⊢ (K \in OL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) = \underset{˙}{⊥} (X) \underset{˙}{\lor} Y$
62	12 61	syl3an1	$⊢ (K \in OML \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) = \underset{˙}{⊥} (X) \underset{˙}{\lor} Y$
63	62	oveq2d	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \underset{˙}{\land} \underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) = X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y)$
64	1 3	latmcom	$⊢ (K \in Lat \land X \in B \land \underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \in B) \to X \underset{˙}{\land} \underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) = \underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X$
65	16 14 54 64	syl3anc	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \underset{˙}{\land} \underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) = \underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X$
66	63 65	eqtr3d	$⊢ (K \in OML \land X \in B \land Y \in B) \to X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) = \underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X$
67	66	eqeq1d	$⊢ (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 \underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X = X \underset{˙}{\land} Y)$
68		oveq1	$⊢ \underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X = X \underset{˙}{\land} Y \to (\underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X) \underset{˙}{\lor} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) = (X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} \underset{˙}{⊥} (Y))$
69	67 68	syl6bi	$⊢ (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 (\underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X) \underset{˙}{\lor} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) = (X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)))$
70	69	imp	$⊢ ((K \in OML \land X \in B \land Y \in B) \land X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) = X \underset{˙}{\land} Y) \to (\underset{˙}{⊥} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) \underset{˙}{\land} X) \underset{˙}{\lor} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)) = (X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} \underset{˙}{⊥} (Y))$
71	60 70	eqtrd	$⊢ ((K \in OML \land X \in B \land Y \in B) \land X \underset{˙}{\land} (\underset{˙}{⊥} (X) \underset{˙}{\lor} Y) = X \underset{˙}{\land} Y) \to X = (X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} \underset{˙}{⊥} (Y))$
72	71	ex	$⊢ (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 = (X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)))$
73	1 2 3 4 5	cmtvalN	$⊢ (K \in OML \land X \in B \land Y \in B) \to (X C Y \leftrightarrow X = (X \underset{˙}{\land} Y) \underset{˙}{\lor} (X \underset{˙}{\land} \underset{˙}{⊥} (Y)))$
74	72 73	sylibrd	$⊢ (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 C Y)$
75	41 74	impbid	$⊢ (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)$

Metamath Proof Explorer

Theorem cmtbr3N

Proof