Theorem 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	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cmtbr4.l	⊢ ≤ = ( le ‘ 𝐾 )
	cmtbr4.j	⊢ ∨ = ( join ‘ 𝐾 )
	cmtbr4.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cmtbr4.o	⊢ ⊥ = ( oc ‘ 𝐾 )
	cmtbr4.c	⊢ 𝐶 = ( cm ‘ 𝐾 )
Assertion	cmtbr4N	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		cmtbr4.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cmtbr4.l	⊢ ≤ = ( le ‘ 𝐾 )
3		cmtbr4.j	⊢ ∨ = ( join ‘ 𝐾 )
4		cmtbr4.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		cmtbr4.o	⊢ ⊥ = ( oc ‘ 𝐾 )
6		cmtbr4.c	⊢ 𝐶 = ( cm ‘ 𝐾 )
7	1 3 4 5 6	cmtbr3N	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) ) )
8		omllat	⊢ ( 𝐾 ∈ OML → 𝐾 ∈ Lat )
9	1 2 4	latmle2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 )
10	8 9	syl3an1	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 )
11		breq1	⊢ ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) → ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑌 ↔ ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 ) )
12	10 11	syl5ibrcom	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) → ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑌 ) )
13	8	3ad2ant1	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ Lat )
14		simp2	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
15		omlop	⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OP )
16	15	3ad2ant1	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OP )
17	1 5	opoccl	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 )
18	16 14 17	syl2anc	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 )
19		simp3	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
20	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ∈ 𝐵 )
21	13 18 19 20	syl3anc	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ∈ 𝐵 )
22	1 2 4	latmle1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑋 )
23	13 14 21 22	syl3anc	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑋 )
24	23	anim1i	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑌 ) → ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑋 ∧ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑌 ) )
25	24	ex	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑌 → ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑋 ∧ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑌 ) ) )
26	1 4	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ∈ 𝐵 )
27	13 14 21 26	syl3anc	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ∈ 𝐵 )
28	1 2 4	latlem12	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑋 ∧ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑌 ) ↔ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ ( 𝑋 ∧ 𝑌 ) ) )
29	13 27 14 19 28	syl13anc	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑋 ∧ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑌 ) ↔ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ ( 𝑋 ∧ 𝑌 ) ) )
30	25 29	sylibd	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑌 → ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ ( 𝑋 ∧ 𝑌 ) ) )
31	1 2 3	latlej2	⊢ ( ( 𝐾 ∈ Lat ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ≤ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) )
32	13 18 19 31	syl3anc	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ≤ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) )
33	1 2 4	latmlem2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑌 ∈ 𝐵 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑌 ≤ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) → ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ) )
34	13 19 21 14 33	syl13anc	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ≤ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) → ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ) )
35	32 34	mpd	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) )
36	30 35	jctird	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑌 → ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ ( 𝑋 ∧ 𝑌 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ) ) )
37	1 4	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
38	8 37	syl3an1	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
39	1 2	latasymb	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ) → ( ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ ( 𝑋 ∧ 𝑌 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ) ↔ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) ) )
40	13 27 38 39	syl3anc	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ ( 𝑋 ∧ 𝑌 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ) ↔ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) ) )
41	36 40	sylibd	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑌 → ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) ) )
42	12 41	impbid	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) ↔ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑌 ) )
43	7 42	bitrd	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑌 ) )