Metamath Proof Explorer

Theorem omllaw4

Description: Orthomodular law equivalent. Remark in Holland95 p. 223. (Contributed by NM, 19-Oct-2011)

Ref Expression
Hypotheses omllaw4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
omllaw4.l ⊢ ≤ = ( le ‘ 𝐾 )
omllaw4.m ⊢ ∧ = ( meet ‘ 𝐾 )
omllaw4.o ⊢ ⊥ = ( oc ‘ 𝐾 )
Assertion omllaw4 ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ∧ 𝑌 ) = 𝑋 ) )

Proof

Step Hyp Ref Expression
1 omllaw4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 omllaw4.l ⊢ ≤ = ( le ‘ 𝐾 )
3 omllaw4.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 omllaw4.o ⊢ ⊥ = ( oc ‘ 𝐾 )
5 simp1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OML )
6 omlop ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OP )
7 6 3ad2ant1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OP )
8 simp3 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
9 1 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
10 7 8 9 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
11 simp2 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
12 1 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 )
13 7 11 12 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 )
14 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
15 1 2 14 3 4 omllaw ⊢ ( ( 𝐾 ∈ OML ∧ ( ⊥ ‘ 𝑌 ) ∈ 𝐵 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑌 ) ≤ ( ⊥ ‘ 𝑋 ) → ( ⊥ ‘ 𝑋 ) = ( ( ⊥ ‘ 𝑌 ) ( join ‘ 𝐾 ) ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) ) ) )
16 5 10 13 15 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑌 ) ≤ ( ⊥ ‘ 𝑋 ) → ( ⊥ ‘ 𝑋 ) = ( ( ⊥ ‘ 𝑌 ) ( join ‘ 𝐾 ) ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) ) ) )
17 1 2 4 oplecon3b ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ( ⊥ ‘ 𝑌 ) ≤ ( ⊥ ‘ 𝑋 ) ) )
18 6 17 syl3an1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ( ⊥ ‘ 𝑌 ) ≤ ( ⊥ ‘ 𝑋 ) ) )
19 omllat ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ Lat )
20 19 3ad2ant1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ Lat )
21 1 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ∈ 𝐵 )
22 20 13 8 21 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ∈ 𝐵 )
23 1 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ∈ 𝐵 ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ∈ 𝐵 )
24 7 22 23 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ∈ 𝐵 )
25 1 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ∧ 𝑌 ) ∈ 𝐵 )
26 20 24 8 25 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ∧ 𝑌 ) ∈ 𝐵 )
27 1 4 opcon3b ⊢ ( ( 𝐾 ∈ OP ∧ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ∧ 𝑌 ) = 𝑋 ↔ ( ⊥ ‘ 𝑋 ) = ( ⊥ ‘ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ∧ 𝑌 ) ) ) )
28 7 26 11 27 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ∧ 𝑌 ) = 𝑋 ↔ ( ⊥ ‘ 𝑋 ) = ( ⊥ ‘ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ∧ 𝑌 ) ) ) )
29 1 14 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ∈ 𝐵 ∧ ( ⊥ ‘ 𝑌 ) ∈ 𝐵 ) → ( ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ( join ‘ 𝐾 ) ( ⊥ ‘ 𝑌 ) ) = ( ( ⊥ ‘ 𝑌 ) ( join ‘ 𝐾 ) ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) )
30 20 22 10 29 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ( join ‘ 𝐾 ) ( ⊥ ‘ 𝑌 ) ) = ( ( ⊥ ‘ 𝑌 ) ( join ‘ 𝐾 ) ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) )
31 omlol ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OL )
32 31 3ad2ant1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OL )
33 1 14 3 4 oldmm2 ⊢ ( ( 𝐾 ∈ OL ∧ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ∧ 𝑌 ) ) = ( ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ( join ‘ 𝐾 ) ( ⊥ ‘ 𝑌 ) ) )
34 32 22 8 33 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ∧ 𝑌 ) ) = ( ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ( join ‘ 𝐾 ) ( ⊥ ‘ 𝑌 ) ) )
35 1 4 opococ ⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 )
36 7 8 35 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 )
37 36 oveq2d ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) = ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) )
38 37 oveq2d ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑌 ) ( join ‘ 𝐾 ) ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) ) = ( ( ⊥ ‘ 𝑌 ) ( join ‘ 𝐾 ) ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) )
39 30 34 38 3eqtr4d ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ∧ 𝑌 ) ) = ( ( ⊥ ‘ 𝑌 ) ( join ‘ 𝐾 ) ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) ) )
40 39 eqeq2d ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑋 ) = ( ⊥ ‘ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ∧ 𝑌 ) ) ↔ ( ⊥ ‘ 𝑋 ) = ( ( ⊥ ‘ 𝑌 ) ( join ‘ 𝐾 ) ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) ) ) )
41 28 40 bitrd ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ∧ 𝑌 ) = 𝑋 ↔ ( ⊥ ‘ 𝑋 ) = ( ( ⊥ ‘ 𝑌 ) ( join ‘ 𝐾 ) ( ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) ) ) )
42 16 18 41 3imtr4d ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ∧ 𝑌 ) = 𝑋 ) )