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

Metamath Proof Explorer

Theorem mdslj1i

Description: Join preservation of the one-to-one onto mapping between the two sublattices in Lemma 1.3 of MaedaMaeda p. 2. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses mdslle1.1 ⊢ 𝐴 ∈ Cℋ
mdslle1.2 ⊢ 𝐵 ∈ Cℋ
mdslle1.3 ⊢ 𝐶 ∈ Cℋ
mdslle1.4 ⊢ 𝐷 ∈ Cℋ
Assertion mdslj1i ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∨ℋ 𝐷 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 mdslle1.1 ⊢ 𝐴 ∈ Cℋ
2 mdslle1.2 ⊢ 𝐵 ∈ Cℋ
3 mdslle1.3 ⊢ 𝐶 ∈ Cℋ
4 mdslle1.4 ⊢ 𝐷 ∈ Cℋ
5 ssin ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ↔ 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) )
6 5 bicomi ⊢ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ↔ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) )
7 1 2 chjcli ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
8 3 4 7 chlubi ⊢ ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
9 8 bicomi ⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
10 6 9 anbi12i ⊢ ( ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
11 simpr ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) → 𝐵 𝑀ℋ* 𝐴 )
12 simpl ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) → 𝐴 ⊆ 𝐶 )
13 simpl ⊢ ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
14 1 2 3 3pm3.2i ⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ )
15 dmdsl3 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐶 )
16 14 15 mpan ⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐶 )
17 11 12 13 16 syl3an ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐶 )
18 3 2 chincli ⊢ ( 𝐶 ∩ 𝐵 ) ∈ Cℋ
19 4 2 chincli ⊢ ( 𝐷 ∩ 𝐵 ) ∈ Cℋ
20 18 19 chub1i ⊢ ( 𝐶 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) )
21 18 19 chjcli ⊢ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∈ Cℋ
22 18 21 1 chlej1i ⊢ ( ( 𝐶 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ 𝐴 ) ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) )
23 20 22 mp1i ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ 𝐴 ) ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) )
24 17 23 eqsstrrd ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → 𝐶 ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) )
25 simpr ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) → 𝐴 ⊆ 𝐷 )
26 simpr ⊢ ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
27 1 2 4 3pm3.2i ⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ )
28 dmdsl3 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ∧ ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐷 ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐷 )
29 27 28 mpan ⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐷 ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐷 )
30 11 25 26 29 syl3an ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐷 )
31 19 18 chub2i ⊢ ( 𝐷 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) )
32 19 21 1 chlej1i ⊢ ( ( 𝐷 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) )
33 31 32 mp1i ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) )
34 30 33 eqsstrrd ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → 𝐷 ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) )
35 24 34 jca ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( 𝐶 ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∧ 𝐷 ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ) )
36 21 1 chjcli ⊢ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∈ Cℋ
37 3 4 36 chlubi ⊢ ( ( 𝐶 ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∧ 𝐷 ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ) ↔ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) )
38 35 37 sylib ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) )
39 38 ssrind ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∨ℋ 𝐷 ) ∩ 𝐵 ) ⊆ ( ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) )
40 simpl ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) → 𝐴 𝑀ℋ 𝐵 )
41 ssrin ⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐵 ) )
42 41 20 sstrdi ⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )
43 42 adantr ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )
44 inss2 ⊢ ( 𝐶 ∩ 𝐵 ) ⊆ 𝐵
45 inss2 ⊢ ( 𝐷 ∩ 𝐵 ) ⊆ 𝐵
46 18 19 2 chlubi ⊢ ( ( ( 𝐶 ∩ 𝐵 ) ⊆ 𝐵 ∧ ( 𝐷 ∩ 𝐵 ) ⊆ 𝐵 ) ↔ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝐵 )
47 46 bicomi ⊢ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝐵 ↔ ( ( 𝐶 ∩ 𝐵 ) ⊆ 𝐵 ∧ ( 𝐷 ∩ 𝐵 ) ⊆ 𝐵 ) )
48 44 45 47 mpbir2an ⊢ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝐵
49 48 a1i ⊢ ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝐵 )
50 1 2 21 3pm3.2i ⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∈ Cℋ )
51 mdsl3 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∧ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝐵 ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )
52 50 51 mpan ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∧ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝐵 ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )
53 40 43 49 52 syl3an ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )
54 39 53 sseqtrd ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∨ℋ 𝐷 ) ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )
55 54 3expb ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( 𝐶 ∨ℋ 𝐷 ) ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )
56 10 55 sylan2b ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∨ℋ 𝐷 ) ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )
57 3 4 2 lediri ⊢ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝐶 ∨ℋ 𝐷 ) ∩ 𝐵 )
58 57 a1i ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝐶 ∨ℋ 𝐷 ) ∩ 𝐵 ) )
59 56 58 eqssd ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∨ℋ 𝐷 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )