This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) ≤ 𝑌 ) )