Metamath Proof Explorer


Theorem omlfh1N

Description: Foulis-Holland Theorem, part 1. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Part of Theorem 5 in Kalmbach p. 25. ( fh1 analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses omlfh1.b B=BaseK
omlfh1.j ˙=joinK
omlfh1.m ˙=meetK
omlfh1.c C=cmK
Assertion omlfh1N KOMLXBYBZBXCYXCZX˙Y˙Z=X˙Y˙X˙Z

Proof

Step Hyp Ref Expression
1 omlfh1.b B=BaseK
2 omlfh1.j ˙=joinK
3 omlfh1.m ˙=meetK
4 omlfh1.c C=cmK
5 omllat KOMLKLat
6 eqid K=K
7 1 6 2 3 latledi KLatXBYBZBX˙Y˙X˙ZKX˙Y˙Z
8 5 7 sylan KOMLXBYBZBX˙Y˙X˙ZKX˙Y˙Z
9 8 3adant3 KOMLXBYBZBXCYXCZX˙Y˙X˙ZKX˙Y˙Z
10 5 adantr KOMLXBYBZBKLat
11 simpr1 KOMLXBYBZBXB
12 simpr2 KOMLXBYBZBYB
13 simpr3 KOMLXBYBZBZB
14 1 2 latjcl KLatYBZBY˙ZB
15 10 12 13 14 syl3anc KOMLXBYBZBY˙ZB
16 1 3 latmcom KLatXBY˙ZBX˙Y˙Z=Y˙Z˙X
17 10 11 15 16 syl3anc KOMLXBYBZBX˙Y˙Z=Y˙Z˙X
18 omlol KOMLKOL
19 18 adantr KOMLXBYBZBKOL
20 1 3 latmcl KLatXBYBX˙YB
21 10 11 12 20 syl3anc KOMLXBYBZBX˙YB
22 1 3 latmcl KLatXBZBX˙ZB
23 10 11 13 22 syl3anc KOMLXBYBZBX˙ZB
24 eqid ocK=ocK
25 1 2 3 24 oldmj1 KOLX˙YBX˙ZBocKX˙Y˙X˙Z=ocKX˙Y˙ocKX˙Z
26 19 21 23 25 syl3anc KOMLXBYBZBocKX˙Y˙X˙Z=ocKX˙Y˙ocKX˙Z
27 1 2 3 24 oldmm1 KOLXBYBocKX˙Y=ocKX˙ocKY
28 19 11 12 27 syl3anc KOMLXBYBZBocKX˙Y=ocKX˙ocKY
29 1 2 3 24 oldmm1 KOLXBZBocKX˙Z=ocKX˙ocKZ
30 19 11 13 29 syl3anc KOMLXBYBZBocKX˙Z=ocKX˙ocKZ
31 28 30 oveq12d KOMLXBYBZBocKX˙Y˙ocKX˙Z=ocKX˙ocKY˙ocKX˙ocKZ
32 26 31 eqtrd KOMLXBYBZBocKX˙Y˙X˙Z=ocKX˙ocKY˙ocKX˙ocKZ
33 17 32 oveq12d KOMLXBYBZBX˙Y˙Z˙ocKX˙Y˙X˙Z=Y˙Z˙X˙ocKX˙ocKY˙ocKX˙ocKZ
34 33 3adant3 KOMLXBYBZBXCYXCZX˙Y˙Z˙ocKX˙Y˙X˙Z=Y˙Z˙X˙ocKX˙ocKY˙ocKX˙ocKZ
35 omlop KOMLKOP
36 35 adantr KOMLXBYBZBKOP
37 1 24 opoccl KOPXBocKXB
38 36 11 37 syl2anc KOMLXBYBZBocKXB
39 1 24 opoccl KOPYBocKYB
40 36 12 39 syl2anc KOMLXBYBZBocKYB
41 1 2 latjcl KLatocKXBocKYBocKX˙ocKYB
42 10 38 40 41 syl3anc KOMLXBYBZBocKX˙ocKYB
43 1 24 opoccl KOPZBocKZB
44 36 13 43 syl2anc KOMLXBYBZBocKZB
45 1 2 latjcl KLatocKXBocKZBocKX˙ocKZB
46 10 38 44 45 syl3anc KOMLXBYBZBocKX˙ocKZB
47 1 3 latmcl KLatocKX˙ocKYBocKX˙ocKZBocKX˙ocKY˙ocKX˙ocKZB
48 10 42 46 47 syl3anc KOMLXBYBZBocKX˙ocKY˙ocKX˙ocKZB
49 1 3 latmassOLD KOLY˙ZBXBocKX˙ocKY˙ocKX˙ocKZBY˙Z˙X˙ocKX˙ocKY˙ocKX˙ocKZ=Y˙Z˙X˙ocKX˙ocKY˙ocKX˙ocKZ
50 19 15 11 48 49 syl13anc KOMLXBYBZBY˙Z˙X˙ocKX˙ocKY˙ocKX˙ocKZ=Y˙Z˙X˙ocKX˙ocKY˙ocKX˙ocKZ
51 50 3adant3 KOMLXBYBZBXCYXCZY˙Z˙X˙ocKX˙ocKY˙ocKX˙ocKZ=Y˙Z˙X˙ocKX˙ocKY˙ocKX˙ocKZ
52 1 24 4 cmt2N KOMLXBYBXCYXCocKY
53 52 3adant3r3 KOMLXBYBZBXCYXCocKY
54 simpl KOMLXBYBZBKOML
55 1 2 3 24 4 cmtbr3N KOMLXBocKYBXCocKYX˙ocKX˙ocKY=X˙ocKY
56 54 11 40 55 syl3anc KOMLXBYBZBXCocKYX˙ocKX˙ocKY=X˙ocKY
57 53 56 bitrd KOMLXBYBZBXCYX˙ocKX˙ocKY=X˙ocKY
58 57 biimpa KOMLXBYBZBXCYX˙ocKX˙ocKY=X˙ocKY
59 58 adantrr KOMLXBYBZBXCYXCZX˙ocKX˙ocKY=X˙ocKY
60 59 3impa KOMLXBYBZBXCYXCZX˙ocKX˙ocKY=X˙ocKY
61 1 24 4 cmt2N KOMLXBZBXCZXCocKZ
62 61 3adant3r2 KOMLXBYBZBXCZXCocKZ
63 1 2 3 24 4 cmtbr3N KOMLXBocKZBXCocKZX˙ocKX˙ocKZ=X˙ocKZ
64 54 11 44 63 syl3anc KOMLXBYBZBXCocKZX˙ocKX˙ocKZ=X˙ocKZ
65 62 64 bitrd KOMLXBYBZBXCZX˙ocKX˙ocKZ=X˙ocKZ
66 65 biimpa KOMLXBYBZBXCZX˙ocKX˙ocKZ=X˙ocKZ
67 66 adantrl KOMLXBYBZBXCYXCZX˙ocKX˙ocKZ=X˙ocKZ
68 67 3impa KOMLXBYBZBXCYXCZX˙ocKX˙ocKZ=X˙ocKZ
69 60 68 oveq12d KOMLXBYBZBXCYXCZX˙ocKX˙ocKY˙X˙ocKX˙ocKZ=X˙ocKY˙X˙ocKZ
70 1 3 latmmdiN KOLXBocKX˙ocKYBocKX˙ocKZBX˙ocKX˙ocKY˙ocKX˙ocKZ=X˙ocKX˙ocKY˙X˙ocKX˙ocKZ
71 19 11 42 46 70 syl13anc KOMLXBYBZBX˙ocKX˙ocKY˙ocKX˙ocKZ=X˙ocKX˙ocKY˙X˙ocKX˙ocKZ
72 71 3adant3 KOMLXBYBZBXCYXCZX˙ocKX˙ocKY˙ocKX˙ocKZ=X˙ocKX˙ocKY˙X˙ocKX˙ocKZ
73 1 3 latmmdiN KOLXBocKYBocKZBX˙ocKY˙ocKZ=X˙ocKY˙X˙ocKZ
74 19 11 40 44 73 syl13anc KOMLXBYBZBX˙ocKY˙ocKZ=X˙ocKY˙X˙ocKZ
75 74 3adant3 KOMLXBYBZBXCYXCZX˙ocKY˙ocKZ=X˙ocKY˙X˙ocKZ
76 69 72 75 3eqtr4d KOMLXBYBZBXCYXCZX˙ocKX˙ocKY˙ocKX˙ocKZ=X˙ocKY˙ocKZ
77 76 oveq2d KOMLXBYBZBXCYXCZY˙Z˙X˙ocKX˙ocKY˙ocKX˙ocKZ=Y˙Z˙X˙ocKY˙ocKZ
78 1 3 latmcl KLatocKYBocKZBocKY˙ocKZB
79 10 40 44 78 syl3anc KOMLXBYBZBocKY˙ocKZB
80 1 3 latm12 KOLY˙ZBXBocKY˙ocKZBY˙Z˙X˙ocKY˙ocKZ=X˙Y˙Z˙ocKY˙ocKZ
81 19 15 11 79 80 syl13anc KOMLXBYBZBY˙Z˙X˙ocKY˙ocKZ=X˙Y˙Z˙ocKY˙ocKZ
82 81 3adant3 KOMLXBYBZBXCYXCZY˙Z˙X˙ocKY˙ocKZ=X˙Y˙Z˙ocKY˙ocKZ
83 51 77 82 3eqtrd KOMLXBYBZBXCYXCZY˙Z˙X˙ocKX˙ocKY˙ocKX˙ocKZ=X˙Y˙Z˙ocKY˙ocKZ
84 1 2 3 24 oldmj1 KOLYBZBocKY˙Z=ocKY˙ocKZ
85 19 12 13 84 syl3anc KOMLXBYBZBocKY˙Z=ocKY˙ocKZ
86 85 oveq2d KOMLXBYBZBY˙Z˙ocKY˙Z=Y˙Z˙ocKY˙ocKZ
87 eqid 0.K=0.K
88 1 24 3 87 opnoncon KOPY˙ZBY˙Z˙ocKY˙Z=0.K
89 36 15 88 syl2anc KOMLXBYBZBY˙Z˙ocKY˙Z=0.K
90 86 89 eqtr3d KOMLXBYBZBY˙Z˙ocKY˙ocKZ=0.K
91 90 oveq2d KOMLXBYBZBX˙Y˙Z˙ocKY˙ocKZ=X˙0.K
92 1 3 87 olm01 KOLXBX˙0.K=0.K
93 19 11 92 syl2anc KOMLXBYBZBX˙0.K=0.K
94 91 93 eqtrd KOMLXBYBZBX˙Y˙Z˙ocKY˙ocKZ=0.K
95 94 3adant3 KOMLXBYBZBXCYXCZX˙Y˙Z˙ocKY˙ocKZ=0.K
96 34 83 95 3eqtrd KOMLXBYBZBXCYXCZX˙Y˙Z˙ocKX˙Y˙X˙Z=0.K
97 1 2 latjcl KLatX˙YBX˙ZBX˙Y˙X˙ZB
98 10 21 23 97 syl3anc KOMLXBYBZBX˙Y˙X˙ZB
99 1 3 latmcl KLatXBY˙ZBX˙Y˙ZB
100 10 11 15 99 syl3anc KOMLXBYBZBX˙Y˙ZB
101 1 6 3 24 87 omllaw3 KOMLX˙Y˙X˙ZBX˙Y˙ZBX˙Y˙X˙ZKX˙Y˙ZX˙Y˙Z˙ocKX˙Y˙X˙Z=0.KX˙Y˙X˙Z=X˙Y˙Z
102 54 98 100 101 syl3anc KOMLXBYBZBX˙Y˙X˙ZKX˙Y˙ZX˙Y˙Z˙ocKX˙Y˙X˙Z=0.KX˙Y˙X˙Z=X˙Y˙Z
103 102 3adant3 KOMLXBYBZBXCYXCZX˙Y˙X˙ZKX˙Y˙ZX˙Y˙Z˙ocKX˙Y˙X˙Z=0.KX˙Y˙X˙Z=X˙Y˙Z
104 9 96 103 mp2and KOMLXBYBZBXCYXCZX˙Y˙X˙Z=X˙Y˙Z
105 104 eqcomd KOMLXBYBZBXCYXCZX˙Y˙Z=X˙Y˙X˙Z