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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) → ( 𝐹 ‘ ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ) = ( ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( 𝐹 ‘ 𝑉 ) ) ) )