Metamath Proof Explorer


Theorem fh2

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

Ref Expression
Assertion fh2
|- ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( A i^i ( B vH C ) ) = ( ( A i^i B ) vH ( A i^i C ) ) )

Proof

Step Hyp Ref Expression
1 chincl
 |-  ( ( A e. CH /\ B e. CH ) -> ( A i^i B ) e. CH )
2 chincl
 |-  ( ( A e. CH /\ C e. CH ) -> ( A i^i C ) e. CH )
3 chjcl
 |-  ( ( ( A i^i B ) e. CH /\ ( A i^i C ) e. CH ) -> ( ( A i^i B ) vH ( A i^i C ) ) e. CH )
4 1 2 3 syl2an
 |-  ( ( ( A e. CH /\ B e. CH ) /\ ( A e. CH /\ C e. CH ) ) -> ( ( A i^i B ) vH ( A i^i C ) ) e. CH )
5 4 anandis
 |-  ( ( A e. CH /\ ( B e. CH /\ C e. CH ) ) -> ( ( A i^i B ) vH ( A i^i C ) ) e. CH )
6 chjcl
 |-  ( ( B e. CH /\ C e. CH ) -> ( B vH C ) e. CH )
7 chincl
 |-  ( ( A e. CH /\ ( B vH C ) e. CH ) -> ( A i^i ( B vH C ) ) e. CH )
8 6 7 sylan2
 |-  ( ( A e. CH /\ ( B e. CH /\ C e. CH ) ) -> ( A i^i ( B vH C ) ) e. CH )
9 chsh
 |-  ( ( A i^i ( B vH C ) ) e. CH -> ( A i^i ( B vH C ) ) e. SH )
10 8 9 syl
 |-  ( ( A e. CH /\ ( B e. CH /\ C e. CH ) ) -> ( A i^i ( B vH C ) ) e. SH )
11 5 10 jca
 |-  ( ( A e. CH /\ ( B e. CH /\ C e. CH ) ) -> ( ( ( A i^i B ) vH ( A i^i C ) ) e. CH /\ ( A i^i ( B vH C ) ) e. SH ) )
12 11 3impb
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( ( A i^i B ) vH ( A i^i C ) ) e. CH /\ ( A i^i ( B vH C ) ) e. SH ) )
13 12 adantr
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( ( ( A i^i B ) vH ( A i^i C ) ) e. CH /\ ( A i^i ( B vH C ) ) e. SH ) )
14 ledi
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( A i^i B ) vH ( A i^i C ) ) C_ ( A i^i ( B vH C ) ) )
15 14 adantr
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( ( A i^i B ) vH ( A i^i C ) ) C_ ( A i^i ( B vH C ) ) )
16 chdmj1
 |-  ( ( ( A i^i B ) e. CH /\ ( A i^i C ) e. CH ) -> ( _|_ ` ( ( A i^i B ) vH ( A i^i C ) ) ) = ( ( _|_ ` ( A i^i B ) ) i^i ( _|_ ` ( A i^i C ) ) ) )
17 1 2 16 syl2an
 |-  ( ( ( A e. CH /\ B e. CH ) /\ ( A e. CH /\ C e. CH ) ) -> ( _|_ ` ( ( A i^i B ) vH ( A i^i C ) ) ) = ( ( _|_ ` ( A i^i B ) ) i^i ( _|_ ` ( A i^i C ) ) ) )
18 chdmm1
 |-  ( ( A e. CH /\ B e. CH ) -> ( _|_ ` ( A i^i B ) ) = ( ( _|_ ` A ) vH ( _|_ ` B ) ) )
19 18 adantr
 |-  ( ( ( A e. CH /\ B e. CH ) /\ ( A e. CH /\ C e. CH ) ) -> ( _|_ ` ( A i^i B ) ) = ( ( _|_ ` A ) vH ( _|_ ` B ) ) )
