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

Metamath Proof Explorer

Theorem trlcoabs2N

Description: Absorption of the trace of a composition. (Contributed by NM, 29-Jul-2013) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 trlcoabs.l ⊢ ≤ = ( le ‘ 𝐾 )
2 trlcoabs.j ⊢ ∨ = ( join ‘ 𝐾 )
3 trlcoabs.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 trlcoabs.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5 trlcoabs.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6 trlcoabs.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
7 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐺 ∈ 𝑇 )
9 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐹 ∈ 𝑇 )
10 4 5 ltrncnv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ◡ 𝐹 ∈ 𝑇 )
11 7 9 10 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ◡ 𝐹 ∈ 𝑇 )
12 4 5 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ◡ 𝐹 ∈ 𝑇 ) → ( 𝐺 ∘ ◡ 𝐹 ) ∈ 𝑇 )
13 7 8 11 12 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐺 ∘ ◡ 𝐹 ) ∈ 𝑇 )
14 1 3 4 5 ltrnel ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) )
15 14 3adant2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) )
16 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
17 1 2 16 3 4 5 6 trlval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∘ ◡ 𝐹 ) ∈ 𝑇 ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) = ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ( meet ‘ 𝐾 ) 𝑊 ) )
18 7 13 15 17 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) = ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ( meet ‘ 𝐾 ) 𝑊 ) )
19 18 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) )
20 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
21 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐴 )
22 1 3 4 5 ltrnat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 )
23 7 9 21 22 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 )
24 1 3 4 5 ltrnat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∘ ◡ 𝐹 ) ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ) → ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ∈ 𝐴 )
25 7 13 23 24 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ∈ 𝐴 )
26 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
27 26 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) )
28 20 23 25 27 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) )
29 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐻 )
30 26 4 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
31 29 30 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
32 1 2 3 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ∈ 𝐴 ) → ( 𝐹 ‘ 𝑃 ) ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) )
33 20 23 25 32 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑃 ) ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) )
34 26 1 2 16 3 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝐹 ‘ 𝑃 ) ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ( meet ‘ 𝐾 ) ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑊 ) ) )
35 20 23 28 31 33 34 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ( meet ‘ 𝐾 ) ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑊 ) ) )
36 1 3 4 5 ltrncoval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐺 ∘ ◡ 𝐹 ) ∈ 𝑇 ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → ( ( ( 𝐺 ∘ ◡ 𝐹 ) ∘ 𝐹 ) ‘ 𝑃 ) = ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) )
37 7 13 9 21 36 syl121anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( 𝐺 ∘ ◡ 𝐹 ) ∘ 𝐹 ) ‘ 𝑃 ) = ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) )
38 coass ⊢ ( ( 𝐺 ∘ ◡ 𝐹 ) ∘ 𝐹 ) = ( 𝐺 ∘ ( ◡ 𝐹 ∘ 𝐹 ) )
39 26 4 5 ltrn1o ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
40 7 9 39 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
41 f1ococnv1 ⊢ ( 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝐾 ) ) )
42 40 41 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝐾 ) ) )
43 42 coeq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐺 ∘ ( ◡ 𝐹 ∘ 𝐹 ) ) = ( 𝐺 ∘ ( I ↾ ( Base ‘ 𝐾 ) ) ) )
44 26 4 5 ltrn1o ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
45 7 8 44 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
46 f1of ⊢ ( 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → 𝐺 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) )
47 fcoi1 ⊢ ( 𝐺 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) → ( 𝐺 ∘ ( I ↾ ( Base ‘ 𝐾 ) ) ) = 𝐺 )
48 45 46 47 3syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐺 ∘ ( I ↾ ( Base ‘ 𝐾 ) ) ) = 𝐺 )
49 43 48 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐺 ∘ ( ◡ 𝐹 ∘ 𝐹 ) ) = 𝐺 )
50 38 49 eqtrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐺 ∘ ◡ 𝐹 ) ∘ 𝐹 ) = 𝐺 )
51 50 fveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( 𝐺 ∘ ◡ 𝐹 ) ∘ 𝐹 ) ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) )
52 37 51 eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) = ( 𝐺 ‘ 𝑃 ) )
53 52 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) = ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐺 ‘ 𝑃 ) ) )
54 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
55 1 2 54 3 4 lhpjat2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
56 7 15 55 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
57 53 56 oveq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ( meet ‘ 𝐾 ) ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑊 ) ) = ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐺 ‘ 𝑃 ) ) ( meet ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) )
58 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
59 20 58 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐾 ∈ OL )
60 1 3 4 5 ltrnat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 )
61 7 8 21 60 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 )
62 26 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) )
63 20 23 61 62 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) )
64 26 16 54 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐺 ‘ 𝑃 ) ) ( meet ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) = ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐺 ‘ 𝑃 ) ) )
65 59 63 64 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐺 ‘ 𝑃 ) ) ( meet ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) = ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐺 ‘ 𝑃 ) ) )
66 57 65 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝐺 ∘ ◡ 𝐹 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ( meet ‘ 𝐾 ) ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑊 ) ) = ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐺 ‘ 𝑃 ) ) )
67 19 35 66 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐺 ‘ 𝑃 ) ) )