# 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}={\mathrm{Base}}_{{K}}$
omlfh1.j
omlfh1.m
omlfh1.c ${⊢}{C}=\mathrm{cm}\left({K}\right)$
Assertion omlfh1N

### Proof

Step Hyp Ref Expression
1 omlfh1.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 omlfh1.j
3 omlfh1.m
4 omlfh1.c ${⊢}{C}=\mathrm{cm}\left({K}\right)$
5 omllat ${⊢}{K}\in \mathrm{OML}\to {K}\in \mathrm{Lat}$
6 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
7 1 6 2 3 latledi
8 5 7 sylan
10 5 adantr ${⊢}\left({K}\in \mathrm{OML}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {K}\in \mathrm{Lat}$
11 simpr1 ${⊢}\left({K}\in \mathrm{OML}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {X}\in {B}$
12 simpr2 ${⊢}\left({K}\in \mathrm{OML}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Y}\in {B}$
13 simpr3 ${⊢}\left({K}\in \mathrm{OML}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Z}\in {B}$
14 1 2 latjcl
15 10 12 13 14 syl3anc
16 1 3 latmcom
17 10 11 15 16 syl3anc
18 omlol ${⊢}{K}\in \mathrm{OML}\to {K}\in \mathrm{OL}$
19 18 adantr ${⊢}\left({K}\in \mathrm{OML}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {K}\in \mathrm{OL}$
20 1 3 latmcl
21 10 11 12 20 syl3anc
22 1 3 latmcl
23 10 11 13 22 syl3anc
24 eqid ${⊢}\mathrm{oc}\left({K}\right)=\mathrm{oc}\left({K}\right)$
25 1 2 3 24 oldmj1
26 19 21 23 25 syl3anc
27 1 2 3 24 oldmm1
28 19 11 12 27 syl3anc
29 1 2 3 24 oldmm1
30 19 11 13 29 syl3anc
31 28 30 oveq12d
32 26 31 eqtrd
33 17 32 oveq12d
35 omlop ${⊢}{K}\in \mathrm{OML}\to {K}\in \mathrm{OP}$
36 35 adantr ${⊢}\left({K}\in \mathrm{OML}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {K}\in \mathrm{OP}$
37 1 24 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {X}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}$
38 36 11 37 syl2anc ${⊢}\left({K}\in \mathrm{OML}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}$
39 1 24 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}$
40 36 12 39 syl2anc ${⊢}\left({K}\in \mathrm{OML}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}$
41 1 2 latjcl
42 10 38 40 41 syl3anc
43 1 24 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {Z}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({Z}\right)\in {B}$
44 36 13 43 syl2anc ${⊢}\left({K}\in \mathrm{OML}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \mathrm{oc}\left({K}\right)\left({Z}\right)\in {B}$
45 1 2 latjcl
46 10 38 44 45 syl3anc
47 1 3 latmcl
48 10 42 46 47 syl3anc
49 1 3 latmassOLD
50 19 15 11 48 49 syl13anc
52 1 24 4 cmt2N ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left({X}{C}{Y}↔{X}{C}\mathrm{oc}\left({K}\right)\left({Y}\right)\right)$
53 52 3adant3r3 ${⊢}\left({K}\in \mathrm{OML}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left({X}{C}{Y}↔{X}{C}\mathrm{oc}\left({K}\right)\left({Y}\right)\right)$
54 simpl ${⊢}\left({K}\in \mathrm{OML}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {K}\in \mathrm{OML}$
55 1 2 3 24 4 cmtbr3N
56 54 11 40 55 syl3anc
57 53 56 bitrd
58 57 biimpa
60 59 3impa
61 1 24 4 cmt2N ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {Z}\in {B}\right)\to \left({X}{C}{Z}↔{X}{C}\mathrm{oc}\left({K}\right)\left({Z}\right)\right)$
62 61 3adant3r2 ${⊢}\left({K}\in \mathrm{OML}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left({X}{C}{Z}↔{X}{C}\mathrm{oc}\left({K}\right)\left({Z}\right)\right)$
63 1 2 3 24 4 cmtbr3N
64 54 11 44 63 syl3anc
65 62 64 bitrd
66 65 biimpa
68 67 3impa
69 60 68 oveq12d
70 1 3 latmmdiN
71 19 11 42 46 70 syl13anc
73 1 3 latmmdiN
74 19 11 40 44 73 syl13anc
76 69 72 75 3eqtr4d
77 76 oveq2d
78 1 3 latmcl
79 10 40 44 78 syl3anc
80 1 3 latm12
81 19 15 11 79 80 syl13anc
83 51 77 82 3eqtrd
84 1 2 3 24 oldmj1
85 19 12 13 84 syl3anc
86 85 oveq2d
87 eqid ${⊢}\mathrm{0.}\left({K}\right)=\mathrm{0.}\left({K}\right)$
88 1 24 3 87 opnoncon
89 36 15 88 syl2anc
90 86 89 eqtr3d
91 90 oveq2d
92 1 3 87 olm01
93 19 11 92 syl2anc
94 91 93 eqtrd