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

Metamath Proof Explorer

Theorem trlcolem

Description: Lemma for trlco . (Contributed by NM, 1-Jun-2013)

Ref Expression
Hypotheses trlco.l ⊢ ≤ = ( le ‘ 𝐾 )
trlco.j ⊢ ∨ = ( join ‘ 𝐾 )
trlco.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
trlco.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
trlco.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
trlcolem.m ⊢ ∧ = ( meet ‘ 𝐾 )
trlcolem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion trlcolem ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 trlco.l ⊢ ≤ = ( le ‘ 𝐾 )
2 trlco.j ⊢ ∨ = ( join ‘ 𝐾 )
3 trlco.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 trlco.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 trlco.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
6 trlcolem.m ⊢ ∧ = ( meet ‘ 𝐾 )
7 trlcolem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
8 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
9 8 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
10 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐴 )
11 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12 11 7 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
13 10 12 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
14 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
15 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐺 ∈ 𝑇 )
16 1 7 3 4 ltrnat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 )
17 14 15 10 16 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 )
18 11 7 atbase ⊢ ( ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 → ( 𝐺 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
19 17 18 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐺 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
20 11 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐺 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ) → 𝑃 ≤ ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) )
21 9 13 19 20 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ≤ ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) )
22 11 2 7 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ) → ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) )
23 8 10 17 22 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) )
24 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐹 ∈ 𝑇 )
25 11 3 4 ltrncl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝐺 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) )
26 14 24 19 25 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) )
27 11 1 2 latjlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑃 ≤ ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) → ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ≤ ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ) )
28 9 13 23 26 27 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ≤ ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) → ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ≤ ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ) )
29 21 28 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ≤ ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) )
30 11 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) )
31 9 13 26 30 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) )
32 11 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) )
33 9 23 26 32 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) )
34 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐻 )
35 11 3 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
36 34 35 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
37 11 1 6 latmlem1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ≤ ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) ≤ ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) ) )
38 9 31 33 36 37 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ≤ ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) ≤ ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) ) )
39 29 38 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) ≤ ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) )
40 3 4 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 )
41 14 24 15 40 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 )
42 1 2 6 7 3 4 5 trlval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑃 ∨ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑃 ) ) ∧ 𝑊 ) )
43 41 42 syld3an2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑃 ∨ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑃 ) ) ∧ 𝑊 ) )
44 1 7 3 4 ltrncoval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑃 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) )
45 44 3adant3r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑃 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) )
46 45 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑃 ) ) = ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) )
47 46 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑃 ) ) ∧ 𝑊 ) = ( ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) )
48 43 47 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) )
49 1 7 3 4 ltrnel ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐺 ‘ 𝑃 ) ≤ 𝑊 ) )
50 15 49 syld3an2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐺 ‘ 𝑃 ) ≤ 𝑊 ) )
51 1 2 6 7 3 4 5 trlval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐺 ‘ 𝑃 ) ≤ 𝑊 ) ) → ( 𝑅 ‘ 𝐹 ) = ( ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) )
52 14 24 50 51 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ 𝐹 ) = ( ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) )
53 1 2 6 7 3 4 5 trlval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ 𝐺 ) = ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) )
54 15 53 syld3an2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ 𝐺 ) = ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) )
55 52 54 oveq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) = ( ( ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) ∨ ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ) )
56 1 7 3 4 ltrnat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ 𝐴 )
57 14 24 17 56 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ 𝐴 )
58 11 2 7 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) )
59 8 17 57 58 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) )
60 11 6 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
61 9 59 36 60 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
62 11 6 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
63 9 23 36 62 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
64 11 2 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) ∨ ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ) = ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ ( ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) ) )
65 9 61 63 64 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) ∨ ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ) = ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ ( ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) ) )
66 11 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐺 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) )
67 9 19 26 66 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) )
68 11 1 6 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ≤ 𝑊 )
69 9 23 36 68 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ≤ 𝑊 )
70 11 1 2 6 3 lhpmod6i1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ≤ 𝑊 ) → ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ ( ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) ) = ( ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ) ∧ 𝑊 ) )
71 14 63 67 69 70 syl121anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ ( ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) ) = ( ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ) ∧ 𝑊 ) )
72 11 2 latjass ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐺 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) = ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ) )
73 9 63 19 26 72 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) = ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ) )
74 11 1 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐺 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐺 ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) )
75 9 13 19 74 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐺 ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) )
76 11 1 2 6 3 lhpmod2i2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐺 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝐺 ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ) → ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ ( 𝐺 ‘ 𝑃 ) ) = ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ ( 𝑊 ∨ ( 𝐺 ‘ 𝑃 ) ) ) )
77 14 23 19 75 76 syl121anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ ( 𝐺 ‘ 𝑃 ) ) = ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ ( 𝑊 ∨ ( 𝐺 ‘ 𝑃 ) ) ) )
78 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
79 1 2 78 7 3 lhpjat1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐺 ‘ 𝑃 ) ≤ 𝑊 ) ) → ( 𝑊 ∨ ( 𝐺 ‘ 𝑃 ) ) = ( 1. ‘ 𝐾 ) )
80 14 50 79 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑊 ∨ ( 𝐺 ‘ 𝑃 ) ) = ( 1. ‘ 𝐾 ) )
81 80 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ ( 𝑊 ∨ ( 𝐺 ‘ 𝑃 ) ) ) = ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ ( 1. ‘ 𝐾 ) ) )
82 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
83 8 82 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐾 ∈ OL )
84 11 6 78 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) )
85 83 23 84 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) )
86 77 81 85 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ ( 𝐺 ‘ 𝑃 ) ) = ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) )
87 86 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) = ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) )
88 73 87 eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ) = ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) )
89 88 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ) ∧ 𝑊 ) = ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) )
90 71 89 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ ( ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) ) = ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) )
91 55 65 90 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) = ( ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) )
92 39 48 91 3brtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )