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 ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ) → ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) )

Proof

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