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 e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A 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 ) /\ ( A C_H B /\ A 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 ) /\ ( A C_H B /\ A C_H C ) ) -> ( ( A i^i B ) vH ( A i^i C ) ) C_ ( A i^i ( B vH C ) ) )
16 incom 
 |-  ( A i^i ( B vH C ) ) = ( ( B vH C ) i^i A )
17 16 a1i 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ ( A e. CH /\ C e. CH ) ) -> ( A i^i ( B vH C ) ) = ( ( B vH C ) i^i A ) )
18 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 ) ) ) )
19 1 2 18 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 ) ) ) )
20 chdmm1 
 |-  ( ( A e. CH /\ B e. CH ) -> ( _|_ ` ( A i^i B ) ) = ( ( _|_ ` A ) vH ( _|_ ` B ) ) )
21 chdmm1 
 |-  ( ( A e. CH /\ C e. CH ) -> ( _|_ ` ( A i^i C ) ) = ( ( _|_ ` A ) vH ( _|_ ` C ) ) )
22 20 21 ineqan12d 
 |-  ( ( ( 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 ) vH ( _|_ ` C ) ) ) )
23 19 22 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 ) vH ( _|_ ` C ) ) ) )
24 17 23 ineq12d 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ ( A e. CH /\ C e. CH ) ) -> ( ( A i^i ( B vH C ) ) i^i ( _|_ ` ( ( A i^i B ) vH ( A i^i C ) ) ) ) = ( ( ( B vH C ) i^i A ) i^i ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) ) )
25 24 3impdi 
 |-  ( ( 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 ) ) ) ) = ( ( ( B vH C ) i^i A ) i^i ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) ) )
26 25 adantr 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( ( A i^i ( B vH C ) ) i^i ( _|_ ` ( ( A i^i B ) vH ( A i^i C ) ) ) ) = ( ( ( B vH C ) i^i A ) i^i ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) ) )
27 inass 
 |-  ( ( ( B vH C ) i^i A ) i^i ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) ) = ( ( B vH C ) i^i ( A i^i ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) ) )
28 cmcm2 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A C_H B <-> A C_H ( _|_ ` B ) ) )
29 choccl 
 |-  ( B e. CH -> ( _|_ ` B ) e. CH )
30 cmbr3 
 |-  ( ( A e. CH /\ ( _|_ ` B ) e. CH ) -> ( A C_H ( _|_ ` B ) <-> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( A i^i ( _|_ ` B ) ) ) )
31 29 30 sylan2 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A C_H ( _|_ ` B ) <-> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( A i^i ( _|_ ` B ) ) ) )
32 28 31 bitrd 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A C_H B <-> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( A i^i ( _|_ ` B ) ) ) )
33 32 biimpa 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ A C_H B ) -> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( A i^i ( _|_ ` B ) ) )
34 33 3adantl3 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ A C_H B ) -> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( A i^i ( _|_ ` B ) ) )
35 34 adantrr 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( A i^i ( _|_ ` B ) ) )
36 cmcm2 
 |-  ( ( A e. CH /\ C e. CH ) -> ( A C_H C <-> A C_H ( _|_ ` C ) ) )
37 choccl 
 |-  ( C e. CH -> ( _|_ ` C ) e. CH )
38 cmbr3 
 |-  ( ( A e. CH /\ ( _|_ ` C ) e. CH ) -> ( A C_H ( _|_ ` C ) <-> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) = ( A i^i ( _|_ ` C ) ) ) )
39 37 38 sylan2 
 |-  ( ( A e. CH /\ C e. CH ) -> ( A C_H ( _|_ ` C ) <-> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) = ( A i^i ( _|_ ` C ) ) ) )
40 36 39 bitrd 
 |-  ( ( A e. CH /\ C e. CH ) -> ( A C_H C <-> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) = ( A i^i ( _|_ ` C ) ) ) )
41 40 biimpa 
 |-  ( ( ( A e. CH /\ C e. CH ) /\ A C_H C ) -> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) = ( A i^i ( _|_ ` C ) ) )
42 41 3adantl2 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ A C_H C ) -> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) = ( A i^i ( _|_ ` C ) ) )
43 42 adantrl 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) = ( A i^i ( _|_ ` C ) ) )
44 35 43 ineq12d 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) i^i ( A i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) ) = ( ( A i^i ( _|_ ` B ) ) i^i ( A i^i ( _|_ ` C ) ) ) )
45 inindi 
 |-  ( A i^i ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) ) = ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) i^i ( A i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) )