20 19 ineq1d
 |-  ( ( ( A e. CH /\ B e. CH ) /\ ( A e. CH /\ C e. CH ) ) -> ( ( _|_ ` ( A i^i B ) ) i^i ( _|_ ` ( A i^i C ) ) ) = ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( _|_ ` ( A i^i C ) ) ) )
21 17 20 eqtrd
 |-  ( ( ( A e. CH /\ B e. CH ) /\ ( A e. CH /\ C e. CH ) ) -> ( _|_ ` ( ( A i^i B ) vH ( A i^i C ) ) ) = ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( _|_ ` ( A i^i C ) ) ) )
22 21 3impdi
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( _|_ ` ( ( A i^i B ) vH ( A i^i C ) ) ) = ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( _|_ ` ( A i^i C ) ) ) )
23 22 ineq2d
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( A i^i ( B vH C ) ) i^i ( _|_ ` ( ( A i^i B ) vH ( A i^i C ) ) ) ) = ( ( A i^i ( B vH C ) ) i^i ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( _|_ ` ( A i^i C ) ) ) ) )
24 23 adantr
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( ( A i^i ( B vH C ) ) i^i ( _|_ ` ( ( A i^i B ) vH ( A i^i C ) ) ) ) = ( ( A i^i ( B vH C ) ) i^i ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( _|_ ` ( A i^i C ) ) ) ) )
25 in4
 |-  ( ( A i^i ( B vH C ) ) i^i ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( _|_ ` ( A i^i C ) ) ) ) = ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) i^i ( ( B vH C ) i^i ( _|_ ` ( A i^i C ) ) ) )
26 cmcm2
 |-  ( ( A e. CH /\ B e. CH ) -> ( A C_H B <-> A C_H ( _|_ ` B ) ) )
27 cmcm
 |-  ( ( A e. CH /\ B e. CH ) -> ( A C_H B <-> B C_H A ) )
28 choccl
 |-  ( B e. CH -> ( _|_ ` B ) e. CH )
29 cmbr3
 |-  ( ( A e. CH /\ ( _|_ ` B ) e. CH ) -> ( A C_H ( _|_ ` B ) <-> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( A i^i ( _|_ ` B ) ) ) )
30 28 29 sylan2
 |-  ( ( A e. CH /\ B e. CH ) -> ( A C_H ( _|_ ` B ) <-> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( A i^i ( _|_ ` B ) ) ) )
31 26 27 30 3bitr3d
 |-  ( ( A e. CH /\ B e. CH ) -> ( B C_H A <-> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( A i^i ( _|_ ` B ) ) ) )
32 31 biimpa
 |-  ( ( ( A e. CH /\ B e. CH ) /\ B C_H A ) -> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( A i^i ( _|_ ` B ) ) )
33 incom
 |-  ( A i^i ( _|_ ` B ) ) = ( ( _|_ ` B ) i^i A )
34 32 33 eqtrdi
 |-  ( ( ( A e. CH /\ B e. CH ) /\ B C_H A ) -> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( ( _|_ ` B ) i^i A ) )
35 34 3adantl3
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ B C_H A ) -> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( ( _|_ ` B ) i^i A ) )
36 35 adantrr
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( ( _|_ ` B ) i^i A ) )
37 36 ineq1d
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) i^i ( ( B vH C ) i^i ( _|_ ` ( A i^i C ) ) ) ) = ( ( ( _|_ ` B ) i^i A ) i^i ( ( B vH C ) i^i ( _|_ ` ( A i^i C ) ) ) ) )
38 25 37 syl5eq
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( ( A i^i ( B vH C ) ) i^i ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( _|_ ` ( A i^i C ) ) ) ) = ( ( ( _|_ ` B ) i^i A ) i^i ( ( B vH C ) i^i ( _|_ ` ( A i^i C ) ) ) ) )
39 24 38 eqtrd
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( ( A i^i ( B vH C ) ) i^i ( _|_ ` ( ( A i^i B ) vH ( A i^i C ) ) ) ) = ( ( ( _|_ ` B ) i^i A ) i^i ( ( B vH C ) i^i ( _|_ ` ( A i^i C ) ) ) ) )
40 in4
 |-  ( ( ( _|_ ` B ) i^i A ) i^i ( ( B vH C ) i^i ( _|_ ` ( A i^i C ) ) ) ) = ( ( ( _|_ ` B ) i^i ( B vH C ) ) i^i ( A i^i ( _|_ ` ( A i^i C ) ) ) )
41 39 40 eqtrdi
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( ( A i^i ( B vH C ) ) i^i ( _|_ ` ( ( A i^i B ) vH ( A i^i C ) ) ) ) = ( ( ( _|_ ` B ) i^i ( B vH C ) ) i^i ( A i^i ( _|_ ` ( A i^i C ) ) ) ) )
42 ococ
 |-  ( B e. CH -> ( _|_ ` ( _|_ ` B ) ) = B )
43 42 oveq1d
 |-  ( B e. CH -> ( ( _|_ ` ( _|_ ` B ) ) vH C ) = ( B vH C ) )
44 43 ineq2d
 |-  ( B e. CH -> ( ( _|_ ` B ) i^i ( ( _|_ ` ( _|_ ` B ) ) vH C ) ) = ( ( _|_ ` B ) i^i ( B vH C ) ) )
45 44 3ad2ant2
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( _|_ ` B ) i^i ( ( _|_ ` ( _|_ ` B ) ) vH C ) ) = ( ( _|_ ` B ) i^i ( B vH C ) ) )
46 45 adantr
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( ( _|_ ` B ) i^i ( ( _|_ ` ( _|_ ` B ) ) vH C ) ) = ( ( _|_ ` B ) i^i ( B vH C ) ) )
47 cmcm3
 |-  ( ( B e. CH /\ C e. CH ) -> ( B C_H C <-> ( _|_ ` B ) C_H C ) )
48 cmbr3
 |-  ( ( ( _|_ ` B ) e. CH /\ C e. CH ) -> ( ( _|_ ` B ) C_H C <-> ( ( _|_ ` B ) i^i ( ( _|_ ` ( _|_ ` B ) ) vH C ) ) = ( ( _|_ ` B ) i^i C ) ) )
49 28 48 sylan
 |-  ( ( B e. CH /\ C e. CH ) -> ( ( _|_ ` B ) C_H C <-> ( ( _|_ ` B ) i^i ( ( _|_ ` ( _|_ ` B ) ) vH C ) ) = ( ( _|_ ` B ) i^i C ) ) )
50 47 49 bitrd
 |-  ( ( B e. CH /\ C e. CH ) -> ( B C_H C <-> ( ( _|_ ` B ) i^i ( ( _|_ ` ( _|_ ` B ) ) vH C ) ) = ( ( _|_ ` B ) i^i C ) ) )
51 50 biimpa
 |-  ( ( ( B e. CH /\ C e. CH ) /\ B C_H C ) -> ( ( _|_ ` B ) i^i ( ( _|_ ` ( _|_ ` B ) ) vH C ) ) = ( ( _|_ ` B ) i^i C ) )
52 51 3adantl1
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ B C_H C ) -> ( ( _|_ ` B ) i^i ( ( _|_ ` ( _|_ ` B ) ) vH C ) ) = ( ( _|_ ` B ) i^i C ) )
53 52 adantrl
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( ( _|_ ` B ) i^i ( ( _|_ ` ( _|_ ` B ) ) vH C ) ) = ( ( _|_ ` B ) i^i C ) )
54 46 53 eqtr3d
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( ( _|_ ` B ) i^i ( B vH C ) ) = ( ( _|_ ` B ) i^i C ) )
55 54 ineq1d
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( ( ( _|_ ` B ) i^i ( B vH C ) ) i^i ( A i^i ( _|_ ` ( A i^i C ) ) ) ) = ( ( ( _|_ ` B ) i^i C ) i^i ( A i^i ( _|_ ` ( A i^i C ) ) ) ) )
56 inass
 |-  ( ( ( _|_ ` B ) i^i C ) i^i ( A i^i ( _|_ ` ( A i^i C ) ) ) ) = ( ( _|_ ` B ) i^i ( C i^i ( A i^i ( _|_ ` ( A i^i C ) ) ) ) )
57 in12
 |-  ( C i^i ( A i^i ( _|_ ` ( A i^i C ) ) ) ) = ( A i^i ( C i^i ( _|_ ` ( A i^i C ) ) ) )
58 inass
 |-  ( ( A i^i C ) i^i ( _|_ ` ( A i^i C ) ) ) = ( A i^i ( C i^i ( _|_ ` ( A i^i C ) ) ) )
59 57 58 eqtr4i
 |-  ( C i^i ( A i^i ( _|_ ` ( A i^i C ) ) ) ) = ( ( A i^i C ) i^i ( _|_ ` ( A i^i C ) ) )
60 chocin
 |-  ( ( A i^i C ) e. CH -> ( ( A i^i C ) i^i ( _|_ ` ( A i^i C ) ) ) = 0H )
61 2 60 syl
 |-  ( ( A e. CH /\ C e. CH ) -> ( ( A i^i C ) i^i ( _|_ ` ( A i^i C ) ) ) = 0H )
62 59 61 syl5eq
 |-  ( ( A e. CH /\ C e. CH ) -> ( C i^i ( A i^i ( _|_ ` ( A i^i C ) ) ) ) = 0H )
