Metamath Proof Explorer


Theorem 2lplnja

Description: The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj in terms of atoms). (Contributed by NM, 12-Jul-2012)

Ref Expression
Hypotheses 2lplnja.l = ( le ‘ 𝐾 )
2lplnja.j = ( join ‘ 𝐾 )
2lplnja.a 𝐴 = ( Atoms ‘ 𝐾 )
2lplnja.v 𝑉 = ( LVols ‘ 𝐾 )
Assertion 2lplnja ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) = 𝑊 )

Proof

Step Hyp Ref Expression
1 2lplnja.l = ( le ‘ 𝐾 )
2 2lplnja.j = ( join ‘ 𝐾 )
3 2lplnja.a 𝐴 = ( Atoms ‘ 𝐾 )
4 2lplnja.v 𝑉 = ( LVols ‘ 𝐾 )
5 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝐾 ∈ HL )
7 6 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝐾 ∈ Lat )
8 simp121 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑃𝐴 )
9 simp122 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑄𝐴 )
10 5 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
11 6 8 9 10 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
12 simp123 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑅𝐴 )
13 5 3 atbase ( 𝑅𝐴𝑅 ∈ ( Base ‘ 𝐾 ) )
14 12 13 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
15 5 2 latjcl ( ( 𝐾 ∈ Lat ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
16 7 11 14 15 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
17 simp2l1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑆𝐴 )
18 simp2l2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑇𝐴 )
19 5 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
20 6 17 18 19 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
21 simp2l3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑈𝐴 )
22 5 3 atbase ( 𝑈𝐴𝑈 ∈ ( Base ‘ 𝐾 ) )
23 21 22 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑈 ∈ ( Base ‘ 𝐾 ) )
24 5 2 latjcl ( ( 𝐾 ∈ Lat ∧ ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
25 7 20 23 24 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
26 5 2 latjcl ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ∈ ( Base ‘ 𝐾 ) )
27 7 16 25 26 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ∈ ( Base ‘ 𝐾 ) )
28 simp11r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑊𝑉 )
29 5 4 lvolbase ( 𝑊𝑉𝑊 ∈ ( Base ‘ 𝐾 ) )
30 28 29 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
31 simp31 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 )
32 simp32 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 )
33 5 1 2 latjle12 ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ) ↔ ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) 𝑊 ) )
34 7 16 25 30 33 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ) ↔ ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) 𝑊 ) )
35 31 32 34 mpbi2and ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) 𝑊 )
36 5 1 2 latlej2 ( ( 𝐾 ∈ Lat ∧ ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) → 𝑈 ( ( 𝑆 𝑇 ) 𝑈 ) )
37 7 20 23 36 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑈 ( ( 𝑆 𝑇 ) 𝑈 ) )
38 5 1 7 23 25 30 37 32 lattrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑈 𝑊 )
39 5 1 2 latjle12 ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊𝑈 𝑊 ) ↔ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑈 ) 𝑊 ) )
40 7 16 23 30 39 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊𝑈 𝑊 ) ↔ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑈 ) 𝑊 ) )
41 31 38 40 mpbi2and ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑈 ) 𝑊 )
42 41 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑈 ) 𝑊 )
43 6 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → 𝐾 ∈ HL )
44 6 8 9 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) )
45 44 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) )
46 12 21 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( 𝑅𝐴𝑈𝐴 ) )
47 46 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( 𝑅𝐴𝑈𝐴 ) )
48 simp13l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑃𝑄 )
49 48 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → 𝑃𝑄 )
50 simp13r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ¬ 𝑅 ( 𝑃 𝑄 ) )
51 50 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ¬ 𝑅 ( 𝑃 𝑄 ) )
52 simp33 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) )
53 52 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) )
54 simplr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) )
55 simpr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) )
56 5 3 atbase ( 𝑆𝐴𝑆 ∈ ( Base ‘ 𝐾 ) )
57 17 56 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
58 5 3 atbase ( 𝑇𝐴𝑇 ∈ ( Base ‘ 𝐾 ) )
59 18 58 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑇 ∈ ( Base ‘ 𝐾 ) )
60 5 1 2 latjle12 ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) ↔ ( 𝑆 𝑇 ) ( ( 𝑃 𝑄 ) 𝑅 ) ) )
61 7 57 59 16 60 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) ↔ ( 𝑆 𝑇 ) ( ( 𝑃 𝑄 ) 𝑅 ) ) )
62 61 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) ↔ ( 𝑆 𝑇 ) ( ( 𝑃 𝑄 ) 𝑅 ) ) )
63 54 55 62 mpbi2and ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( 𝑆 𝑇 ) ( ( 𝑃 𝑄 ) 𝑅 ) )
64 63 adantr ( ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑈 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( 𝑆 𝑇 ) ( ( 𝑃 𝑄 ) 𝑅 ) )
65 simpr ( ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑈 ( ( 𝑃 𝑄 ) 𝑅 ) ) → 𝑈 ( ( 𝑃 𝑄 ) 𝑅 ) )
66 5 1 2 latjle12 ( ( 𝐾 ∈ Lat ∧ ( ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑆 𝑇 ) ( ( 𝑃 𝑄 ) 𝑅 ) ∧ 𝑈 ( ( 𝑃 𝑄 ) 𝑅 ) ) ↔ ( ( 𝑆 𝑇 ) 𝑈 ) ( ( 𝑃 𝑄 ) 𝑅 ) ) )
67 7 20 23 16 66 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( ( 𝑆 𝑇 ) ( ( 𝑃 𝑄 ) 𝑅 ) ∧ 𝑈 ( ( 𝑃 𝑄 ) 𝑅 ) ) ↔ ( ( 𝑆 𝑇 ) 𝑈 ) ( ( 𝑃 𝑄 ) 𝑅 ) ) )
68 67 ad3antrrr ( ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑈 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( 𝑆 𝑇 ) ( ( 𝑃 𝑄 ) 𝑅 ) ∧ 𝑈 ( ( 𝑃 𝑄 ) 𝑅 ) ) ↔ ( ( 𝑆 𝑇 ) 𝑈 ) ( ( 𝑃 𝑄 ) 𝑅 ) ) )
69 64 65 68 mpbi2and ( ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑈 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) ( ( 𝑃 𝑄 ) 𝑅 ) )
70 simp2l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) )
71 simp12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) )
72 simp2rr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ¬ 𝑈 ( 𝑆 𝑇 ) )
73 simp2rl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑆𝑇 )
74 1 2 3 3at ( ( ( 𝐾 ∈ HL ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( ¬ 𝑈 ( 𝑆 𝑇 ) ∧ 𝑆𝑇 ) ) → ( ( ( 𝑆 𝑇 ) 𝑈 ) ( ( 𝑃 𝑄 ) 𝑅 ) ↔ ( ( 𝑆 𝑇 ) 𝑈 ) = ( ( 𝑃 𝑄 ) 𝑅 ) ) )
75 6 70 71 72 73 74 syl32anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( ( 𝑆 𝑇 ) 𝑈 ) ( ( 𝑃 𝑄 ) 𝑅 ) ↔ ( ( 𝑆 𝑇 ) 𝑈 ) = ( ( 𝑃 𝑄 ) 𝑅 ) ) )
76 75 ad3antrrr ( ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑈 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( 𝑆 𝑇 ) 𝑈 ) ( ( 𝑃 𝑄 ) 𝑅 ) ↔ ( ( 𝑆 𝑇 ) 𝑈 ) = ( ( 𝑃 𝑄 ) 𝑅 ) ) )
77 69 76 mpbid ( ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑈 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) = ( ( 𝑃 𝑄 ) 𝑅 ) )
78 77 eqcomd ( ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑈 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) )
79 78 ex ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( 𝑈 ( ( 𝑃 𝑄 ) 𝑅 ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) ) )
80 79 necon3ad ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) → ¬ 𝑈 ( ( 𝑃 𝑄 ) 𝑅 ) ) )
81 53 80 mpd ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ¬ 𝑈 ( ( 𝑃 𝑄 ) 𝑅 ) )
82 1 2 3 4 lvoli2 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑈𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑈 ) ∈ 𝑉 )
83 45 47 49 51 81 82 syl113anc ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑈 ) ∈ 𝑉 )
84 28 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → 𝑊𝑉 )
85 1 4 lvolcmp ( ( 𝐾 ∈ HL ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑈 ) ∈ 𝑉𝑊𝑉 ) → ( ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑈 ) 𝑊 ↔ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑈 ) = 𝑊 ) )
86 43 83 84 85 syl3anc ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑈 ) 𝑊 ↔ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑈 ) = 𝑊 ) )
87 42 86 mpbid ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑈 ) = 𝑊 )
88 5 1 2 latjlej2 ( ( 𝐾 ∈ Lat ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑈 ( ( 𝑆 𝑇 ) 𝑈 ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑈 ) ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ) )
89 7 23 25 16 88 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( 𝑈 ( ( 𝑆 𝑇 ) 𝑈 ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑈 ) ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ) )
90 37 89 mpd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑈 ) ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
91 90 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑈 ) ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
92 87 91 eqbrtrrd ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → 𝑊 ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
93 5 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑈𝐴 ) → ( 𝑆 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
94 6 17 21 93 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( 𝑆 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
95 5 1 2 latlej2 ( ( 𝐾 ∈ Lat ∧ ( 𝑆 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) → 𝑇 ( ( 𝑆 𝑈 ) 𝑇 ) )
96 7 94 59 95 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑇 ( ( 𝑆 𝑈 ) 𝑇 ) )
97 2 3 hlatj32 ( ( 𝐾 ∈ HL ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) = ( ( 𝑆 𝑈 ) 𝑇 ) )
98 6 17 18 21 97 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) = ( ( 𝑆 𝑈 ) 𝑇 ) )
99 96 98 breqtrrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑇 ( ( 𝑆 𝑇 ) 𝑈 ) )
100 5 1 7 59 25 30 99 32 lattrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑇 𝑊 )
101 5 1 2 latjle12 ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊𝑇 𝑊 ) ↔ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑇 ) 𝑊 ) )
102 7 16 59 30 101 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊𝑇 𝑊 ) ↔ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑇 ) 𝑊 ) )
103 31 100 102 mpbi2and ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑇 ) 𝑊 )
104 103 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑇 ) 𝑊 )
105 6 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → 𝐾 ∈ HL )
106 44 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) )
107 12 18 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( 𝑅𝐴𝑇𝐴 ) )
108 107 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( 𝑅𝐴𝑇𝐴 ) )
109 48 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → 𝑃𝑄 )
110 50 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ¬ 𝑅 ( 𝑃 𝑄 ) )
111 simpr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ¬ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) )
112 1 2 3 4 lvoli2 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑇𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑇 ) ∈ 𝑉 )
113 106 108 109 110 111 112 syl113anc ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑇 ) ∈ 𝑉 )
114 28 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → 𝑊𝑉 )
115 1 4 lvolcmp ( ( 𝐾 ∈ HL ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑇 ) ∈ 𝑉𝑊𝑉 ) → ( ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑇 ) 𝑊 ↔ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑇 ) = 𝑊 ) )
116 105 113 114 115 syl3anc ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑇 ) 𝑊 ↔ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑇 ) = 𝑊 ) )
117 104 116 mpbid ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑇 ) = 𝑊 )
118 5 1 2 latjlej2 ( ( 𝐾 ∈ Lat ∧ ( 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑇 ( ( 𝑆 𝑇 ) 𝑈 ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑇 ) ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ) )
119 7 59 25 16 118 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( 𝑇 ( ( 𝑆 𝑇 ) 𝑈 ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑇 ) ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ) )
120 99 119 mpd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑇 ) ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
121 120 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑇 ) ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
122 117 121 eqbrtrrd ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ) → 𝑊 ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
123 92 122 pm2.61dan ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) → 𝑊 ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
124 5 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴 ) → ( 𝑇 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
125 6 18 21 124 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( 𝑇 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
126 5 1 2 latlej1 ( ( 𝐾 ∈ Lat ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑇 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) → 𝑆 ( 𝑆 ( 𝑇 𝑈 ) ) )
127 7 57 125 126 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑆 ( 𝑆 ( 𝑇 𝑈 ) ) )
128 5 2 latjass ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) = ( 𝑆 ( 𝑇 𝑈 ) ) )
129 7 57 59 23 128 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) = ( 𝑆 ( 𝑇 𝑈 ) ) )
130 127 129 breqtrrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑆 ( ( 𝑆 𝑇 ) 𝑈 ) )
131 5 1 7 57 25 30 130 32 lattrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑆 𝑊 )
132 5 1 2 latjle12 ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊𝑆 𝑊 ) ↔ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑆 ) 𝑊 ) )
133 7 16 57 30 132 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊𝑆 𝑊 ) ↔ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑆 ) 𝑊 ) )
134 31 131 133 mpbi2and ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑆 ) 𝑊 )
135 134 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑆 ) 𝑊 )
136 6 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) → 𝐾 ∈ HL )
137 44 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) )
138 12 17 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( 𝑅𝐴𝑆𝐴 ) )
139 138 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( 𝑅𝐴𝑆𝐴 ) )
140 48 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) → 𝑃𝑄 )
141 50 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ¬ 𝑅 ( 𝑃 𝑄 ) )
142 simpr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) )
143 1 2 3 4 lvoli2 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑆 ) ∈ 𝑉 )
144 137 139 140 141 142 143 syl113anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑆 ) ∈ 𝑉 )
145 28 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) → 𝑊𝑉 )
146 1 4 lvolcmp ( ( 𝐾 ∈ HL ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑆 ) ∈ 𝑉𝑊𝑉 ) → ( ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑆 ) 𝑊 ↔ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑆 ) = 𝑊 ) )
147 136 144 145 146 syl3anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑆 ) 𝑊 ↔ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑆 ) = 𝑊 ) )
148 135 147 mpbid ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑆 ) = 𝑊 )
149 5 1 2 latjlej2 ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑆 ( ( 𝑆 𝑇 ) 𝑈 ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑆 ) ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ) )
150 7 57 25 16 149 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( 𝑆 ( ( 𝑆 𝑇 ) 𝑈 ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑆 ) ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ) )
151 130 150 mpd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑆 ) ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
152 151 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑆 ) ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
153 148 152 eqbrtrrd ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) → 𝑊 ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
154 123 153 pm2.61dan ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → 𝑊 ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
155 5 1 7 27 30 35 154 latasymd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝑉 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ∧ ( 𝑆𝑇 ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) ∧ ( ( ( 𝑃 𝑄 ) 𝑅 ) 𝑊 ∧ ( ( 𝑆 𝑇 ) 𝑈 ) 𝑊 ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ≠ ( ( 𝑆 𝑇 ) 𝑈 ) ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) = 𝑊 )