Metamath Proof Explorer

Theorem cdlemi1

Description: Part of proof of Lemma I of Crawley p. 118. (Contributed by NM, 18-Jun-2013)

Ref Expression
Hypotheses cdlemi.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdlemi.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemi.j ⊢ ∨ = ( join ‘ 𝐾 )
cdlemi.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdlemi.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemi.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemi.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemi.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
cdlemi.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemi1 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 cdlemi.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdlemi.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cdlemi.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cdlemi.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 cdlemi.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemi.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 cdlemi.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8 cdlemi.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
9 cdlemi.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
10 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
11 10 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
12 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑈 ∈ 𝐸 )
14 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐺 ∈ 𝑇 )
15 6 7 9 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑈 ‘ 𝐺 ) ∈ 𝑇 )
16 12 13 14 15 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑈 ‘ 𝐺 ) ∈ 𝑇 )
17 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐴 )
18 1 5 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
19 17 18 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐵 )
20 1 6 7 ltrncl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ‘ 𝐺 ) ∈ 𝑇 ∧ 𝑃 ∈ 𝐵 ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ∈ 𝐵 )
21 12 16 19 20 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ∈ 𝐵 )
22 1 6 7 8 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ‘ 𝐺 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) ∈ 𝐵 )
23 12 16 22 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) ∈ 𝐵 )
24 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) ∈ 𝐵 ) → ( 𝑃 ∨ ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) ) ∈ 𝐵 )
25 11 19 23 24 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) ) ∈ 𝐵 )
26 1 6 7 8 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐺 ) ∈ 𝐵 )
27 12 14 26 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ 𝐺 ) ∈ 𝐵 )
28 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ ( 𝑅 ‘ 𝐺 ) ∈ 𝐵 ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ 𝐵 )
29 11 19 27 28 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ 𝐵 )
30 1 2 3 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ∈ 𝐵 ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) )
31 11 19 21 30 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) )
32 2 3 4 5 6 7 8 trlval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ‘ 𝐺 ) ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) = ( ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) ∧ 𝑊 ) )
33 16 32 syld3an2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) = ( ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) ∧ 𝑊 ) )
34 33 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) ) = ( 𝑃 ∨ ( ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) ∧ 𝑊 ) ) )
35 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ∈ 𝐵 ) → ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) ∈ 𝐵 )
36 11 19 21 35 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) ∈ 𝐵 )
37 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐻 )
38 1 6 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
39 37 38 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐵 )
40 1 2 3 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ∈ 𝐵 ) → 𝑃 ≤ ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) )
41 11 19 21 40 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ≤ ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) )
42 1 2 3 4 5 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝑃 ≤ ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
43 10 17 36 39 41 42 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
44 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
45 2 3 44 5 6 lhpjat2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
46 45 3adant2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
47 46 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) ∧ ( 𝑃 ∨ 𝑊 ) ) = ( ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) ∧ ( 1. ‘ 𝐾 ) ) )
48 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
49 10 48 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐾 ∈ OL )
50 1 4 44 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) ∈ 𝐵 ) → ( ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) )
51 49 36 50 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) )
52 47 51 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) ∧ ( 𝑃 ∨ 𝑊 ) ) = ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) )
53 34 43 52 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) ) = ( 𝑃 ∨ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ) )
54 31 53 breqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) ) )
55 2 6 7 8 9 tendotp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) ≤ ( 𝑅 ‘ 𝐺 ) )
56 12 13 14 55 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) ≤ ( 𝑅 ‘ 𝐺 ) )
57 1 2 3 latjlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) ∈ 𝐵 ∧ ( 𝑅 ‘ 𝐺 ) ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ) ) → ( ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) ≤ ( 𝑅 ‘ 𝐺 ) → ( 𝑃 ∨ ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ) )
58 11 23 27 19 57 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) ≤ ( 𝑅 ‘ 𝐺 ) → ( 𝑃 ∨ ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ) )
59 56 58 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( 𝑅 ‘ ( 𝑈 ‘ 𝐺 ) ) ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) )
60 1 2 11 21 25 29 54 59 lattrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) )