Metamath Proof Explorer


Theorem cdleme20j

Description: Part of proof of Lemma E in Crawley p. 113, last paragraph on p. 114. D , F , Y , G represent s_2, f(s), t_2, f(t). We show s_2 =/= t_2. (Contributed by NM, 18-Nov-2012)

Ref Expression
Hypotheses cdleme19.l = ( le ‘ 𝐾 )
cdleme19.j = ( join ‘ 𝐾 )
cdleme19.m = ( meet ‘ 𝐾 )
cdleme19.a 𝐴 = ( Atoms ‘ 𝐾 )
cdleme19.h 𝐻 = ( LHyp ‘ 𝐾 )
cdleme19.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
cdleme19.f 𝐹 = ( ( 𝑆 𝑈 ) ( 𝑄 ( ( 𝑃 𝑆 ) 𝑊 ) ) )
cdleme19.g 𝐺 = ( ( 𝑇 𝑈 ) ( 𝑄 ( ( 𝑃 𝑇 ) 𝑊 ) ) )
cdleme19.d 𝐷 = ( ( 𝑅 𝑆 ) 𝑊 )
cdleme19.y 𝑌 = ( ( 𝑅 𝑇 ) 𝑊 )
cdleme20.v 𝑉 = ( ( 𝑆 𝑇 ) 𝑊 )
Assertion cdleme20j ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝐷𝑌 )

Proof

Step Hyp Ref Expression
1 cdleme19.l = ( le ‘ 𝐾 )
2 cdleme19.j = ( join ‘ 𝐾 )
3 cdleme19.m = ( meet ‘ 𝐾 )
4 cdleme19.a 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme19.h 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme19.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
7 cdleme19.f 𝐹 = ( ( 𝑆 𝑈 ) ( 𝑄 ( ( 𝑃 𝑆 ) 𝑊 ) ) )
8 cdleme19.g 𝐺 = ( ( 𝑇 𝑈 ) ( 𝑄 ( ( 𝑃 𝑇 ) 𝑊 ) ) )
9 cdleme19.d 𝐷 = ( ( 𝑅 𝑆 ) 𝑊 )
10 cdleme19.y 𝑌 = ( ( 𝑅 𝑇 ) 𝑊 )
11 cdleme20.v 𝑉 = ( ( 𝑆 𝑇 ) 𝑊 )
12 simp33 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ¬ 𝑅 ( 𝑆 𝑇 ) )
13 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝐾 ∈ HL )
14 simp22l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝑆𝐴 )
15 simp21l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝑅𝐴 )
16 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17 16 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴 ) → ( 𝑅 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
18 13 15 14 17 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( 𝑅 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
19 simp11r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝑊𝐻 )
20 16 5 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
21 19 20 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
22 1 2 4 hlatlej2 ( ( 𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴 ) → 𝑆 ( 𝑅 𝑆 ) )
23 13 15 14 22 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝑆 ( 𝑅 𝑆 ) )
24 16 1 2 3 4 atmod2i1 ( ( 𝐾 ∈ HL ∧ ( 𝑆𝐴 ∧ ( 𝑅 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑆 ( 𝑅 𝑆 ) ) → ( ( ( 𝑅 𝑆 ) 𝑊 ) 𝑆 ) = ( ( 𝑅 𝑆 ) ( 𝑊 𝑆 ) ) )
25 13 14 18 21 23 24 syl131anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( ( ( 𝑅 𝑆 ) 𝑊 ) 𝑆 ) = ( ( 𝑅 𝑆 ) ( 𝑊 𝑆 ) ) )
26 simp22 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) )
27 eqid ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
28 1 2 27 4 5 lhpjat1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) → ( 𝑊 𝑆 ) = ( 1. ‘ 𝐾 ) )
29 13 19 26 28 syl21anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( 𝑊 𝑆 ) = ( 1. ‘ 𝐾 ) )
30 29 oveq2d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( ( 𝑅 𝑆 ) ( 𝑊 𝑆 ) ) = ( ( 𝑅 𝑆 ) ( 1. ‘ 𝐾 ) ) )
31 hlol ( 𝐾 ∈ HL → 𝐾 ∈ OL )
32 13 31 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝐾 ∈ OL )
33 16 3 27 olm11 ( ( 𝐾 ∈ OL ∧ ( 𝑅 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 𝑆 ) ( 1. ‘ 𝐾 ) ) = ( 𝑅 𝑆 ) )
34 32 18 33 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( ( 𝑅 𝑆 ) ( 1. ‘ 𝐾 ) ) = ( 𝑅 𝑆 ) )
35 25 30 34 3eqtrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( ( ( 𝑅 𝑆 ) 𝑊 ) 𝑆 ) = ( 𝑅 𝑆 ) )
36 35 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( ( ( 𝑅 𝑆 ) 𝑊 ) 𝑆 ) = ( 𝑅 𝑆 ) )
37 simp1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) )
38 simp23 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) )
39 simp21 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) )
40 simp31 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( 𝑃𝑄𝑆𝑇 ) )
41 simp321 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ¬ 𝑆 ( 𝑃 𝑄 ) )
42 simp322 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ¬ 𝑇 ( 𝑃 𝑄 ) )
43 41 42 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ) )
44 simp323 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝑅 ( 𝑃 𝑄 ) )
45 1 2 3 4 5 6 7 8 9 10 11 cdleme20d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( 𝐹 𝐺 ) ( 𝐷 𝑌 ) ) = 𝑉 )
46 37 26 38 39 40 43 44 45 syl133anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( ( 𝐹 𝐺 ) ( 𝐷 𝑌 ) ) = 𝑉 )
47 13 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝐾 ∈ Lat )
48 simp12l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝑃𝐴 )
49 simp13l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝑄𝐴 )
50 1 2 3 4 5 6 7 16 cdleme1b ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴𝑆𝐴 ) ) → 𝐹 ∈ ( Base ‘ 𝐾 ) )
51 13 19 48 49 14 50 syl23anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝐹 ∈ ( Base ‘ 𝐾 ) )
52 simp23l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝑇𝐴 )
53 1 2 3 4 5 6 8 16 cdleme1b ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴𝑇𝐴 ) ) → 𝐺 ∈ ( Base ‘ 𝐾 ) )
54 13 19 48 49 52 53 syl23anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝐺 ∈ ( Base ‘ 𝐾 ) )
55 16 2 latjcl ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ ( Base ‘ 𝐾 ) ∧ 𝐺 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐹 𝐺 ) ∈ ( Base ‘ 𝐾 ) )
56 47 51 54 55 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( 𝐹 𝐺 ) ∈ ( Base ‘ 𝐾 ) )
57 simp22r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ¬ 𝑆 𝑊 )
58 1 2 3 4 5 9 cdlemeda ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑅𝐴𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐷𝐴 )
59 13 19 14 57 15 44 41 58 syl223anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝐷𝐴 )
60 simp23r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ¬ 𝑇 𝑊 )
61 1 2 3 4 5 10 cdlemeda ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑅𝐴𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ) ) → 𝑌𝐴 )
62 13 19 52 60 15 44 42 61 syl223anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝑌𝐴 )
63 16 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝐷𝐴𝑌𝐴 ) → ( 𝐷 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
64 13 59 62 63 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( 𝐷 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
65 16 1 3 latmle2 ( ( 𝐾 ∈ Lat ∧ ( 𝐹 𝐺 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐷 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐹 𝐺 ) ( 𝐷 𝑌 ) ) ( 𝐷 𝑌 ) )
66 47 56 64 65 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( ( 𝐹 𝐺 ) ( 𝐷 𝑌 ) ) ( 𝐷 𝑌 ) )
67 46 66 eqbrtrrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝑉 ( 𝐷 𝑌 ) )
68 67 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → 𝑉 ( 𝐷 𝑌 ) )
69 2 4 hlatjidm ( ( 𝐾 ∈ HL ∧ 𝐷𝐴 ) → ( 𝐷 𝐷 ) = 𝐷 )
70 13 59 69 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( 𝐷 𝐷 ) = 𝐷 )
71 oveq2 ( 𝐷 = 𝑌 → ( 𝐷 𝐷 ) = ( 𝐷 𝑌 ) )
72 70 71 sylan9req ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → 𝐷 = ( 𝐷 𝑌 ) )
73 68 72 breqtrrd ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → 𝑉 𝐷 )
74 hlatl ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
75 13 74 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝐾 ∈ AtLat )
76 simp31r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝑆𝑇 )
77 1 2 3 4 5 11 lhpat2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴𝑆𝑇 ) ) → 𝑉𝐴 )
78 13 19 14 57 52 76 77 syl222anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝑉𝐴 )
79 1 4 atcmp ( ( 𝐾 ∈ AtLat ∧ 𝑉𝐴𝐷𝐴 ) → ( 𝑉 𝐷𝑉 = 𝐷 ) )
80 75 78 59 79 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( 𝑉 𝐷𝑉 = 𝐷 ) )
81 80 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( 𝑉 𝐷𝑉 = 𝐷 ) )
82 73 81 mpbid ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → 𝑉 = 𝐷 )
83 82 11 eqtr3di ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → 𝐷 = ( ( 𝑆 𝑇 ) 𝑊 ) )
84 9 83 eqtr3id ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( ( 𝑅 𝑆 ) 𝑊 ) = ( ( 𝑆 𝑇 ) 𝑊 ) )
85 16 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
86 13 14 52 85 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
87 16 1 3 latmle1 ( ( 𝐾 ∈ Lat ∧ ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑆 𝑇 ) 𝑊 ) ( 𝑆 𝑇 ) )
88 47 86 21 87 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( ( 𝑆 𝑇 ) 𝑊 ) ( 𝑆 𝑇 ) )
89 88 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( ( 𝑆 𝑇 ) 𝑊 ) ( 𝑆 𝑇 ) )
90 84 89 eqbrtrd ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( ( 𝑅 𝑆 ) 𝑊 ) ( 𝑆 𝑇 ) )
91 1 2 4 hlatlej1 ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → 𝑆 ( 𝑆 𝑇 ) )
92 13 14 52 91 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝑆 ( 𝑆 𝑇 ) )
93 92 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → 𝑆 ( 𝑆 𝑇 ) )
94 16 3 latmcl ( ( 𝐾 ∈ Lat ∧ ( 𝑅 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 𝑆 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
95 47 18 21 94 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( ( 𝑅 𝑆 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
96 16 4 atbase ( 𝑆𝐴𝑆 ∈ ( Base ‘ 𝐾 ) )
97 14 96 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
98 16 1 2 latjle12 ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑅 𝑆 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑅 𝑆 ) 𝑊 ) ( 𝑆 𝑇 ) ∧ 𝑆 ( 𝑆 𝑇 ) ) ↔ ( ( ( 𝑅 𝑆 ) 𝑊 ) 𝑆 ) ( 𝑆 𝑇 ) ) )
99 47 95 97 86 98 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( ( ( ( 𝑅 𝑆 ) 𝑊 ) ( 𝑆 𝑇 ) ∧ 𝑆 ( 𝑆 𝑇 ) ) ↔ ( ( ( 𝑅 𝑆 ) 𝑊 ) 𝑆 ) ( 𝑆 𝑇 ) ) )
100 99 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( ( ( ( 𝑅 𝑆 ) 𝑊 ) ( 𝑆 𝑇 ) ∧ 𝑆 ( 𝑆 𝑇 ) ) ↔ ( ( ( 𝑅 𝑆 ) 𝑊 ) 𝑆 ) ( 𝑆 𝑇 ) ) )
101 90 93 100 mpbi2and ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( ( ( 𝑅 𝑆 ) 𝑊 ) 𝑆 ) ( 𝑆 𝑇 ) )
102 36 101 eqbrtrrd ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( 𝑅 𝑆 ) ( 𝑆 𝑇 ) )
103 16 4 atbase ( 𝑅𝐴𝑅 ∈ ( Base ‘ 𝐾 ) )
104 15 103 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
105 16 1 2 latjle12 ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ( 𝑆 𝑇 ) ∧ 𝑆 ( 𝑆 𝑇 ) ) ↔ ( 𝑅 𝑆 ) ( 𝑆 𝑇 ) ) )
106 47 104 97 86 105 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( ( 𝑅 ( 𝑆 𝑇 ) ∧ 𝑆 ( 𝑆 𝑇 ) ) ↔ ( 𝑅 𝑆 ) ( 𝑆 𝑇 ) ) )
107 106 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( ( 𝑅 ( 𝑆 𝑇 ) ∧ 𝑆 ( 𝑆 𝑇 ) ) ↔ ( 𝑅 𝑆 ) ( 𝑆 𝑇 ) ) )
108 102 107 mpbird ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → ( 𝑅 ( 𝑆 𝑇 ) ∧ 𝑆 ( 𝑆 𝑇 ) ) )
109 108 simpld ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) ∧ 𝐷 = 𝑌 ) → 𝑅 ( 𝑆 𝑇 ) )
110 109 ex ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( 𝐷 = 𝑌𝑅 ( 𝑆 𝑇 ) ) )
111 110 necon3bd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → ( ¬ 𝑅 ( 𝑆 𝑇 ) → 𝐷𝑌 ) )
112 12 111 mpd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ) ∧ ( ( 𝑃𝑄𝑆𝑇 ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ¬ 𝑅 ( 𝑆 𝑇 ) ) ) → 𝐷𝑌 )