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 B=BaseK
omllaw4.l ˙=K
omllaw4.m ˙=meetK
omllaw4.o ˙=ocK
Assertion omllaw4 KOMLXBYBX˙Y˙˙X˙Y˙Y=X

Proof

Step Hyp Ref Expression
1 omllaw4.b B=BaseK
2 omllaw4.l ˙=K
3 omllaw4.m ˙=meetK
4 omllaw4.o ˙=ocK
5 simp1 KOMLXBYBKOML
6 omlop KOMLKOP
7 6 3ad2ant1 KOMLXBYBKOP
8 simp3 KOMLXBYBYB
9 1 4 opoccl KOPYB˙YB
10 7 8 9 syl2anc KOMLXBYB˙YB
11 simp2 KOMLXBYBXB
12 1 4 opoccl KOPXB˙XB
13 7 11 12 syl2anc KOMLXBYB˙XB
14 eqid joinK=joinK
15 1 2 14 3 4 omllaw KOML˙YB˙XB˙Y˙˙X˙X=˙YjoinK˙X˙˙˙Y
16 5 10 13 15 syl3anc KOMLXBYB˙Y˙˙X˙X=˙YjoinK˙X˙˙˙Y
17 1 2 4 oplecon3b KOPXBYBX˙Y˙Y˙˙X
18 6 17 syl3an1 KOMLXBYBX˙Y˙Y˙˙X
19 omllat KOMLKLat
20 19 3ad2ant1 KOMLXBYBKLat
21 1 3 latmcl KLat˙XBYB˙X˙YB
22 20 13 8 21 syl3anc KOMLXBYB˙X˙YB
23 1 4 opoccl KOP˙X˙YB˙˙X˙YB
24 7 22 23 syl2anc KOMLXBYB˙˙X˙YB
25 1 3 latmcl KLat˙˙X˙YBYB˙˙X˙Y˙YB
26 20 24 8 25 syl3anc KOMLXBYB˙˙X˙Y˙YB
27 1 4 opcon3b KOP˙˙X˙Y˙YBXB˙˙X˙Y˙Y=X˙X=˙˙˙X˙Y˙Y
28 7 26 11 27 syl3anc KOMLXBYB˙˙X˙Y˙Y=X˙X=˙˙˙X˙Y˙Y
29 1 14 latjcom KLat˙X˙YB˙YB˙X˙YjoinK˙Y=˙YjoinK˙X˙Y
30 20 22 10 29 syl3anc KOMLXBYB˙X˙YjoinK˙Y=˙YjoinK˙X˙Y
31 omlol KOMLKOL
32 31 3ad2ant1 KOMLXBYBKOL
33 1 14 3 4 oldmm2 KOL˙X˙YBYB˙˙˙X˙Y˙Y=˙X˙YjoinK˙Y
34 32 22 8 33 syl3anc KOMLXBYB˙˙˙X˙Y˙Y=˙X˙YjoinK˙Y
35 1 4 opococ KOPYB˙˙Y=Y
36 7 8 35 syl2anc KOMLXBYB˙˙Y=Y
37 36 oveq2d KOMLXBYB˙X˙˙˙Y=˙X˙Y
38 37 oveq2d KOMLXBYB˙YjoinK˙X˙˙˙Y=˙YjoinK˙X˙Y
39 30 34 38 3eqtr4d KOMLXBYB˙˙˙X˙Y˙Y=˙YjoinK˙X˙˙˙Y
40 39 eqeq2d KOMLXBYB˙X=˙˙˙X˙Y˙Y˙X=˙YjoinK˙X˙˙˙Y
41 28 40 bitrd KOMLXBYB˙˙X˙Y˙Y=X˙X=˙YjoinK˙X˙˙˙Y
42 16 18 41 3imtr4d KOMLXBYBX˙Y˙˙X˙Y˙Y=X