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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 cmtbr2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cmtbr2.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cmtbr2.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cmtbr2.o ⊢ ⊥ = ( oc ‘ 𝐾 )
5 cmtbr2.c ⊢ 𝐶 = ( cm ‘ 𝐾 )
6 1 5 cmtcomN ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ 𝑌 𝐶 𝑋 ) )
7 1 2 3 4 5 cmtbr2N ⊢ ( ( 𝐾 ∈ OML ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 𝐶 𝑋 ↔ 𝑌 = ( ( 𝑌 ∨ 𝑋 ) ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ) ) )
8 7 3com23 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 𝐶 𝑋 ↔ 𝑌 = ( ( 𝑌 ∨ 𝑋 ) ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ) ) )
9 6 8 bitrd ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ 𝑌 = ( ( 𝑌 ∨ 𝑋 ) ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ) ) )
10 oveq2 ⊢ ( 𝑌 = ( ( 𝑌 ∨ 𝑋 ) ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( ( 𝑌 ∨ 𝑋 ) ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ) ) )
11 10 adantl ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 = ( ( 𝑌 ∨ 𝑋 ) ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ) ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ ( ( 𝑌 ∨ 𝑋 ) ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ) ) )
12 omlol ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OL )
13 12 3ad2ant1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OL )
14 simp2 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
15 omllat ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ Lat )
16 15 3ad2ant1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ Lat )
17 simp3 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
18 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 ∨ 𝑋 ) ∈ 𝐵 )
19 16 17 14 18 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ∨ 𝑋 ) ∈ 𝐵 )
20 omlop ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OP )
21 20 3ad2ant1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OP )
22 1 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 )
23 21 14 22 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 )
24 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ) → ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ∈ 𝐵 )
25 16 17 23 24 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ∈ 𝐵 )
26 1 3 latmassOLD ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑌 ∨ 𝑋 ) ∈ 𝐵 ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ∈ 𝐵 ) ) → ( ( 𝑋 ∧ ( 𝑌 ∨ 𝑋 ) ) ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ) = ( 𝑋 ∧ ( ( 𝑌 ∨ 𝑋 ) ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ) ) )
27 13 14 19 25 26 syl13anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ ( 𝑌 ∨ 𝑋 ) ) ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ) = ( 𝑋 ∧ ( ( 𝑌 ∨ 𝑋 ) ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ) ) )
28 1 2 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 ∨ 𝑋 ) = ( 𝑋 ∨ 𝑌 ) )
29 16 17 14 28 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ∨ 𝑋 ) = ( 𝑋 ∨ 𝑌 ) )
30 29 oveq2d ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ ( 𝑌 ∨ 𝑋 ) ) = ( 𝑋 ∧ ( 𝑋 ∨ 𝑌 ) ) )
31 1 2 3 latabs2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ ( 𝑋 ∨ 𝑌 ) ) = 𝑋 )
32 15 31 syl3an1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ ( 𝑋 ∨ 𝑌 ) ) = 𝑋 )
33 30 32 eqtrd ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ ( 𝑌 ∨ 𝑋 ) ) = 𝑋 )
34 1 2 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ) → ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) = ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) )
35 16 17 23 34 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) = ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) )
36 33 35 oveq12d ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ ( 𝑌 ∨ 𝑋 ) ) ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ) = ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) )
37 27 36 eqtr3d ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ ( ( 𝑌 ∨ 𝑋 ) ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ) ) = ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) )
38 37 adantr ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 = ( ( 𝑌 ∨ 𝑋 ) ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ) ) → ( 𝑋 ∧ ( ( 𝑌 ∨ 𝑋 ) ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ) ) = ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) )
39 11 38 eqtr2d ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 = ( ( 𝑌 ∨ 𝑋 ) ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ) ) → ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) )
40 39 ex ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 = ( ( 𝑌 ∨ 𝑋 ) ∧ ( 𝑌 ∨ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) ) )
41 9 40 sylbid ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 → ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) ) )
42 simp1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OML )
43 1 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
44 21 17 43 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
45 1 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ∈ 𝐵 )
46 16 14 44 45 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ∈ 𝐵 )
47 42 46 14 3jca ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐾 ∈ OML ∧ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
48 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
49 1 48 3 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ( le ‘ 𝐾 ) 𝑋 )
50 16 14 44 49 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ( le ‘ 𝐾 ) 𝑋 )
51 1 48 2 3 4 omllaw2N ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ( le ‘ 𝐾 ) 𝑋 → ( ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ∨ ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) ) = 𝑋 ) )
52 47 50 51 sylc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ∨ ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) ) = 𝑋 )
53 1 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∈ 𝐵 )
54 21 46 53 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∈ 𝐵 )
55 1 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) ∈ 𝐵 )
56 16 54 14 55 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) ∈ 𝐵 )
57 1 2 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ∈ 𝐵 ∧ ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) ∈ 𝐵 ) → ( ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ∨ ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) ) = ( ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) )
58 16 46 56 57 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ∨ ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) ) = ( ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) )
59 52 58 eqtr3d ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 = ( ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) )
60 59 adantr ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) ) → 𝑋 = ( ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) )
61 1 2 3 4 oldmm3N ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) = ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) )
62 12 61 syl3an1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) = ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) )
63 62 oveq2d ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ) = ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) )
64 1 3 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∈ 𝐵 ) → ( 𝑋 ∧ ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ) = ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) )
65 16 14 54 64 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ) = ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) )
66 63 65 eqtr3d ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) )
67 66 eqeq1d ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) ↔ ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) = ( 𝑋 ∧ 𝑌 ) ) )
68 oveq1 ⊢ ( ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) = ( 𝑋 ∧ 𝑌 ) → ( ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) )
69 67 68 biimtrdi ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) → ( ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ) )
70 69 imp ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) ) → ( ( ( ⊥ ‘ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ∧ 𝑋 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) )
71 60 70 eqtrd ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) ) → 𝑋 = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) )
72 71 ex ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) → 𝑋 = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ) )
73 1 2 3 4 5 cmtvalN ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ 𝑋 = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ) )
74 72 73 sylibrd ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) → 𝑋 𝐶 𝑌 ) )
75 41 74 impbid ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 ∧ ( ( ⊥ ‘ 𝑋 ) ∨ 𝑌 ) ) = ( 𝑋 ∧ 𝑌 ) ) )