Metamath Proof Explorer


Theorem cdlemk7u

Description: Part of proof of Lemma K of Crawley p. 118. Line 5, p. 119 for the sigma_1 case. (Contributed by NM, 3-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 𝑈 = ( 𝑒𝑇 ↦ ( 𝑗𝑇 ( 𝑗𝑃 ) = ( ( 𝑃 ( 𝑅𝑒 ) ) ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝑒 𝐷 ) ) ) ) ) )
cdlemk1.v 𝑉 = ( ( ( 𝐺𝑃 ) ( 𝑋𝑃 ) ) ( ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ) )
Assertion cdlemk7u ( ( ( ( 𝐾 ∈ 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 cdlemk1.v 𝑉 = ( ( ( 𝐺𝑃 ) ( 𝑋𝑃 ) ) ( ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ) )
13 simp31 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) )
14 simp33 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) )
15 13 14 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) )
16 1 2 3 4 5 6 7 8 9 10 cdlemk6u ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑃 ( 𝐺𝑃 ) ) ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ) ) ( ( ( ( 𝐺𝑃 ) ( 𝑋𝑃 ) ) ( ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ) ) ( ( ( 𝑋𝑃 ) 𝑃 ) ( ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ( 𝑂𝑃 ) ) ) ) )
17 15 16 syld3an3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑃 ( 𝐺𝑃 ) ) ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ) ) ( ( ( ( 𝐺𝑃 ) ( 𝑋𝑃 ) ) ( ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ) ) ( ( ( 𝑋𝑃 ) 𝑃 ) ( ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ( 𝑂𝑃 ) ) ) ) )
18 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝐾 ∈ HL )
19 simp11r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝑊𝐻 )
20 18 19 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
21 simp23 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝐹 ) = ( 𝑅𝑁 ) )
22 simp212 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝐺𝑇 )
23 simp12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝐹𝑇 )
24 simp13 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝐷𝑇 )
25 simp211 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝑁𝑇 )
26 23 24 25 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) )
27 simp331 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) )
28 simp332 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) )
29 28 necomd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝐷 ) ≠ ( 𝑅𝐺 ) )
30 27 29 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐺 ) ) )
31 simp311 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
32 simp313 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝐺 ≠ ( I ↾ 𝐵 ) )
33 simp312 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝐷 ≠ ( I ↾ 𝐵 ) )
34 31 32 33 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) )
35 simp22 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
36 1 2 3 4 5 6 7 8 9 10 11 cdlemkuv2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐺𝑇 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) = ( ( 𝑃 ( 𝑅𝐺 ) ) ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ) ) )
37 20 21 22 26 30 34 35 36 syl313anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) = ( ( 𝑃 ( 𝑅𝐺 ) ) ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ) ) )
38 2 3 5 6 7 8 trljat1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 ( 𝑅𝐺 ) ) = ( 𝑃 ( 𝐺𝑃 ) ) )
39 20 22 35 38 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑃 ( 𝑅𝐺 ) ) = ( 𝑃 ( 𝐺𝑃 ) ) )
40 39 oveq1d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑃 ( 𝑅𝐺 ) ) ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ) ) = ( ( 𝑃 ( 𝐺𝑃 ) ) ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ) ) )
41 37 40 eqtrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) = ( ( 𝑃 ( 𝐺𝑃 ) ) ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ) ) )
42 18 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝐾 ∈ Lat )
43 simp213 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝑋𝑇 )
44 simp333 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) )
45 44 necomd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅𝐷 ) ≠ ( 𝑅𝑋 ) )
46 27 45 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝑋 ) ) )
47 simp32 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝑋 ≠ ( I ↾ 𝐵 ) )
48 31 47 33 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) )
49 1 2 3 4 5 6 7 8 9 10 11 cdlemkuat ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝑋𝑇 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝑋 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ) → ( ( 𝑈𝑋 ) ‘ 𝑃 ) ∈ 𝐴 )
50 20 21 43 26 46 48 35 49 syl313anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑈𝑋 ) ‘ 𝑃 ) ∈ 𝐴 )
51 1 5 atbase ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) ∈ 𝐴 → ( ( 𝑈𝑋 ) ‘ 𝑃 ) ∈ 𝐵 )
52 50 51 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑈𝑋 ) ‘ 𝑃 ) ∈ 𝐵 )
53 simp22l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝑃𝐴 )
54 1 2 3 5 6 7 8 4 12 cdlemkvcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐷𝑇𝐺𝑇𝑋𝑇 ) ∧ 𝑃𝐴 ) → 𝑉𝐵 )
55 18 19 24 22 43 53 54 syl231anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝑉𝐵 )
56 1 3 latjcom ( ( 𝐾 ∈ Lat ∧ ( ( 𝑈𝑋 ) ‘ 𝑃 ) ∈ 𝐵𝑉𝐵 ) → ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) 𝑉 ) = ( 𝑉 ( ( 𝑈𝑋 ) ‘ 𝑃 ) ) )
57 42 52 55 56 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) 𝑉 ) = ( 𝑉 ( ( 𝑈𝑋 ) ‘ 𝑃 ) ) )
58 12 a1i ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → 𝑉 = ( ( ( 𝐺𝑃 ) ( 𝑋𝑃 ) ) ( ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ) ) )
59 1 2 3 4 5 6 7 8 9 10 11 cdlemkuv2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝑋𝑇 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝑋 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ) → ( ( 𝑈𝑋 ) ‘ 𝑃 ) = ( ( 𝑃 ( 𝑅𝑋 ) ) ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ) ) )
60 20 21 43 26 46 48 35 59 syl313anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑈𝑋 ) ‘ 𝑃 ) = ( ( 𝑃 ( 𝑅𝑋 ) ) ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ) ) )
61 2 3 5 6 7 8 trljat1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 ( 𝑅𝑋 ) ) = ( 𝑃 ( 𝑋𝑃 ) ) )
62 20 43 35 61 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑃 ( 𝑅𝑋 ) ) = ( 𝑃 ( 𝑋𝑃 ) ) )
63 2 5 6 7 ltrnat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑇𝑃𝐴 ) → ( 𝑋𝑃 ) ∈ 𝐴 )
64 20 43 53 63 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑋𝑃 ) ∈ 𝐴 )
65 3 5 hlatjcom ( ( 𝐾 ∈ HL ∧ ( 𝑋𝑃 ) ∈ 𝐴𝑃𝐴 ) → ( ( 𝑋𝑃 ) 𝑃 ) = ( 𝑃 ( 𝑋𝑃 ) ) )
66 18 64 53 65 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑋𝑃 ) 𝑃 ) = ( 𝑃 ( 𝑋𝑃 ) ) )
67 62 66 eqtr4d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑃 ( 𝑅𝑋 ) ) = ( ( 𝑋𝑃 ) 𝑃 ) )
68 simp1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) )
69 25 35 21 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) )
70 31 33 27 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) )
71 1 2 3 4 5 6 7 8 9 10 cdlemkoatnle ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ) → ( ( 𝑂𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝑂𝑃 ) 𝑊 ) )
72 71 simpld ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ) → ( 𝑂𝑃 ) ∈ 𝐴 )
73 68 69 70 72 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑂𝑃 ) ∈ 𝐴 )
74 43 24 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑋𝑇𝐷𝑇 ) )
75 5 6 7 8 trlcocnvat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝑇𝐷𝑇 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) → ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ∈ 𝐴 )
76 20 74 44 75 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ∈ 𝐴 )
77 3 5 hlatjcom ( ( 𝐾 ∈ HL ∧ ( 𝑂𝑃 ) ∈ 𝐴 ∧ ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ∈ 𝐴 ) → ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ) = ( ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ( 𝑂𝑃 ) ) )
78 18 73 76 77 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ) = ( ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ( 𝑂𝑃 ) ) )
79 67 78 oveq12d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑃 ( 𝑅𝑋 ) ) ( ( 𝑂𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ) ) = ( ( ( 𝑋𝑃 ) 𝑃 ) ( ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ( 𝑂𝑃 ) ) ) )
80 60 79 eqtrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑈𝑋 ) ‘ 𝑃 ) = ( ( ( 𝑋𝑃 ) 𝑃 ) ( ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ( 𝑂𝑃 ) ) ) )
81 58 80 oveq12d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( 𝑉 ( ( 𝑈𝑋 ) ‘ 𝑃 ) ) = ( ( ( ( 𝐺𝑃 ) ( 𝑋𝑃 ) ) ( ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ) ) ( ( ( 𝑋𝑃 ) 𝑃 ) ( ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ( 𝑂𝑃 ) ) ) ) )
82 57 81 eqtrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) 𝑉 ) = ( ( ( ( 𝐺𝑃 ) ( 𝑋𝑃 ) ) ( ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ) ) ( ( ( 𝑋𝑃 ) 𝑃 ) ( ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ( 𝑂𝑃 ) ) ) ) )
83 17 41 82 3brtr4d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐷𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝑋𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑋 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝑅𝑋 ) ≠ ( 𝑅𝐷 ) ) ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) ( ( ( 𝑈𝑋 ) ‘ 𝑃 ) 𝑉 ) )