Metamath Proof Explorer

Theorem lhpmod6i1

Description: Modular law for hyperplanes analogous to complement of atmod2i1 for atoms. (Contributed by NM, 1-Jun-2013)

Ref Expression
Hypotheses lhpmod.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lhpmod.l ⊢ ≤ = ( le ‘ 𝐾 )
lhpmod.j ⊢ ∨ = ( join ‘ 𝐾 )
lhpmod.m ⊢ ∧ = ( meet ‘ 𝐾 )
lhpmod.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpmod6i1 ( ( ( 𝐾 ∈ 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 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
22 7 21 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑊 ) → 𝑊 ∈ 𝐵 )
23 1 2 8 oplecon3b ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑊 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
24 13 14 22 23 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑊 ) → ( 𝑋 ≤ 𝑊 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
25 20 24 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑊 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) )
26 1 2 3 4 9 atmod2i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
27 6 11 16 19 25 26 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑊 ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
28 6 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑊 ) → 𝐾 ∈ Lat )
29 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 )
30 28 17 22 29 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑊 ) → ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 )
31 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑊 ) ) ∈ 𝐵 )
32 28 14 30 31 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑊 ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑊 ) ) ∈ 𝐵 )
33 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
34 28 14 17 33 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑊 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
35 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑊 ) ∈ 𝐵 )
36 28 34 22 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 34 22 41 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑊 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑊 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∨ 𝑌 ) ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) )
43 1 3 4 8 oldmj1 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
44 40 14 17 43 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑊 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
45 44 oveq1d ⊢ ( ( ( 𝐾 ∈ 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 14 30 47 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑊 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ∨ ( 𝑌 ∧ 𝑊 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( 𝑌 ∧ 𝑊 ) ) ) )
49 1 3 4 8 oldmm1 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑌 ∧ 𝑊 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) )
50 40 17 22 49 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑊 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑌 ∧ 𝑊 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∨ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) )
51 50 oveq2d ⊢ ( ( ( 𝐾 ∈ 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 27 54 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑊 ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑊 ) ) = ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑊 ) )