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

Metamath Proof Explorer

Theorem lhpmod2i2

Description: Modular law for hyperplanes analogous to atmod2i2 for atoms. (Contributed by NM, 9-Feb-2013)

Ref Expression
Hypotheses lhpmod.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lhpmod.l ⊢ ≤ = ( le ‘ 𝐾 )
lhpmod.j ⊢ ∨ = ( join ‘ 𝐾 )
lhpmod.m ⊢ ∧ = ( meet ‘ 𝐾 )
lhpmod.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpmod2i2 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( 𝑋 ∧ 𝑊 ) ∨ 𝑌 ) = ( 𝑋 ∧ ( 𝑊 ∨ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 lhpmod.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lhpmod.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lhpmod.j ⊢ ∨ = ( join ‘ 𝐾 )
4 lhpmod.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 lhpmod.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → 𝐾 ∈ HL )
7 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → 𝑊 ∈ 𝐻 )
8 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
9 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
10 8 9 5 lhpocat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) )
11 6 7 10 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) )
12 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
13 6 12 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → 𝐾 ∈ OP )
14 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → 𝑋 ∈ 𝐵 )
15 1 8 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
16 13 14 15 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
17 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → 𝑌 ∈ 𝐵 )
18 1 8 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 )
19 13 17 18 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 )
20 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → 𝑌 ≤ 𝑋 )
21 1 2 8 oplecon3b ⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 ≤ 𝑋 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
22 13 17 14 21 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( 𝑌 ≤ 𝑋 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
23 20 22 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) )
24 1 2 3 4 9 atmod1i2 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
25 6 11 16 19 23 24 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
26 6 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → 𝐾 ∈ Lat )
27 1 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
28 7 27 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → 𝑊 ∈ 𝐵 )
29 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
30 26 14 28 29 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
31 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑊 ) ∨ 𝑌 ) ∈ 𝐵 )
32 26 30 17 31 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( 𝑋 ∧ 𝑊 ) ∨ 𝑌 ) ∈ 𝐵 )
33 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑊 ∨ 𝑌 ) ∈ 𝐵 )
34 26 28 17 33 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( 𝑊 ∨ 𝑌 ) ∈ 𝐵 )
35 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑊 ∨ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 ∧ ( 𝑊 ∨ 𝑌 ) ) ∈ 𝐵 )
36 26 14 34 35 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( 𝑋 ∧ ( 𝑊 ∨ 𝑌 ) ) ∈ 𝐵 )
37 1 8 opcon3b ⊢ ( ( 𝐾 ∈ OP ∧ ( ( 𝑋 ∧ 𝑊 ) ∨ 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ∧ ( 𝑊 ∨ 𝑌 ) ) ∈ 𝐵 ) → ( ( ( 𝑋 ∧ 𝑊 ) ∨ 𝑌 ) = ( 𝑋 ∧ ( 𝑊 ∨ 𝑌 ) ) ↔ ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ ( 𝑊 ∨ 𝑌 ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 ∧ 𝑊 ) ∨ 𝑌 ) ) ) )
38 13 32 36 37 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( ( 𝑋 ∧ 𝑊 ) ∨ 𝑌 ) = ( 𝑋 ∧ ( 𝑊 ∨ 𝑌 ) ) ↔ ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ ( 𝑊 ∨ 𝑌 ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 ∧ 𝑊 ) ∨ 𝑌 ) ) ) )
39 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
40 6 39 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → 𝐾 ∈ OL )
41 1 3 4 8 oldmm1 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑊 ∨ 𝑌 ) ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ ( 𝑊 ∨ 𝑌 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ ( 𝑊 ∨ 𝑌 ) ) ) )
42 40 14 34 41 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ ( 𝑊 ∨ 𝑌 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ ( 𝑊 ∨ 𝑌 ) ) ) )
43 1 3 4 8 oldmj1 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑊 ∨ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
44 40 28 17 43 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑊 ∨ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
45 44 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ ( 𝑊 ∨ 𝑌 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
46 42 45 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ ( 𝑊 ∨ 𝑌 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
47 1 3 4 8 oldmj1 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 ∧ 𝑊 ) ∨ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑊 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
48 40 30 17 47 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 ∧ 𝑊 ) ∨ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑊 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
49 1 3 4 8 oldmm1 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑊 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) )
50 40 14 28 49 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑊 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) )
51 50 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ 𝑊 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
52 48 51 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 ∧ 𝑊 ) ∨ 𝑌 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
53 46 52 eqeq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∧ ( 𝑊 ∨ 𝑌 ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 ∧ 𝑊 ) ∨ 𝑌 ) ) ↔ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
54 38 53 bitrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( ( 𝑋 ∧ 𝑊 ) ∨ 𝑌 ) = ( 𝑋 ∧ ( 𝑊 ∨ 𝑌 ) ) ↔ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
55 25 54 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑌 ≤ 𝑋 ) → ( ( 𝑋 ∧ 𝑊 ) ∨ 𝑌 ) = ( 𝑋 ∧ ( 𝑊 ∨ 𝑌 ) ) )