63 62 ineq2d
 |-  ( ( A e. CH /\ C e. CH ) -> ( ( _|_ ` B ) i^i ( C i^i ( A i^i ( _|_ ` ( A i^i C ) ) ) ) ) = ( ( _|_ ` B ) i^i 0H ) )
64 56 63 syl5eq
 |-  ( ( A e. CH /\ C e. CH ) -> ( ( ( _|_ ` B ) i^i C ) i^i ( A i^i ( _|_ ` ( A i^i C ) ) ) ) = ( ( _|_ ` B ) i^i 0H ) )
65 64 3adant2
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( ( _|_ ` B ) i^i C ) i^i ( A i^i ( _|_ ` ( A i^i C ) ) ) ) = ( ( _|_ ` B ) i^i 0H ) )
66 chm0
 |-  ( ( _|_ ` B ) e. CH -> ( ( _|_ ` B ) i^i 0H ) = 0H )
67 28 66 syl
 |-  ( B e. CH -> ( ( _|_ ` B ) i^i 0H ) = 0H )
68 67 3ad2ant2
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( _|_ ` B ) i^i 0H ) = 0H )
69 65 68 eqtrd
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( ( _|_ ` B ) i^i C ) i^i ( A i^i ( _|_ ` ( A i^i C ) ) ) ) = 0H )
70 69 adantr
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( ( ( _|_ ` B ) i^i C ) i^i ( A i^i ( _|_ ` ( A i^i C ) ) ) ) = 0H )
71 55 70 eqtrd
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( ( ( _|_ ` B ) i^i ( B vH C ) ) i^i ( A i^i ( _|_ ` ( A i^i C ) ) ) ) = 0H )
72 41 71 eqtrd
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( ( A i^i ( B vH C ) ) i^i ( _|_ ` ( ( A i^i B ) vH ( A i^i C ) ) ) ) = 0H )
73 pjoml
 |-  ( ( ( ( ( A i^i B ) vH ( A i^i C ) ) e. CH /\ ( A i^i ( B vH C ) ) e. SH ) /\ ( ( ( A i^i B ) vH ( A i^i C ) ) C_ ( A i^i ( B vH C ) ) /\ ( ( A i^i ( B vH C ) ) i^i ( _|_ ` ( ( A i^i B ) vH ( A i^i C ) ) ) ) = 0H ) ) -> ( ( A i^i B ) vH ( A i^i C ) ) = ( A i^i ( B vH C ) ) )
74 13 15 72 73 syl12anc
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( ( A i^i B ) vH ( A i^i C ) ) = ( A i^i ( B vH C ) ) )
75 74 eqcomd
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B C_H A /\ B C_H C ) ) -> ( A i^i ( B vH C ) ) = ( ( A i^i B ) vH ( A i^i C ) ) )