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

Metamath Proof Explorer

Theorem cdlemh

Description: 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 cdlemh ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) )

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 simp1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) )
11 simp21l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑃 ∈ 𝐴 )
12 simp22l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑄 ∈ 𝐴 )
13 simp23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) )
14 simp33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) )
15 1 2 3 4 5 6 7 8 9 cdlemh1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑆 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
16 10 11 12 13 14 15 syl122anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑆 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
17 oveq1 ⊢ ( 𝑆 = ( 0. ‘ 𝐾 ) → ( 𝑆 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( ( 0. ‘ 𝐾 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
18 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐾 ∈ HL )
19 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
20 18 19 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐾 ∈ OL )
21 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑊 ∈ 𝐻 )
22 18 21 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
23 simp13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐺 ∈ 𝑇 )
24 simp12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐹 ∈ 𝑇 )
25 6 7 ltrncnv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ◡ 𝐹 ∈ 𝑇 )
26 22 24 25 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ◡ 𝐹 ∈ 𝑇 )
27 23 26 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝐺 ∈ 𝑇 ∧ ◡ 𝐹 ∈ 𝑇 ) )
28 14 necomd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) )
29 6 7 8 trlcnv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ◡ 𝐹 ) = ( 𝑅 ‘ 𝐹 ) )
30 22 24 29 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ ◡ 𝐹 ) = ( 𝑅 ‘ 𝐹 ) )
31 28 30 neeqtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ ◡ 𝐹 ) )
32 5 6 7 8 trlcoat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ◡ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ ◡ 𝐹 ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐴 )
33 22 27 31 32 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐴 )
34 1 5 atbase ⊢ ( ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐴 → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐵 )
35 33 34 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐵 )
36 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
37 1 3 36 olj02 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐵 ) → ( ( 0. ‘ 𝐾 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) )
38 20 35 37 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 0. ‘ 𝐾 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) )
39 17 38 sylan9eqr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) → ( 𝑆 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) )
40 6 7 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ◡ 𝐹 ∈ 𝑇 ) → ( 𝐺 ∘ ◡ 𝐹 ) ∈ 𝑇 )
41 22 23 26 40 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝐺 ∘ ◡ 𝐹 ) ∈ 𝑇 )
42 2 6 7 8 trlle ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∘ ◡ 𝐹 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ≤ 𝑊 )
43 22 41 42 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ≤ 𝑊 )
44 simp22r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ¬ 𝑄 ≤ 𝑊 )
45 nbrne2 ⊢ ( ( ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ≤ 𝑊 ∧ ¬ 𝑄 ≤ 𝑊 ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ≠ 𝑄 )
46 45 necomd ⊢ ( ( ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ≤ 𝑊 ∧ ¬ 𝑄 ≤ 𝑊 ) → 𝑄 ≠ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) )
47 43 44 46 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑄 ≠ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) )
48 eqid ⊢ ( LLines ‘ 𝐾 ) = ( LLines ‘ 𝐾 )
49 3 5 48 llni2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐴 ) ∧ 𝑄 ≠ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) → ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∈ ( LLines ‘ 𝐾 ) )
50 18 12 33 47 49 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∈ ( LLines ‘ 𝐾 ) )
51 5 48 llnneat ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∈ ( LLines ‘ 𝐾 ) ) → ¬ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∈ 𝐴 )
52 18 50 51 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ¬ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∈ 𝐴 )
53 nelne2 ⊢ ( ( ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐴 ∧ ¬ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∈ 𝐴 ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ≠ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
54 33 52 53 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ≠ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
55 54 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ≠ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
56 39 55 eqnetrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) → ( 𝑆 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ≠ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
57 56 ex ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑆 = ( 0. ‘ 𝐾 ) → ( 𝑆 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ≠ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) )
58 57 necon2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑆 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) = ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) → 𝑆 ≠ ( 0. ‘ 𝐾 ) ) )
59 16 58 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑆 ≠ ( 0. ‘ 𝐾 ) )
60 simp32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐺 ≠ ( I ↾ 𝐵 ) )
61 1 5 6 7 8 trlnidat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) → ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 )
62 22 23 60 61 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 )
63 2 3 5 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 ) → ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) )
64 18 11 62 63 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) )
65 simp22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
66 simp31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
67 1 6 7 ltrncnvnid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ◡ 𝐹 ≠ ( I ↾ 𝐵 ) )
68 22 24 66 67 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ◡ 𝐹 ≠ ( I ↾ 𝐵 ) )
69 1 6 7 8 trlcone ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ◡ 𝐹 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ ◡ 𝐹 ) ∧ ◡ 𝐹 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) )
70 69 necomd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ◡ 𝐹 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ ◡ 𝐹 ) ∧ ◡ 𝐹 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ≠ ( 𝑅 ‘ 𝐺 ) )
71 22 23 26 31 68 70 syl122anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ≠ ( 𝑅 ‘ 𝐺 ) )
72 2 6 7 8 trlle ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐺 ) ≤ 𝑊 )
73 22 23 72 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) ≤ 𝑊 )
74 2 3 5 6 lhp2atnle ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐴 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ≤ 𝑊 ) ∧ ( ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 ∧ ( 𝑅 ‘ 𝐺 ) ≤ 𝑊 ) ) → ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
75 22 65 71 33 43 62 73 74 syl322anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
76 nbrne1 ⊢ ( ( ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ≠ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
77 64 75 76 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ≠ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
78 3 4 36 5 2atmat0 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐴 ∧ ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ≠ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ) → ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) = ( 0. ‘ 𝐾 ) ) )
79 18 11 62 12 33 77 78 syl33anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) = ( 0. ‘ 𝐾 ) ) )
80 9 eleq1i ⊢ ( 𝑆 ∈ 𝐴 ↔ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ∈ 𝐴 )
81 9 eqeq1i ⊢ ( 𝑆 = ( 0. ‘ 𝐾 ) ↔ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) = ( 0. ‘ 𝐾 ) )
82 80 81 orbi12i ⊢ ( ( 𝑆 ∈ 𝐴 ∨ 𝑆 = ( 0. ‘ 𝐾 ) ) ↔ ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) = ( 0. ‘ 𝐾 ) ) )
83 79 82 sylibr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑆 ∈ 𝐴 ∨ 𝑆 = ( 0. ‘ 𝐾 ) ) )
84 83 ord ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ¬ 𝑆 ∈ 𝐴 → 𝑆 = ( 0. ‘ 𝐾 ) ) )
85 84 necon1ad ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑆 ≠ ( 0. ‘ 𝐾 ) → 𝑆 ∈ 𝐴 ) )
86 59 85 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑆 ∈ 𝐴 )
87 simp21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
88 87 65 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) )
89 1 2 3 4 5 6 7 8 9 36 cdlemh2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑆 ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) )
90 88 89 syld3an2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑆 ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) )
91 2 4 36 5 6 lhpmatb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐴 ) → ( ¬ 𝑆 ≤ 𝑊 ↔ ( 𝑆 ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) ) )
92 18 21 86 91 syl21anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ¬ 𝑆 ≤ 𝑊 ↔ ( 𝑆 ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) ) )
93 90 92 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ¬ 𝑆 ≤ 𝑊 )
94 86 93 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) )