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

Metamath Proof Explorer

Theorem ps-2

Description: Lattice analogue for the projective geometry axiom, "if a line intersects two sides of a triangle at different points then it also intersects the third side." Projective space condition PS2 in MaedaMaeda p. 68 and part of Theorem 16.4 in MaedaMaeda p. 69. (Contributed by NM, 1-Dec-2011)

Ref Expression
Hypotheses ps1.l ⊢ ≤ = ( le ‘ 𝐾 )
ps1.j ⊢ ∨ = ( join ‘ 𝐾 )
ps1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion ps-2 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 ps1.l ⊢ ≤ = ( le ‘ 𝐾 )
2 ps1.j ⊢ ∨ = ( join ‘ 𝐾 )
3 ps1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 simpl21 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑆 = 𝑃 ) → 𝑃 ∈ 𝐴 )
5 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
6 simp21 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 )
7 simp23 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑅 ∈ 𝐴 )
8 1 2 3 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → 𝑃 ≤ ( 𝑃 ∨ 𝑅 ) )
9 5 6 7 8 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑃 ≤ ( 𝑃 ∨ 𝑅 ) )
10 9 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑆 = 𝑃 ) → 𝑃 ≤ ( 𝑃 ∨ 𝑅 ) )
11 simp3r ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑇 ∈ 𝐴 )
12 1 2 3 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → 𝑃 ≤ ( 𝑃 ∨ 𝑇 ) )
13 5 6 11 12 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑃 ≤ ( 𝑃 ∨ 𝑇 ) )
14 oveq1 ⊢ ( 𝑆 = 𝑃 → ( 𝑆 ∨ 𝑇 ) = ( 𝑃 ∨ 𝑇 ) )
15 14 breq2d ⊢ ( 𝑆 = 𝑃 → ( 𝑃 ≤ ( 𝑆 ∨ 𝑇 ) ↔ 𝑃 ≤ ( 𝑃 ∨ 𝑇 ) ) )
16 13 15 syl5ibrcom ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 𝑆 = 𝑃 → 𝑃 ≤ ( 𝑆 ∨ 𝑇 ) ) )
17 16 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑆 = 𝑃 ) → 𝑃 ≤ ( 𝑆 ∨ 𝑇 ) )
18 breq1 ⊢ ( 𝑢 = 𝑃 → ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ↔ 𝑃 ≤ ( 𝑃 ∨ 𝑅 ) ) )
19 breq1 ⊢ ( 𝑢 = 𝑃 → ( 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ↔ 𝑃 ≤ ( 𝑆 ∨ 𝑇 ) ) )
20 18 19 anbi12d ⊢ ( 𝑢 = 𝑃 → ( ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ↔ ( 𝑃 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑃 ≤ ( 𝑆 ∨ 𝑇 ) ) ) )
21 20 rspcev ⊢ ( ( 𝑃 ∈ 𝐴 ∧ ( 𝑃 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑃 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) )
22 4 10 17 21 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑆 = 𝑃 ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) )
23 22 a1d ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑆 = 𝑃 ) → ( ( ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) )
24 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
25 24 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝐾 ∈ OP )
26 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
27 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
28 26 27 op0cl ⊢ ( 𝐾 ∈ OP → ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
29 25 28 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
30 26 3 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
31 6 30 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
32 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
33 27 32 3 atcvr0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( 0. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) 𝑃 )
34 5 6 33 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 0. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) 𝑃 )
35 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
36 26 35 32 cvrlt ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 0. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) 𝑃 ) → ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑃 )
37 5 29 31 34 36 syl31anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑃 )
38 hlpos ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
39 38 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝐾 ∈ Poset )
40 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
41 40 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
42 26 3 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
43 7 42 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
44 26 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
45 41 31 43 44 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
46 26 1 35 pltletr ⊢ ( ( 𝐾 ∈ Poset ∧ ( ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑃 ∧ 𝑃 ≤ ( 𝑃 ∨ 𝑅 ) ) → ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) )
47 39 29 31 45 46 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑃 ∧ 𝑃 ≤ ( 𝑃 ∨ 𝑅 ) ) → ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) )
48 37 9 47 mp2and ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) )
49 35 pltne ⊢ ( ( 𝐾 ∈ HL ∧ ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) → ( 0. ‘ 𝐾 ) ≠ ( 𝑃 ∨ 𝑅 ) ) )
50 5 29 45 49 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) → ( 0. ‘ 𝐾 ) ≠ ( 𝑃 ∨ 𝑅 ) ) )
51 48 50 mpd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 0. ‘ 𝐾 ) ≠ ( 𝑃 ∨ 𝑅 ) )
52 51 necomd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑅 ) ≠ ( 0. ‘ 𝐾 ) )
53 52 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( 𝑆 ≠ 𝑃 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ( 𝑃 ∨ 𝑅 ) ≠ ( 0. ‘ 𝐾 ) )
54 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
55 54 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝐾 ∈ AtLat )
56 simp3l ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑆 ∈ 𝐴 )
57 1 3 atncmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → ( ¬ 𝑆 ≤ 𝑃 ↔ 𝑆 ≠ 𝑃 ) )
58 55 56 6 57 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ¬ 𝑆 ≤ 𝑃 ↔ 𝑆 ≠ 𝑃 ) )
59 simp22 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 )
60 26 1 2 3 hlexch1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑆 ≤ 𝑃 ) → ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ) )
61 60 3expia ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) ) → ( ¬ 𝑆 ≤ 𝑃 → ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ) ) )
62 5 56 59 31 61 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ¬ 𝑆 ≤ 𝑃 → ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ) ) )
63 58 62 sylbird ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 𝑆 ≠ 𝑃 → ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ) ) )
64 63 imp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( 𝑆 ≠ 𝑃 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) )
65 26 3 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
66 59 65 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
67 26 3 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
68 56 67 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
69 26 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
70 41 31 68 69 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
71 26 1 2 latjlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) → ( 𝑄 ∨ 𝑅 ) ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) ) )
72 41 66 70 43 71 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) → ( 𝑄 ∨ 𝑅 ) ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) ) )
73 72 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( 𝑆 ≠ 𝑃 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) → ( 𝑄 ∨ 𝑅 ) ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) ) )
74 64 73 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( 𝑆 ≠ 𝑃 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑄 ∨ 𝑅 ) ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) )
75 74 adantrrr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( 𝑆 ≠ 𝑃 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ( 𝑄 ∨ 𝑅 ) ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) )
76 26 3 atbase ⊢ ( 𝑇 ∈ 𝐴 → 𝑇 ∈ ( Base ‘ 𝐾 ) )
77 11 76 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑇 ∈ ( Base ‘ 𝐾 ) )
78 26 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
79 41 66 43 78 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
80 26 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
81 41 70 43 80 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
82 26 1 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑄 ∨ 𝑅 ) ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) ) → 𝑇 ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) ) )
83 41 77 79 81 82 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑄 ∨ 𝑅 ) ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) ) → 𝑇 ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) ) )
84 83 expdimp ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑄 ∨ 𝑅 ) ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) → 𝑇 ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) ) )
85 84 adantrl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) → 𝑇 ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) ) )
86 85 adantrl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( 𝑆 ≠ 𝑃 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) → 𝑇 ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) ) )
87 75 86 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( 𝑆 ≠ 𝑃 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → 𝑇 ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) )
88 2 3 hlatj32 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) = ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑆 ) )
89 5 6 56 7 88 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) = ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑆 ) )
90 89 breq2d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 𝑇 ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) ↔ 𝑇 ≤ ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑆 ) ) )
91 90 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( 𝑆 ≠ 𝑃 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ( 𝑇 ≤ ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑅 ) ↔ 𝑇 ≤ ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑆 ) ) )
92 87 91 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( 𝑆 ≠ 𝑃 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → 𝑇 ≤ ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑆 ) )
93 53 92 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( 𝑆 ≠ 𝑃 ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ( ( 𝑃 ∨ 𝑅 ) ≠ ( 0. ‘ 𝐾 ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑆 ) ) )
94 93 adantrrl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( 𝑆 ≠ 𝑃 ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) ) → ( ( 𝑃 ∨ 𝑅 ) ≠ ( 0. ‘ 𝐾 ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑆 ) ) )
95 94 ex ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( 𝑆 ≠ 𝑃 ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ( ( 𝑃 ∨ 𝑅 ) ≠ ( 0. ‘ 𝐾 ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑆 ) ) ) )
96 26 1 2 27 3 cvrat4 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑅 ) ≠ ( 0. ‘ 𝐾 ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑆 ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑇 ≤ ( 𝑆 ∨ 𝑢 ) ) ) )
97 5 45 11 56 96 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑅 ) ≠ ( 0. ‘ 𝐾 ) ∧ 𝑇 ≤ ( ( 𝑃 ∨ 𝑅 ) ∨ 𝑆 ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑇 ≤ ( 𝑆 ∨ 𝑢 ) ) ) )
98 95 97 syld ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( 𝑆 ≠ 𝑃 ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑇 ≤ ( 𝑆 ∨ 𝑢 ) ) ) )
99 98 impl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑆 ≠ 𝑃 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑇 ≤ ( 𝑆 ∨ 𝑢 ) ) )
100 99 adantrlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑆 ≠ 𝑃 ) ∧ ( ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑇 ≤ ( 𝑆 ∨ 𝑢 ) ) )
101 1 3 atncmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( ¬ 𝑇 ≤ 𝑆 ↔ 𝑇 ≠ 𝑆 ) )
102 55 11 56 101 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ¬ 𝑇 ≤ 𝑆 ↔ 𝑇 ≠ 𝑆 ) )
103 necom ⊢ ( 𝑇 ≠ 𝑆 ↔ 𝑆 ≠ 𝑇 )
104 102 103 bitrdi ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ¬ 𝑇 ≤ 𝑆 ↔ 𝑆 ≠ 𝑇 ) )
105 104 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( ¬ 𝑇 ≤ 𝑆 ↔ 𝑆 ≠ 𝑇 ) )
106 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → 𝐾 ∈ HL )
107 simpl3r ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → 𝑇 ∈ 𝐴 )
108 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → 𝑢 ∈ 𝐴 )
109 68 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
110 26 1 2 3 hlexch1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑇 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑇 ≤ 𝑆 ) → ( 𝑇 ≤ ( 𝑆 ∨ 𝑢 ) → 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) )
111 110 3expia ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑇 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) ) → ( ¬ 𝑇 ≤ 𝑆 → ( 𝑇 ≤ ( 𝑆 ∨ 𝑢 ) → 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) )
112 106 107 108 109 111 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( ¬ 𝑇 ≤ 𝑆 → ( 𝑇 ≤ ( 𝑆 ∨ 𝑢 ) → 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) )
113 105 112 sylbird ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑆 ≠ 𝑇 → ( 𝑇 ≤ ( 𝑆 ∨ 𝑢 ) → 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) )
114 113 imp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑆 ≠ 𝑇 ) → ( 𝑇 ≤ ( 𝑆 ∨ 𝑢 ) → 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) )
115 114 an32s ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑆 ≠ 𝑇 ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑇 ≤ ( 𝑆 ∨ 𝑢 ) → 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) )
116 115 anim2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑆 ≠ 𝑇 ) ∧ 𝑢 ∈ 𝐴 ) → ( ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑇 ≤ ( 𝑆 ∨ 𝑢 ) ) → ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) )
117 116 reximdva ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑆 ≠ 𝑇 ) → ( ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑇 ≤ ( 𝑆 ∨ 𝑢 ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) )
118 117 ad2ant2rl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑆 ≠ 𝑃 ) ∧ ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ) ) → ( ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑇 ≤ ( 𝑆 ∨ 𝑢 ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) )
119 118 adantrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑆 ≠ 𝑃 ) ∧ ( ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ( ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑇 ≤ ( 𝑆 ∨ 𝑢 ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) )
120 100 119 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑆 ≠ 𝑃 ) ∧ ( ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) )
121 120 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ 𝑆 ≠ 𝑃 ) → ( ( ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) )
122 23 121 pm2.61dane ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) ) )
123 122 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑢 ≤ ( 𝑆 ∨ 𝑇 ) ) )