46 inindi 
 |-  ( A i^i ( ( _|_ ` B ) i^i ( _|_ ` C ) ) ) = ( ( A i^i ( _|_ ` B ) ) i^i ( A i^i ( _|_ ` C ) ) )
47 44 45 46 3eqtr4g 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( A i^i ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) ) = ( A i^i ( ( _|_ ` B ) i^i ( _|_ ` C ) ) ) )
48 47 ineq2d 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( ( B vH C ) i^i ( A i^i ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) ) ) = ( ( B vH C ) i^i ( A i^i ( ( _|_ ` B ) i^i ( _|_ ` C ) ) ) ) )
49 27 48 syl5eq 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( ( ( B vH C ) i^i A ) i^i ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) ) = ( ( B vH C ) i^i ( A i^i ( ( _|_ ` B ) i^i ( _|_ ` C ) ) ) ) )
50 in12 
 |-  ( ( B vH C ) i^i ( A i^i ( ( _|_ ` B ) i^i ( _|_ ` C ) ) ) ) = ( A i^i ( ( B vH C ) i^i ( ( _|_ ` B ) i^i ( _|_ ` C ) ) ) )
51 49 50 eqtrdi 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( ( ( B vH C ) i^i A ) i^i ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) ) = ( A i^i ( ( B vH C ) i^i ( ( _|_ ` B ) i^i ( _|_ ` C ) ) ) ) )
52 chdmj1 
 |-  ( ( B e. CH /\ C e. CH ) -> ( _|_ ` ( B vH C ) ) = ( ( _|_ ` B ) i^i ( _|_ ` C ) ) )
53 52 ineq2d 
 |-  ( ( B e. CH /\ C e. CH ) -> ( ( B vH C ) i^i ( _|_ ` ( B vH C ) ) ) = ( ( B vH C ) i^i ( ( _|_ ` B ) i^i ( _|_ ` C ) ) ) )
54 chocin 
 |-  ( ( B vH C ) e. CH -> ( ( B vH C ) i^i ( _|_ ` ( B vH C ) ) ) = 0H )
55 6 54 syl 
 |-  ( ( B e. CH /\ C e. CH ) -> ( ( B vH C ) i^i ( _|_ ` ( B vH C ) ) ) = 0H )
56 53 55 eqtr3d 
 |-  ( ( B e. CH /\ C e. CH ) -> ( ( B vH C ) i^i ( ( _|_ ` B ) i^i ( _|_ ` C ) ) ) = 0H )
57 56 ineq2d 
 |-  ( ( B e. CH /\ C e. CH ) -> ( A i^i ( ( B vH C ) i^i ( ( _|_ ` B ) i^i ( _|_ ` C ) ) ) ) = ( A i^i 0H ) )
58 chm0 
 |-  ( A e. CH -> ( A i^i 0H ) = 0H )
59 57 58 sylan9eqr 
 |-  ( ( A e. CH /\ ( B e. CH /\ C e. CH ) ) -> ( A i^i ( ( B vH C ) i^i ( ( _|_ ` B ) i^i ( _|_ ` C ) ) ) ) = 0H )
60 59 3impb 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A i^i ( ( B vH C ) i^i ( ( _|_ ` B ) i^i ( _|_ ` C ) ) ) ) = 0H )
61 60 adantr 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( A i^i ( ( B vH C ) i^i ( ( _|_ ` B ) i^i ( _|_ ` C ) ) ) ) = 0H )
62 51 61 eqtrd 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( ( ( B vH C ) i^i A ) i^i ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) ) = 0H )
63 26 62 eqtrd 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( ( A i^i ( B vH C ) ) i^i ( _|_ ` ( ( A i^i B ) vH ( A i^i C ) ) ) ) = 0H )
64 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 ) ) )
65 13 15 63 64 syl12anc 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( ( A i^i B ) vH ( A i^i C ) ) = ( A i^i ( B vH C ) ) )
66 65 eqcomd 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( A i^i ( B vH C ) ) = ( ( A i^i B ) vH ( A i^i C ) ) )