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 ( ( ( 𝐴 ∈ 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 chdmj1 ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ ( 𝐴 ∩ 𝐶 ) ∈ Cℋ ) → ( ⊥ ‘ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ) = ( ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) )
17 1 2 16 syl2an ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ) → ( ⊥ ‘ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ) = ( ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) )
18 chdmm1 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) = ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) )
19 18 adantr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ) → ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) = ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) )
20 19 ineq1d ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ) → ( ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) )
21 17 20 eqtrd ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ) → ( ⊥ ‘ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) )
22 21 3impdi ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ⊥ ‘ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) )
23 22 ineq2d ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∩ ( ⊥ ‘ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ) ) = ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∩ ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) )
24 23 adantr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶 ) ) → ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∩ ( ⊥ ‘ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ) ) = ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∩ ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) )
25 in4 ⊢ ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∩ ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) = ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∩ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) )
26 cmcm2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 𝐶ℋ ( ⊥ ‘ 𝐵 ) ) )
27 cmcm ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐵 𝐶ℋ 𝐴 ) )
28 choccl ⊢ ( 𝐵 ∈ Cℋ → ( ⊥ ‘ 𝐵 ) ∈ Cℋ )
29 cmbr3 ⊢ ( ( 𝐴 ∈ Cℋ ∧ ( ⊥ ‘ 𝐵 ) ∈ Cℋ ) → ( 𝐴 𝐶ℋ ( ⊥ ‘ 𝐵 ) ↔ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) )
30 28 29 sylan2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝐶ℋ ( ⊥ ‘ 𝐵 ) ↔ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) )
31 26 27 30 3bitr3d ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐵 𝐶ℋ 𝐴 ↔ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) )
32 31 biimpa ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝐵 𝐶ℋ 𝐴 ) → ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) )
33 incom ⊢ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ 𝐴 )
34 32 33 eqtrdi ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝐵 𝐶ℋ 𝐴 ) → ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ 𝐴 ) )
35 34 3adantl3 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ 𝐵 𝐶ℋ 𝐴 ) → ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ 𝐴 ) )
36 35 adantrr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶 ) ) → ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ 𝐴 ) )
37 36 ineq1d ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶 ) ) → ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∩ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) = ( ( ( ⊥ ‘ 𝐵 ) ∩ 𝐴 ) ∩ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) )
38 25 37 eqtrid ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶 ) ) → ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∩ ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) = ( ( ( ⊥ ‘ 𝐵 ) ∩ 𝐴 ) ∩ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) )
39 24 38 eqtrd ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶 ) ) → ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∩ ( ⊥ ‘ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ) ) = ( ( ( ⊥ ‘ 𝐵 ) ∩ 𝐴 ) ∩ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) )
40 in4 ⊢ ( ( ( ⊥ ‘ 𝐵 ) ∩ 𝐴 ) ∩ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) = ( ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∩ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) )
41 39 40 eqtrdi ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶 ) ) → ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∩ ( ⊥ ‘ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ) ) = ( ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∩ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) )
42 ococ ⊢ ( 𝐵 ∈ Cℋ → ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) = 𝐵 )
43 42 oveq1d ⊢ ( 𝐵 ∈ Cℋ → ( ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ∨ℋ 𝐶 ) = ( 𝐵 ∨ℋ 𝐶 ) )
44 43 ineq2d ⊢ ( 𝐵 ∈ Cℋ → ( ( ⊥ ‘ 𝐵 ) ∩ ( ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ∨ℋ 𝐶 ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) ) )
45 44 3ad2ant2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐵 ) ∩ ( ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ∨ℋ 𝐶 ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) ) )
46 45 adantr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶 ) ) → ( ( ⊥ ‘ 𝐵 ) ∩ ( ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ∨ℋ 𝐶 ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) ) )
47 cmcm3 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐵 𝐶ℋ 𝐶 ↔ ( ⊥ ‘ 𝐵 ) 𝐶ℋ 𝐶 ) )
48 cmbr3 ⊢ ( ( ( ⊥ ‘ 𝐵 ) ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐵 ) 𝐶ℋ 𝐶 ↔ ( ( ⊥ ‘ 𝐵 ) ∩ ( ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ∨ℋ 𝐶 ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ 𝐶 ) ) )
49 28 48 sylan ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐵 ) 𝐶ℋ 𝐶 ↔ ( ( ⊥ ‘ 𝐵 ) ∩ ( ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ∨ℋ 𝐶 ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ 𝐶 ) ) )
50 47 49 bitrd ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐵 𝐶ℋ 𝐶 ↔ ( ( ⊥ ‘ 𝐵 ) ∩ ( ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ∨ℋ 𝐶 ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ 𝐶 ) ) )
51 50 biimpa ⊢ ( ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ 𝐵 𝐶ℋ 𝐶 ) → ( ( ⊥ ‘ 𝐵 ) ∩ ( ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ∨ℋ 𝐶 ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ 𝐶 ) )
52 51 3adantl1 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ 𝐵 𝐶ℋ 𝐶 ) → ( ( ⊥ ‘ 𝐵 ) ∩ ( ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ∨ℋ 𝐶 ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ 𝐶 ) )
53 52 adantrl ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶 ) ) → ( ( ⊥ ‘ 𝐵 ) ∩ ( ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ∨ℋ 𝐶 ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ 𝐶 ) )
54 46 53 eqtr3d ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶 ) ) → ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ 𝐶 ) )
55 54 ineq1d ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶 ) ) → ( ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∩ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) = ( ( ( ⊥ ‘ 𝐵 ) ∩ 𝐶 ) ∩ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) )
56 inass ⊢ ( ( ( ⊥ ‘ 𝐵 ) ∩ 𝐶 ) ∩ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐶 ∩ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) )
57 in12 ⊢ ( 𝐶 ∩ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) = ( 𝐴 ∩ ( 𝐶 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) )
58 inass ⊢ ( ( 𝐴 ∩ 𝐶 ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) = ( 𝐴 ∩ ( 𝐶 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) )
59 57 58 eqtr4i ⊢ ( 𝐶 ∩ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) = ( ( 𝐴 ∩ 𝐶 ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) )
60 chocin ⊢ ( ( 𝐴 ∩ 𝐶 ) ∈ Cℋ → ( ( 𝐴 ∩ 𝐶 ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) = 0ℋ )
61 2 60 syl ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝐶 ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) = 0ℋ )
62 59 61 eqtrid ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐶 ∩ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) = 0ℋ )
63 62 ineq2d ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐶 ∩ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ 0ℋ ) )
64 56 63 eqtrid ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝐵 ) ∩ 𝐶 ) ∩ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ 0ℋ ) )
65 64 3adant2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝐵 ) ∩ 𝐶 ) ∩ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ 0ℋ ) )
66 chm0 ⊢ ( ( ⊥ ‘ 𝐵 ) ∈ Cℋ → ( ( ⊥ ‘ 𝐵 ) ∩ 0ℋ ) = 0ℋ )
67 28 66 syl ⊢ ( 𝐵 ∈ Cℋ → ( ( ⊥ ‘ 𝐵 ) ∩ 0ℋ ) = 0ℋ )
68 67 3ad2ant2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐵 ) ∩ 0ℋ ) = 0ℋ )
69 65 68 eqtrd ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝐵 ) ∩ 𝐶 ) ∩ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) = 0ℋ )
70 69 adantr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶 ) ) → ( ( ( ⊥ ‘ 𝐵 ) ∩ 𝐶 ) ∩ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) = 0ℋ )
71 55 70 eqtrd ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶 ) ) → ( ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∩ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) ) = 0ℋ )
72 41 71 eqtrd ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶 ) ) → ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∩ ( ⊥ ‘ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ) ) = 0ℋ )
73 pjoml ⊢ ( ( ( ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ∈ Cℋ ∧ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∈ Sℋ ) ∧ ( ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ⊆ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∧ ( ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∩ ( ⊥ ‘ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ) ) = 0ℋ ) ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) = ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) )
74 13 15 72 73 syl12anc ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶 ) ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) = ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) )
75 74 eqcomd ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶 ) ) → ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) )