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 ) ) )