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

Metamath Proof Explorer

Theorem cdlemh1

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

Ref Expression
Hypotheses cdlemh.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdlemh.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemh.j ⊢ ∨ = ( join ‘ 𝐾 )
cdlemh.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdlemh.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemh.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemh.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemh.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
cdlemh.s ⊢ 𝑆 = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
Assertion cdlemh1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑆 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )

Proof

Step Hyp Ref Expression
1 cdlemh.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdlemh.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cdlemh.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cdlemh.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 cdlemh.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemh.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 cdlemh.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8 cdlemh.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
9 cdlemh.s ⊢ 𝑆 = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
10 9 oveq1i ⊢ ( 𝑆 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) )
11 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐾 ∈ HL )
12 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 simp13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐺 ∈ 𝑇 )
14 simp12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐹 ∈ 𝑇 )
15 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) )
16 15 necomd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) )
17 5 6 7 8 trlcocnvat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐴 )
18 12 13 14 16 17 syl121anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐴 )
19 11 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐾 ∈ Lat )
20 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑃 ∈ 𝐴 )
21 1 5 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
22 20 21 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑃 ∈ 𝐵 )
23 1 6 7 8 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐺 ) ∈ 𝐵 )
24 12 13 23 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) ∈ 𝐵 )
25 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ ( 𝑅 ‘ 𝐺 ) ∈ 𝐵 ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ 𝐵 )
26 19 22 24 25 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ 𝐵 )
27 simp2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑄 ∈ 𝐴 )
28 1 3 5 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐴 ) → ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∈ 𝐵 )
29 11 27 18 28 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∈ 𝐵 )
30 2 3 5 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐴 ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ≤ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
31 11 27 18 30 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ≤ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
32 1 2 3 4 5 atmod4i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐴 ∧ ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ 𝐵 ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∈ 𝐵 ) ∧ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ≤ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) → ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) )
33 11 18 26 29 31 32 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) )
34 6 7 ltrncnv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ◡ 𝐹 ∈ 𝑇 )
35 12 14 34 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ◡ 𝐹 ∈ 𝑇 )
36 3 6 7 8 trljco2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ◡ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐺 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( ( 𝑅 ‘ ◡ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
37 12 13 35 36 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑅 ‘ 𝐺 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( ( 𝑅 ‘ ◡ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
38 6 7 8 trlcnv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ◡ 𝐹 ) = ( 𝑅 ‘ 𝐹 ) )
39 12 14 38 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ ◡ 𝐹 ) = ( 𝑅 ‘ 𝐹 ) )
40 39 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑅 ‘ ◡ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
41 37 40 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑅 ‘ 𝐺 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
42 41 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑃 ∨ ( ( 𝑅 ‘ 𝐺 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) = ( 𝑃 ∨ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) )
43 6 7 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ◡ 𝐹 ∈ 𝑇 ) → ( 𝐺 ∘ ◡ 𝐹 ) ∈ 𝑇 )
44 12 13 35 43 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝐺 ∘ ◡ 𝐹 ) ∈ 𝑇 )
45 1 6 7 8 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∘ ◡ 𝐹 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐵 )
46 12 44 45 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐵 )
47 1 3 latjass ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝑅 ‘ 𝐺 ) ∈ 𝐵 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐵 ) ) → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( 𝑃 ∨ ( ( 𝑅 ‘ 𝐺 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) )
48 19 22 24 46 47 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( 𝑃 ∨ ( ( 𝑅 ‘ 𝐺 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) )
49 1 6 7 8 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐵 )
50 12 14 49 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐵 )
51 1 3 latjass ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝑅 ‘ 𝐹 ) ∈ 𝐵 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐵 ) ) → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( 𝑃 ∨ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) )
52 19 22 50 46 51 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( 𝑃 ∨ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) )
53 42 48 52 3eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
54 53 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) = ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) )
55 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) )
56 1 5 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
57 27 56 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑄 ∈ 𝐵 )
58 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ ( 𝑅 ‘ 𝐹 ) ∈ 𝐵 ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∈ 𝐵 )
59 19 22 50 58 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∈ 𝐵 )
60 1 2 3 latjlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ 𝐵 ∧ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∈ 𝐵 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐵 ) ) → ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) → ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ≤ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) )
61 19 57 59 46 60 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) → ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ≤ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) )
62 55 61 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ≤ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
63 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∈ 𝐵 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐵 ) → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∈ 𝐵 )
64 19 59 46 63 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∈ 𝐵 )
65 1 2 4 latleeqm2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∈ 𝐵 ∧ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∈ 𝐵 ) → ( ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ≤ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ↔ ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) = ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) )
66 19 29 64 65 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ≤ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ↔ ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) = ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) )
67 62 66 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) = ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
68 33 54 67 3eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
69 10 68 eqtrid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑆 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )