Metamath Proof Explorer

Theorem cmtbr2N

Description: Alternate definition of the commutes relation. Remark in Kalmbach p. 23. ( cmbr2i 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 cmtbr2N ( ( 𝐾 ∈ 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 4 5 cmt4N ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( ⊥ ‘ 𝑋 ) 𝐶 ( ⊥ ‘ 𝑌 ) ) )
7 simp1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OML )
8 omlop ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OP )
9 8 3ad2ant1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OP )
10 simp2 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
11 1 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 )
12 9 10 11 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 )
13 simp3 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
14 1 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
15 9 13 14 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
16 1 2 3 4 5 cmtvalN ⊢ ( ( 𝐾 ∈ OML ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ∧ ( ⊥ ‘ 𝑌 ) ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑋 ) 𝐶 ( ⊥ ‘ 𝑌 ) ↔ ( ⊥ ‘ 𝑋 ) = ( ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ 𝑌 ) ) ∨ ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) ) ) )
17 7 12 15 16 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑋 ) 𝐶 ( ⊥ ‘ 𝑌 ) ↔ ( ⊥ ‘ 𝑋 ) = ( ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ 𝑌 ) ) ∨ ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) ) ) )
18 eqcom ⊢ ( 𝑋 = ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) ↔ ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) = 𝑋 )
19 18 a1i ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) ↔ ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) = 𝑋 ) )
20 omllat ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ Lat )
21 20 3ad2ant1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ Lat )
22 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
23 20 22 syl3an1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
24 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ∈ 𝐵 )
25 21 10 15 24 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ∈ 𝐵 )
26 1 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ∈ 𝐵 ) → ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) ∈ 𝐵 )
27 21 23 25 26 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) ∈ 𝐵 )
28 1 4 opcon3b ⊢ ( ( 𝐾 ∈ OP ∧ ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) = 𝑋 ↔ ( ⊥ ‘ 𝑋 ) = ( ⊥ ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) ) ) )
29 9 27 10 28 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) = 𝑋 ↔ ( ⊥ ‘ 𝑋 ) = ( ⊥ ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) ) ) )
30 omlol ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OL )
31 30 3ad2ant1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OL )
32 1 2 3 4 oldmm1 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ∈ 𝐵 ) → ( ⊥ ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) ) = ( ( ⊥ ‘ ( 𝑋 ∨ 𝑌 ) ) ∨ ( ⊥ ‘ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) ) )
33 31 23 25 32 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) ) = ( ( ⊥ ‘ ( 𝑋 ∨ 𝑌 ) ) ∨ ( ⊥ ‘ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) ) )
34 1 2 3 4 oldmj1 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ 𝑌 ) ) )
35 30 34 syl3an1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ 𝑌 ) ) )
36 1 2 3 4 oldmj1 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑌 ) ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) = ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) )
37 31 10 15 36 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) = ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) )
38 35 37 oveq12d ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ ( 𝑋 ∨ 𝑌 ) ) ∨ ( ⊥ ‘ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) ) = ( ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ 𝑌 ) ) ∨ ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) ) )
39 33 38 eqtrd ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) ) = ( ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ 𝑌 ) ) ∨ ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) ) )
40 39 eqeq2d ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑋 ) = ( ⊥ ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) ) ↔ ( ⊥ ‘ 𝑋 ) = ( ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ 𝑌 ) ) ∨ ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) ) ) )
41 19 29 40 3bitrrd ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑋 ) = ( ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ 𝑌 ) ) ∨ ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) ) ↔ 𝑋 = ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) ) )
42 6 17 41 3bitrd ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ 𝑋 = ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ) ) )