Metamath Proof Explorer


Theorem fh1

Description: Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. First of two parts. Theorem 5 of Kalmbach p. 25. (Contributed by NM, 14-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion fh1 A C B C C C A 𝐶 B A 𝐶 C A B C = A B A C

Proof

Step Hyp Ref Expression
1 chincl A C B C A B C
2 chincl A C C C A C C
3 chjcl A B C A C C A B A C C
4 1 2 3 syl2an A C B C A C C C A B A C C
5 4 anandis A C B C C C A B A C C
6 chjcl B C C C B C C
7 chincl A C B C C A B C C
8 6 7 sylan2 A C B C C C A B C C
9 chsh A B C C A B C S
10 8 9 syl A C B C C C A B C S
11 5 10 jca A C B C C C A B A C C A B C S
12 11 3impb A C B C C C A B A C C A B C S
13 12 adantr A C B C C C A 𝐶 B A 𝐶 C A B A C C A B C S
14 ledi A C B C C C A B A C A B C
15 14 adantr A C B C C C A 𝐶 B A 𝐶 C A B A C A B C
16 incom A B C = B C A
17 16 a1i A C B C A C C C A B C = B C A
18 chdmj1 A B C A C C A B A C = A B A C
19 1 2 18 syl2an A C B C A C C C A B A C = A B A C
20 chdmm1 A C B C A B = A B
21 chdmm1 A C C C A C = A C
22 20 21 ineqan12d A C B C A C C C A B A C = A B A C
23 19 22 eqtrd A C B C A C C C A B A C = A B A C
24 17 23 ineq12d A C B C A C C C A B C A B A C = B C A A B A C
25 24 3impdi A C B C C C A B C A B A C = B C A A B A C
26 25 adantr A C B C C C A 𝐶 B A 𝐶 C A B C A B A C = B C A A B A C
27 inass B C A A B A C = B C A A B A C
28 cmcm2 A C B C A 𝐶 B A 𝐶 B
29 choccl B C B C
30 cmbr3 A C B C A 𝐶 B A A B = A B
31 29 30 sylan2 A C B C A 𝐶 B A A B = A B
32 28 31 bitrd A C B C A 𝐶 B A A B = A B
33 32 biimpa A C B C A 𝐶 B A A B = A B
34 33 3adantl3 A C B C C C A 𝐶 B A A B = A B
35 34 adantrr A C B C C C A 𝐶 B A 𝐶 C A A B = A B
36 cmcm2 A C C C A 𝐶 C A 𝐶 C
37 choccl C C C C
38 cmbr3 A C C C A 𝐶 C A A C = A C
39 37 38 sylan2 A C C C A 𝐶 C A A C = A C
40 36 39 bitrd A C C C A 𝐶 C A A C = A C
41 40 biimpa A C C C A 𝐶 C A A C = A C
42 41 3adantl2 A C B C C C A 𝐶 C A A C = A C
43 42 adantrl A C B C C C A 𝐶 B A 𝐶 C A A C = A C
44 35 43 ineq12d A C B C C C A 𝐶 B A 𝐶 C A A B A A C = A B A C
45 inindi A A B A C = A A B A A C
46 inindi A B C = A B A C
47 44 45 46 3eqtr4g A C B C C C A 𝐶 B A 𝐶 C A A B A C = A B C
48 47 ineq2d A C B C C C A 𝐶 B A 𝐶 C B C A A B A C = B C A B C
49 27 48 syl5eq A C B C C C A 𝐶 B A 𝐶 C B C A A B A C = B C A B C
50 in12 B C A B C = A B C B C
51 49 50 eqtrdi A C B C C C A 𝐶 B A 𝐶 C B C A A B A C = A B C B C
52 chdmj1 B C C C B C = B C
53 52 ineq2d B C C C B C B C = B C B C
54 chocin B C C B C B C = 0
55 6 54 syl B C C C B C B C = 0
56 53 55 eqtr3d B C C C B C B C = 0
57 56 ineq2d B C C C A B C B C = A 0
58 chm0 A C A 0 = 0
59 57 58 sylan9eqr A C B C C C A B C B C = 0
60 59 3impb A C B C C C A B C B C = 0
61 60 adantr A C B C C C A 𝐶 B A 𝐶 C A B C B C = 0
62 51 61 eqtrd A C B C C C A 𝐶 B A 𝐶 C B C A A B A C = 0
63 26 62 eqtrd A C B C C C A 𝐶 B A 𝐶 C A B C A B A C = 0
64 pjoml A B A C C A B C S A B A C A B C A B C A B A C = 0 A B A C = A B C
65 13 15 63 64 syl12anc A C B C C C A 𝐶 B A 𝐶 C A B A C = A B C
66 65 eqcomd A C B C C C A 𝐶 B A 𝐶 C A B C = A B A C