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

Metamath Proof Explorer

Theorem pl42lem1N

Description: Lemma for pl42N . (Contributed by NM, 8-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pl42lem.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
pl42lem.l ⊢ ≤ = ( le ‘ 𝐾 )
pl42lem.j ⊢ ∨ = ( join ‘ 𝐾 )
pl42lem.m ⊢ ∧ = ( meet ‘ 𝐾 )
pl42lem.o ⊢ ⊥ = ( oc ‘ 𝐾 )
pl42lem.f ⊢ 𝐹 = ( pmap ‘ 𝐾 )
pl42lem.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion pl42lem1N ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) → ( 𝐹 ‘ ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ) = ( ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( 𝐹 ‘ 𝑉 ) ) ) )

Proof

Step Hyp Ref Expression
1 pl42lem.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 pl42lem.l ⊢ ≤ = ( le ‘ 𝐾 )
3 pl42lem.j ⊢ ∨ = ( join ‘ 𝐾 )
4 pl42lem.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 pl42lem.o ⊢ ⊥ = ( oc ‘ 𝐾 )
6 pl42lem.f ⊢ 𝐹 = ( pmap ‘ 𝐾 )
7 pl42lem.p ⊢ + = ( +𝑃 ‘ 𝐾 )
8 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → 𝐾 ∈ HL )
9 8 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → 𝐾 ∈ Lat )
10 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → 𝑋 ∈ 𝐵 )
11 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → 𝑌 ∈ 𝐵 )
12 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
13 9 10 11 12 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
14 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → 𝑍 ∈ 𝐵 )
15 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∈ 𝐵 )
16 9 13 14 15 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∈ 𝐵 )
17 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → 𝑊 ∈ 𝐵 )
18 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∈ 𝐵 )
19 9 16 17 18 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∈ 𝐵 )
20 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → 𝑉 ∈ 𝐵 )
21 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
22 1 4 21 6 pmapmeet ⊢ ( ( 𝐾 ∈ HL ∧ ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝐹 ‘ ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ) = ( ( 𝐹 ‘ ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ) ∩ ( 𝐹 ‘ 𝑉 ) ) )
23 8 19 20 22 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( 𝐹 ‘ ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ) = ( ( 𝐹 ‘ ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ) ∩ ( 𝐹 ‘ 𝑉 ) ) )
24 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
25 8 24 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → 𝐾 ∈ OP )
26 1 5 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑊 ∈ 𝐵 ) → ( ⊥ ‘ 𝑊 ) ∈ 𝐵 )
27 25 17 26 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( ⊥ ‘ 𝑊 ) ∈ 𝐵 )
28 1 2 4 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ≤ 𝑍 )
29 9 13 14 28 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ≤ 𝑍 )
30 simp3r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → 𝑍 ≤ ( ⊥ ‘ 𝑊 ) )
31 1 2 9 16 14 27 29 30 lattrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ≤ ( ⊥ ‘ 𝑊 ) )
32 1 2 3 6 5 7 pmapojoinN ⊢ ( ( ( 𝐾 ∈ HL ∧ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ≤ ( ⊥ ‘ 𝑊 ) ) → ( 𝐹 ‘ ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ) = ( ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) )
33 8 16 17 31 32 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( 𝐹 ‘ ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ) = ( ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) )
34 1 4 21 6 pmapmeet ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) = ( ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) )
35 8 13 14 34 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) = ( ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) )
36 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → 𝑋 ≤ ( ⊥ ‘ 𝑌 ) )
37 1 2 3 6 5 7 pmapojoinN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ) → ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) )
38 8 10 11 36 37 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) )
39 38 ineq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) = ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) )
40 35 39 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) = ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) )
41 40 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) = ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) )
42 33 41 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( 𝐹 ‘ ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ) = ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) )
43 42 ineq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( ( 𝐹 ‘ ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ) ∩ ( 𝐹 ‘ 𝑉 ) ) = ( ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( 𝐹 ‘ 𝑉 ) ) )
44 23 43 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( 𝐹 ‘ ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ) = ( ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( 𝐹 ‘ 𝑉 ) ) )
45 44 3expia ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) → ( 𝐹 ‘ ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ) = ( ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( 𝐹 ‘ 𝑉 ) ) ) )