This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cm2j

Description: A lattice element that commutes with two others also commutes with their join. Theorem 4.2 of Beran p. 49. (Contributed by NM, 15-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion cm2j ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ) → 𝐴 𝐶ℋ ( 𝐵 ∨ℋ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 cmcm ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐵 𝐶ℋ 𝐴 ) )
2 cmbr ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝐵 𝐶ℋ 𝐴 ↔ 𝐵 = ( ( 𝐵 ∩ 𝐴 ) ∨ℋ ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) ) ) )
3 2 ancoms ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐵 𝐶ℋ 𝐴 ↔ 𝐵 = ( ( 𝐵 ∩ 𝐴 ) ∨ℋ ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) ) ) )
4 1 3 bitrd ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐵 = ( ( 𝐵 ∩ 𝐴 ) ∨ℋ ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) ) ) )
5 4 biimpa ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝐴 𝐶ℋ 𝐵 ) → 𝐵 = ( ( 𝐵 ∩ 𝐴 ) ∨ℋ ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) ) )
6 incom ⊢ ( 𝐵 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐵 )
7 incom ⊢ ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 )
8 6 7 oveq12i ⊢ ( ( 𝐵 ∩ 𝐴 ) ∨ℋ ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) ) = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) )
9 5 8 eqtrdi ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝐴 𝐶ℋ 𝐵 ) → 𝐵 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) )
10 9 3adantl3 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ 𝐴 𝐶ℋ 𝐵 ) → 𝐵 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) )
11 10 adantrr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ) → 𝐵 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) )
12 cmcm ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 𝐶ℋ 𝐶 ↔ 𝐶 𝐶ℋ 𝐴 ) )
13 cmbr ⊢ ( ( 𝐶 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝐶 𝐶ℋ 𝐴 ↔ 𝐶 = ( ( 𝐶 ∩ 𝐴 ) ∨ℋ ( 𝐶 ∩ ( ⊥ ‘ 𝐴 ) ) ) ) )
14 13 ancoms ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐶 𝐶ℋ 𝐴 ↔ 𝐶 = ( ( 𝐶 ∩ 𝐴 ) ∨ℋ ( 𝐶 ∩ ( ⊥ ‘ 𝐴 ) ) ) ) )
15 12 14 bitrd ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 𝐶ℋ 𝐶 ↔ 𝐶 = ( ( 𝐶 ∩ 𝐴 ) ∨ℋ ( 𝐶 ∩ ( ⊥ ‘ 𝐴 ) ) ) ) )
16 15 biimpa ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ 𝐴 𝐶ℋ 𝐶 ) → 𝐶 = ( ( 𝐶 ∩ 𝐴 ) ∨ℋ ( 𝐶 ∩ ( ⊥ ‘ 𝐴 ) ) ) )
17 incom ⊢ ( 𝐶 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐶 )
18 incom ⊢ ( 𝐶 ∩ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 )
19 17 18 oveq12i ⊢ ( ( 𝐶 ∩ 𝐴 ) ∨ℋ ( 𝐶 ∩ ( ⊥ ‘ 𝐴 ) ) ) = ( ( 𝐴 ∩ 𝐶 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) )
20 16 19 eqtrdi ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ 𝐴 𝐶ℋ 𝐶 ) → 𝐶 = ( ( 𝐴 ∩ 𝐶 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ) )
21 20 3adantl2 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ 𝐴 𝐶ℋ 𝐶 ) → 𝐶 = ( ( 𝐴 ∩ 𝐶 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ) )
22 21 adantrl ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ) → 𝐶 = ( ( 𝐴 ∩ 𝐶 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ) )
23 11 22 oveq12d ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ) → ( 𝐵 ∨ℋ 𝐶 ) = ( ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) ∨ℋ ( ( 𝐴 ∩ 𝐶 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ) ) )
24 chincl ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∩ 𝐵 ) ∈ Cℋ )
25 choccl ⊢ ( 𝐴 ∈ Cℋ → ( ⊥ ‘ 𝐴 ) ∈ Cℋ )
26 chincl ⊢ ( ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∈ Cℋ )
27 25 26 sylan ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∈ Cℋ )
28 24 27 jca ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∈ Cℋ ) )
29 chincl ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ∩ 𝐶 ) ∈ Cℋ )
30 chincl ⊢ ( ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ∈ Cℋ )
31 25 30 sylan ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ∈ Cℋ )
32 29 31 jca ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝐶 ) ∈ Cℋ ∧ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ∈ Cℋ ) )
33 chj4 ⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∈ Cℋ ) ∧ ( ( 𝐴 ∩ 𝐶 ) ∈ Cℋ ∧ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ∈ Cℋ ) ) → ( ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) ∨ℋ ( ( 𝐴 ∩ 𝐶 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ) ) = ( ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ∨ℋ ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ) ) )
34 28 32 33 syl2an ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ) → ( ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) ∨ℋ ( ( 𝐴 ∩ 𝐶 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ) ) = ( ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ∨ℋ ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ) ) )
35 34 3impdi ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) ∨ℋ ( ( 𝐴 ∩ 𝐶 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ) ) = ( ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ∨ℋ ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ) ) )
36 35 adantr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ) → ( ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) ∨ℋ ( ( 𝐴 ∩ 𝐶 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ) ) = ( ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ∨ℋ ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ) ) )
37 fh1 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ) → ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) )
38 incom ⊢ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) ) = ( ( 𝐵 ∨ℋ 𝐶 ) ∩ 𝐴 )
39 37 38 eqtr3di ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) = ( ( 𝐵 ∨ℋ 𝐶 ) ∩ 𝐴 ) )
40 25 3anim1i ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) )
41 40 adantr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ) → ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) )
42 cmcm3 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝐶ℋ 𝐵 ↔ ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐵 ) )
43 42 3adant3 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 𝐶ℋ 𝐵 ↔ ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐵 ) )
44 cmcm3 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 𝐶ℋ 𝐶 ↔ ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐶 ) )
45 44 3adant2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 𝐶ℋ 𝐶 ↔ ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐶 ) )
46 43 45 anbi12d ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ↔ ( ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐵 ∧ ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐶 ) ) )
47 46 biimpa ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ) → ( ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐵 ∧ ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐶 ) )
48 fh1 ⊢ ( ( ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐵 ∧ ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐶 ) ) → ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ) )
49 41 47 48 syl2anc ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ) → ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ) )
50 incom ⊢ ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) ) = ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( ⊥ ‘ 𝐴 ) )
51 49 50 eqtr3di ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ) → ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ) = ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( ⊥ ‘ 𝐴 ) ) )
52 39 51 oveq12d ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ) → ( ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ∨ℋ ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐶 ) ) ) = ( ( ( 𝐵 ∨ℋ 𝐶 ) ∩ 𝐴 ) ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( ⊥ ‘ 𝐴 ) ) ) )
53 23 36 52 3eqtrd ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ) → ( 𝐵 ∨ℋ 𝐶 ) = ( ( ( 𝐵 ∨ℋ 𝐶 ) ∩ 𝐴 ) ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( ⊥ ‘ 𝐴 ) ) ) )
54 53 ex ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) → ( 𝐵 ∨ℋ 𝐶 ) = ( ( ( 𝐵 ∨ℋ 𝐶 ) ∩ 𝐴 ) ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( ⊥ ‘ 𝐴 ) ) ) ) )
55 chjcl ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐵 ∨ℋ 𝐶 ) ∈ Cℋ )
56 cmcm ⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐵 ∨ℋ 𝐶 ) ∈ Cℋ ) → ( 𝐴 𝐶ℋ ( 𝐵 ∨ℋ 𝐶 ) ↔ ( 𝐵 ∨ℋ 𝐶 ) 𝐶ℋ 𝐴 ) )
57 cmbr ⊢ ( ( ( 𝐵 ∨ℋ 𝐶 ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( ( 𝐵 ∨ℋ 𝐶 ) 𝐶ℋ 𝐴 ↔ ( 𝐵 ∨ℋ 𝐶 ) = ( ( ( 𝐵 ∨ℋ 𝐶 ) ∩ 𝐴 ) ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( ⊥ ‘ 𝐴 ) ) ) ) )
58 57 ancoms ⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐵 ∨ℋ 𝐶 ) ∈ Cℋ ) → ( ( 𝐵 ∨ℋ 𝐶 ) 𝐶ℋ 𝐴 ↔ ( 𝐵 ∨ℋ 𝐶 ) = ( ( ( 𝐵 ∨ℋ 𝐶 ) ∩ 𝐴 ) ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( ⊥ ‘ 𝐴 ) ) ) ) )
59 56 58 bitrd ⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐵 ∨ℋ 𝐶 ) ∈ Cℋ ) → ( 𝐴 𝐶ℋ ( 𝐵 ∨ℋ 𝐶 ) ↔ ( 𝐵 ∨ℋ 𝐶 ) = ( ( ( 𝐵 ∨ℋ 𝐶 ) ∩ 𝐴 ) ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( ⊥ ‘ 𝐴 ) ) ) ) )
60 55 59 sylan2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ) → ( 𝐴 𝐶ℋ ( 𝐵 ∨ℋ 𝐶 ) ↔ ( 𝐵 ∨ℋ 𝐶 ) = ( ( ( 𝐵 ∨ℋ 𝐶 ) ∩ 𝐴 ) ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( ⊥ ‘ 𝐴 ) ) ) ) )
61 60 3impb ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 𝐶ℋ ( 𝐵 ∨ℋ 𝐶 ) ↔ ( 𝐵 ∨ℋ 𝐶 ) = ( ( ( 𝐵 ∨ℋ 𝐶 ) ∩ 𝐴 ) ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( ⊥ ‘ 𝐴 ) ) ) ) )
62 54 61 sylibrd ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) → 𝐴 𝐶ℋ ( 𝐵 ∨ℋ 𝐶 ) ) )
63 62 imp ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ) → 𝐴 𝐶ℋ ( 𝐵 ∨ℋ 𝐶 ) )