Metamath Proof Explorer


Theorem cdlemk12u

Description: Part of proof of Lemma K of Crawley p. 118. Line 18, p. 119, showing Eq. 4 (line 10, p. 119) for the sigma_1 ( U ) case. (Contributed by NM, 4-Jul-2013)

Ref Expression
Hypotheses cdlemk1.b 𝐵 = ( Base ‘ 𝐾 )
cdlemk1.l = ( le ‘ 𝐾 )
cdlemk1.j = ( join ‘ 𝐾 )
cdlemk1.m = ( meet ‘ 𝐾 )
cdlemk1.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemk1.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemk1.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemk1.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
cdlemk1.s 𝑆 = ( 𝑓𝑇 ↦ ( 𝑖𝑇 ( 𝑖𝑃 ) = ( ( 𝑃 ( 𝑅𝑓 ) ) ( ( 𝑁𝑃 ) ( 𝑅 ‘ ( 𝑓 𝐹 ) ) ) ) ) )
cdlemk1.o 𝑂 = ( 𝑆𝐷 )
cdlemk1.u 𝑈 = ( 𝑒𝑇 ↦ ( 𝑗𝑇 ( 𝑗𝑃 ) = ( ( 𝑃 ( 𝑅𝑒 ) ) ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝑒 𝐷 ) ) ) ) ) )
Assertion cdlemk12u ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) = ( ( 𝑃 ( 𝐺𝑃 ) ) ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cdlemk1.b 𝐵 = ( Base ‘ 𝐾 )
2 cdlemk1.l = ( le ‘ 𝐾 )
3 cdlemk1.j = ( join ‘ 𝐾 )
4 cdlemk1.m = ( meet ‘ 𝐾 )
5 cdlemk1.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemk1.h 𝐻 = ( LHyp ‘ 𝐾 )
7 cdlemk1.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8 cdlemk1.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
9 cdlemk1.s 𝑆 = ( 𝑓𝑇 ↦ ( 𝑖𝑇 ( 𝑖𝑃 ) = ( ( 𝑃 ( 𝑅𝑓 ) ) ( ( 𝑁𝑃 ) ( 𝑅 ‘ ( 𝑓 𝐹 ) ) ) ) ) )
10 cdlemk1.o 𝑂 = ( 𝑆𝐷 )
11 cdlemk1.u 𝑈 = ( 𝑒𝑇 ↦ ( 𝑗𝑇 ( 𝑗𝑃 ) = ( ( 𝑃 ( 𝑅𝑒 ) ) ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝑒 𝐷 ) ) ) ) ) )
12 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝐾 ∈ HL )
13 simp22l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝑃𝐴 )
14 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
15 simp212 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝐺𝑇 )
16 2 5 6 7 ltrnat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇𝑃𝐴 ) → ( 𝐺𝑃 ) ∈ 𝐴 )
17 14 15 13 16 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝐺𝑃 ) ∈ 𝐴 )
18 simp23 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝐹 ) = ( 𝑅𝑁 ) )
19 simp213 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝑋𝑇 )
20 simp12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝐹𝑇 )
21 simp13 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝐷𝑇 )
22 simp211 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝑁𝑇 )
23 simp331 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) )
24 simp333 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) )
25 24 necomd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝐷 ) ≠ ( 𝑅𝑋 ) )
26 23 25 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝑋 ) ) )
27 simp311 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
28 simp32l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝑋 ≠ ( I ↾ 𝐵 ) )
29 simp312 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝐷 ≠ ( I ↾ 𝐵 ) )
30 27 28 29 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) )
31 simp22 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
32 1 2 3 4 5 6 7 8 9 10 11 cdlemkuat ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝑋𝑇 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝑋 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ) → ( ( 𝑈𝑋 ) ‘ 𝑃 ) ∈ 𝐴 )
33 14 18 19 20 21 22 26 30 31 32 syl333anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑈𝑋 ) ‘ 𝑃 ) ∈ 𝐴 )
34 simp32r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) )
35 34 necomd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝑋 ) ≠ ( 𝑅𝐺 ) )
36 5 6 7 8 trlcocnvat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝑇𝐺𝑇 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐺 ) ) → ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ∈ 𝐴 )
37 14 19 15 35 36 syl121anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ∈ 𝐴 )
38 simp332 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) )
39 38 necomd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝐷 ) ≠ ( 𝑅𝐺 ) )
40 23 39 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐺 ) ) )
41 simp313 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝐺 ≠ ( I ↾ 𝐵 ) )
42 27 41 29 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) )
43 1 2 3 4 5 6 7 8 9 10 11 cdlemkuat ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐺𝑇 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) ∈ 𝐴 )
44 14 18 15 20 21 22 40 42 31 43 syl333anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) ∈ 𝐴 )
45 1 2 3 4 5 6 7 8 9 10 11 cdlemkuv2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐺𝑇 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) = ( ( 𝑃 ( 𝑅𝐺 ) ) ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ) ) )
46 14 18 15 20 21 22 40 42 31 45 syl333anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) = ( ( 𝑃 ( 𝑅𝐺 ) ) ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ) ) )
47 12 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝐾 ∈ Lat )
48 1 5 6 7 8 trlnidat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) → ( 𝑅𝐺 ) ∈ 𝐴 )
49 14 15 41 48 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝐺 ) ∈ 𝐴 )
50 1 3 5 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ∧ ( 𝑅𝐺 ) ∈ 𝐴 ) → ( 𝑃 ( 𝑅𝐺 ) ) ∈ 𝐵 )
51 12 13 49 50 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑃 ( 𝑅𝐺 ) ) ∈ 𝐵 )
52 simp1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) )
53 22 31 18 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) )
54 1 2 3 4 5 6 7 8 9 10 cdlemkoatnle ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ) → ( ( 𝑂𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝑂𝑃 ) 𝑊 ) )
55 54 simpld ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ) → ( 𝑂𝑃 ) ∈ 𝐴 )
56 52 53 27 29 23 55 syl113anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑂𝑃 ) ∈ 𝐴 )
57 5 6 7 8 trlcocnvat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐺𝑇𝐷𝑇 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) → ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ∈ 𝐴 )
58 14 15 21 38 57 syl121anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ∈ 𝐴 )
59 1 3 5 hlatjcl ( ( 𝐾 ∈ HL ∧ ( 𝑂𝑃 ) ∈ 𝐴 ∧ ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ∈ 𝐴 ) → ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ) ∈ 𝐵 )
60 12 56 58 59 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ) ∈ 𝐵 )
61 1 2 4 latmle1 ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ( 𝑅𝐺 ) ) ∈ 𝐵 ∧ ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ) ∈ 𝐵 ) → ( ( 𝑃 ( 𝑅𝐺 ) ) ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ) ) ( 𝑃 ( 𝑅𝐺 ) ) )
62 47 51 60 61 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑃 ( 𝑅𝐺 ) ) ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ) ) ( 𝑃 ( 𝑅𝐺 ) ) )
63 46 62 eqbrtrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) ( 𝑃 ( 𝑅𝐺 ) ) )
64 2 3 5 6 7 8 trljat1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 ( 𝑅𝐺 ) ) = ( 𝑃 ( 𝐺𝑃 ) ) )
65 14 15 31 64 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑃 ( 𝑅𝐺 ) ) = ( 𝑃 ( 𝐺𝑃 ) ) )
66 63 65 breqtrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) ( 𝑃 ( 𝐺𝑃 ) ) )
67 simp2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) )
68 simp31 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) )
69 simp33 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) )
70 eqid ( ( ( 𝐺𝑃 ) ( 𝑋𝑃 ) ) ( ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ) ) = ( ( ( 𝐺𝑃 ) ( 𝑋𝑃 ) ) ( ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ) )
71 1 2 3 4 5 6 7 8 9 10 11 70 cdlemk11u ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ) )
72 52 67 68 28 69 71 syl113anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ) )
73 2 3 5 hlatlej2 ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ∧ ( 𝑅𝐺 ) ∈ 𝐴 ) → ( 𝑅𝐺 ) ( 𝑃 ( 𝑅𝐺 ) ) )
74 12 13 49 73 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝐺 ) ( 𝑃 ( 𝑅𝐺 ) ) )
75 74 65 breqtrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝐺 ) ( 𝑃 ( 𝐺𝑃 ) ) )
76 1 2 3 4 5 6 7 8 9 10 11 cdlemkuel ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝑋𝑇 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝑋 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ) → ( 𝑈𝑋 ) ∈ 𝑇 )
77 14 18 19 20 21 22 26 30 31 76 syl333anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑈𝑋 ) ∈ 𝑇 )
78 2 5 6 7 ltrnel ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝑋 ) ∈ 𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( ( 𝑈𝑋 ) ‘ 𝑃 ) 𝑊 ) )
79 14 77 31 78 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( ( 𝑈𝑋 ) ‘ 𝑃 ) 𝑊 ) )
80 6 7 ltrncnv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 ) → 𝐺𝑇 )
81 14 15 80 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝐺𝑇 )
82 6 7 8 trlcnv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 ) → ( 𝑅 𝐺 ) = ( 𝑅𝐺 ) )
83 14 15 82 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅 𝐺 ) = ( 𝑅𝐺 ) )
84 83 34 eqnetrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅 𝐺 ) ≠ ( 𝑅𝑋 ) )
85 1 6 7 8 trlcone ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐺𝑇𝑋𝑇 ) ∧ ( ( 𝑅 𝐺 ) ≠ ( 𝑅𝑋 ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑅 𝐺 ) ≠ ( 𝑅 ‘ ( 𝐺𝑋 ) ) )
86 14 81 19 84 28 85 syl122anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅 𝐺 ) ≠ ( 𝑅 ‘ ( 𝐺𝑋 ) ) )
87 86 necomd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅 ‘ ( 𝐺𝑋 ) ) ≠ ( 𝑅 𝐺 ) )
88 6 7 ltrncom ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇𝑋𝑇 ) → ( 𝐺𝑋 ) = ( 𝑋 𝐺 ) )
89 14 81 19 88 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝐺𝑋 ) = ( 𝑋 𝐺 ) )
90 89 fveq2d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅 ‘ ( 𝐺𝑋 ) ) = ( 𝑅 ‘ ( 𝑋 𝐺 ) ) )
91 87 90 83 3netr3d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ≠ ( 𝑅𝐺 ) )
92 6 7 ltrnco ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑇 𝐺𝑇 ) → ( 𝑋 𝐺 ) ∈ 𝑇 )
93 14 19 81 92 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑋 𝐺 ) ∈ 𝑇 )
94 2 6 7 8 trlle ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋 𝐺 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑋 𝐺 ) ) 𝑊 )
95 14 93 94 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅 ‘ ( 𝑋 𝐺 ) ) 𝑊 )
96 2 6 7 8 trlle ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 ) → ( 𝑅𝐺 ) 𝑊 )
97 14 15 96 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝐺 ) 𝑊 )
98 2 3 5 6 lhp2atnle ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( ( 𝑈𝑋 ) ‘ 𝑃 ) 𝑊 ) ∧ ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ≠ ( 𝑅𝐺 ) ) ∧ ( ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ∈ 𝐴 ∧ ( 𝑅 ‘ ( 𝑋 𝐺 ) ) 𝑊 ) ∧ ( ( 𝑅𝐺 ) ∈ 𝐴 ∧ ( 𝑅𝐺 ) 𝑊 ) ) → ¬ ( 𝑅𝐺 ) ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ) )
99 14 79 91 37 95 49 97 98 syl322anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ¬ ( 𝑅𝐺 ) ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ) )
100 nbrne1 ( ( ( 𝑅𝐺 ) ( 𝑃 ( 𝐺𝑃 ) ) ∧ ¬ ( 𝑅𝐺 ) ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ) ) → ( 𝑃 ( 𝐺𝑃 ) ) ≠ ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ) )
101 75 99 100 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑃 ( 𝐺𝑃 ) ) ≠ ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ) )
102 2 3 4 5 2atm ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ∧ ( 𝐺𝑃 ) ∈ 𝐴 ) ∧ ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) ∈ 𝐴 ∧ ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ∈ 𝐴 ∧ ( ( 𝑈𝐺 ) ‘ 𝑃 ) ∈ 𝐴 ) ∧ ( ( ( 𝑈𝐺 ) ‘ 𝑃 ) ( 𝑃 ( 𝐺𝑃 ) ) ∧ ( ( 𝑈𝐺 ) ‘ 𝑃 ) ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ) ∧ ( 𝑃 ( 𝐺𝑃 ) ) ≠ ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ) ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) = ( ( 𝑃 ( 𝐺𝑃 ) ) ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ) ) )
103 12 13 17 33 37 44 66 72 101 102 syl333anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑋 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) = ( ( 𝑃 ( 𝐺𝑃 ) ) ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐺 ) ) ) ) )