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

Metamath Proof Explorer

Theorem cdleme1

Description: Part of proof of Lemma E in Crawley p. 113. F represents their f(r). Here we show r \/ f(r) = r \/ u (7th through 5th lines from bottom on p. 113). (Contributed by NM, 4-Jun-2012)

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

Proof

Step Hyp Ref Expression
1 cdleme1.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdleme1.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdleme1.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cdleme1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme1.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7 cdleme1.f ⊢ 𝐹 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
8 7 oveq2i ⊢ ( 𝑅 ∨ 𝐹 ) = ( 𝑅 ∨ ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
9 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → 𝐾 ∈ HL )
10 simpr3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → 𝑅 ∈ 𝐴 )
11 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
12 11 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → 𝐾 ∈ Lat )
13 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14 13 4 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
15 10 14 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
16 simpr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → 𝑃 ∈ 𝐴 )
17 13 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
18 16 17 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
19 simpr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → 𝑄 ∈ 𝐴 )
20 13 4 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
21 19 20 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
22 13 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
23 12 18 21 22 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
24 13 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
25 24 ad2antlr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
26 13 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
27 12 23 25 26 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
28 6 27 eqeltrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → 𝑈 ∈ ( Base ‘ 𝐾 ) )
29 13 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑅 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
30 12 15 28 29 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( 𝑅 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
31 13 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
32 12 18 15 31 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
33 13 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
34 12 32 25 33 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
35 13 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
36 12 21 34 35 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
37 13 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) → 𝑅 ≤ ( 𝑅 ∨ 𝑈 ) )
38 12 15 28 37 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → 𝑅 ≤ ( 𝑅 ∨ 𝑈 ) )
39 13 1 2 3 4 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑅 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑅 ≤ ( 𝑅 ∨ 𝑈 ) ) → ( 𝑅 ∨ ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) ) = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑅 ∨ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) ) )
40 9 10 30 36 38 39 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( 𝑅 ∨ ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) ) = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑅 ∨ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) ) )
41 13 1 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → 𝑅 ≤ ( 𝑃 ∨ 𝑅 ) )
42 12 18 15 41 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → 𝑅 ≤ ( 𝑃 ∨ 𝑅 ) )
43 13 1 2 3 4 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑅 ) ) → ( 𝑅 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑅 ) ∧ ( 𝑅 ∨ 𝑊 ) ) )
44 9 10 32 25 42 43 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( 𝑅 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑅 ) ∧ ( 𝑅 ∨ 𝑊 ) ) )
45 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
46 1 2 45 4 5 lhpjat2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝑅 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
47 46 3ad2antr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( 𝑅 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
48 47 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑅 ) ∧ ( 𝑅 ∨ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑅 ) ∧ ( 1. ‘ 𝐾 ) ) )
49 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
50 49 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → 𝐾 ∈ OL )
51 13 3 45 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑅 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ 𝑅 ) )
52 50 32 51 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑅 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ 𝑅 ) )
53 44 48 52 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( 𝑅 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) = ( 𝑃 ∨ 𝑅 ) )
54 53 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( 𝑄 ∨ ( 𝑅 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) = ( 𝑄 ∨ ( 𝑃 ∨ 𝑅 ) ) )
55 13 2 latj12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑄 ∨ ( 𝑅 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) = ( 𝑅 ∨ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
56 12 21 15 34 55 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( 𝑄 ∨ ( 𝑅 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) = ( 𝑅 ∨ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
57 13 2 latj13 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑄 ∨ ( 𝑃 ∨ 𝑅 ) ) = ( 𝑅 ∨ ( 𝑃 ∨ 𝑄 ) ) )
58 12 21 18 15 57 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( 𝑄 ∨ ( 𝑃 ∨ 𝑅 ) ) = ( 𝑅 ∨ ( 𝑃 ∨ 𝑄 ) ) )
59 54 56 58 3eqtr3rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( 𝑅 ∨ ( 𝑃 ∨ 𝑄 ) ) = ( 𝑅 ∨ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
60 59 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑅 ∨ ( 𝑃 ∨ 𝑄 ) ) ) = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑅 ∨ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) ) )
61 1 2 3 4 5 6 cdlemeulpq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑈 ≤ ( 𝑃 ∨ 𝑄 ) )
62 61 3adantr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → 𝑈 ≤ ( 𝑃 ∨ 𝑄 ) )
63 13 1 2 latjlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑈 ≤ ( 𝑃 ∨ 𝑄 ) → ( 𝑅 ∨ 𝑈 ) ≤ ( 𝑅 ∨ ( 𝑃 ∨ 𝑄 ) ) ) )
64 12 28 23 15 63 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( 𝑈 ≤ ( 𝑃 ∨ 𝑄 ) → ( 𝑅 ∨ 𝑈 ) ≤ ( 𝑅 ∨ ( 𝑃 ∨ 𝑄 ) ) ) )
65 62 64 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( 𝑅 ∨ 𝑈 ) ≤ ( 𝑅 ∨ ( 𝑃 ∨ 𝑄 ) ) )
66 13 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑅 ∨ ( 𝑃 ∨ 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) )
67 12 15 23 66 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( 𝑅 ∨ ( 𝑃 ∨ 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) )
68 13 1 3 latleeqm1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ∨ ( 𝑃 ∨ 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ∨ 𝑈 ) ≤ ( 𝑅 ∨ ( 𝑃 ∨ 𝑄 ) ) ↔ ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑅 ∨ ( 𝑃 ∨ 𝑄 ) ) ) = ( 𝑅 ∨ 𝑈 ) ) )
69 12 30 67 68 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( ( 𝑅 ∨ 𝑈 ) ≤ ( 𝑅 ∨ ( 𝑃 ∨ 𝑄 ) ) ↔ ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑅 ∨ ( 𝑃 ∨ 𝑄 ) ) ) = ( 𝑅 ∨ 𝑈 ) ) )
70 65 69 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑅 ∨ ( 𝑃 ∨ 𝑄 ) ) ) = ( 𝑅 ∨ 𝑈 ) )
71 40 60 70 3eqtr2rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( 𝑅 ∨ 𝑈 ) = ( 𝑅 ∨ ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) ) )
72 8 71 eqtr4id ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ) → ( 𝑅 ∨ 𝐹 ) = ( 𝑅 ∨ 𝑈 ) )