Theorem cdleme35c

Description: Part of proof of Lemma E in Crawley p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013)

	Ref	Expression
Hypotheses	cdleme35.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdleme35.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdleme35.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdleme35.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdleme35.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdleme35.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
	cdleme35.f	⊢ 𝐹 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
Assertion	cdleme35c	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑄 ∨ 𝐹 ) = ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cdleme35.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdleme35.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdleme35.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdleme35.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdleme35.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdleme35.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7		cdleme35.f	⊢ 𝐹 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
8	7	oveq2i	⊢ ( 𝑄 ∨ 𝐹 ) = ( 𝑄 ∨ ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
9		simp11l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐾 ∈ HL )
10		simp13l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑄 ∈ 𝐴 )
11		simp2rl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑅 ∈ 𝐴 )
12		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13		simp12	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
14		simp2l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑃 ≠ 𝑄 )
15	1 2 3 4 5 6	cdleme0a	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → 𝑈 ∈ 𝐴 )
16	12 13 10 14 15	syl112anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑈 ∈ 𝐴 )
17		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
18	17 2 4	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
19	9 11 16 18	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑅 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
20	9	hllatd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐾 ∈ Lat )
21	17 4	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
22	10 21	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
23		simp12l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑃 ∈ 𝐴 )
24	17 2 4	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
25	9 23 11 24	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
26		simp11r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑊 ∈ 𝐻 )
27	17 5	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
28	26 27	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
29	17 3	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
30	20 25 28 29	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
31	17 2	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
32	20 22 30 31	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
33	17 1 2	latlej1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → 𝑄 ≤ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
34	20 22 30 33	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑄 ≤ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
35	17 1 2 3 4	atmod1i1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑄 ≤ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) → ( 𝑄 ∨ ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) ) = ( ( 𝑄 ∨ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
36	9 10 19 32 34 35	syl131anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑄 ∨ ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) ) = ( ( 𝑄 ∨ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
37	1 2 3 4 5 6 7	cdleme35b	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ≤ ( 𝑄 ∨ ( 𝑅 ∨ 𝑈 ) ) )
38	17 2	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∨ ( 𝑅 ∨ 𝑈 ) ) ∈ ( Base ‘ 𝐾 ) )
39	20 22 19 38	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑄 ∨ ( 𝑅 ∨ 𝑈 ) ) ∈ ( Base ‘ 𝐾 ) )
40	17 1 3	latleeqm2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ ( 𝑅 ∨ 𝑈 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ≤ ( 𝑄 ∨ ( 𝑅 ∨ 𝑈 ) ) ↔ ( ( 𝑄 ∨ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) = ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
41	20 32 39 40	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ≤ ( 𝑄 ∨ ( 𝑅 ∨ 𝑈 ) ) ↔ ( ( 𝑄 ∨ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) = ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
42	37 41	mpbid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑄 ∨ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) = ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
43	36 42	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑄 ∨ ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) ) = ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
44	8 43	syl5eq	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑄 ∨ 𝐹 ) = ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )