Metamath Proof Explorer


Theorem 3dim3

Description: Construct a new layer on top of 3 given atoms. (Contributed by NM, 27-Jul-2012)

Ref Expression
Hypotheses 3dim0.j = ( join ‘ 𝐾 )
3dim0.l = ( le ‘ 𝐾 )
3dim0.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 3dim3 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ∃ 𝑠𝐴 ¬ 𝑠 ( ( 𝑃 𝑄 ) 𝑅 ) )

Proof

Step Hyp Ref Expression
1 3dim0.j = ( join ‘ 𝐾 )
2 3dim0.l = ( le ‘ 𝐾 )
3 3dim0.a 𝐴 = ( Atoms ‘ 𝐾 )
4 1 2 3 3dim2 ( ( 𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴 ) → ∃ 𝑣𝐴𝑤𝐴 ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) )
5 4 3adant3r1 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ∃ 𝑣𝐴𝑤𝐴 ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) )
6 simpl2l ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → 𝑣𝐴 )
7 simp3l ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → ¬ 𝑣 ( 𝑄 𝑅 ) )
8 simp1l ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → 𝐾 ∈ HL )
9 simp1r2 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → 𝑄𝐴 )
10 1 3 hlatjidm ( ( 𝐾 ∈ HL ∧ 𝑄𝐴 ) → ( 𝑄 𝑄 ) = 𝑄 )
11 8 9 10 syl2anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → ( 𝑄 𝑄 ) = 𝑄 )
12 11 oveq1d ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → ( ( 𝑄 𝑄 ) 𝑅 ) = ( 𝑄 𝑅 ) )
13 12 breq2d ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → ( 𝑣 ( ( 𝑄 𝑄 ) 𝑅 ) ↔ 𝑣 ( 𝑄 𝑅 ) ) )
14 7 13 mtbird ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → ¬ 𝑣 ( ( 𝑄 𝑄 ) 𝑅 ) )
15 oveq1 ( 𝑃 = 𝑄 → ( 𝑃 𝑄 ) = ( 𝑄 𝑄 ) )
16 15 oveq1d ( 𝑃 = 𝑄 → ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑄 𝑄 ) 𝑅 ) )
17 16 breq2d ( 𝑃 = 𝑄 → ( 𝑣 ( ( 𝑃 𝑄 ) 𝑅 ) ↔ 𝑣 ( ( 𝑄 𝑄 ) 𝑅 ) ) )
18 17 notbid ( 𝑃 = 𝑄 → ( ¬ 𝑣 ( ( 𝑃 𝑄 ) 𝑅 ) ↔ ¬ 𝑣 ( ( 𝑄 𝑄 ) 𝑅 ) ) )
19 18 biimparc ( ( ¬ 𝑣 ( ( 𝑄 𝑄 ) 𝑅 ) ∧ 𝑃 = 𝑄 ) → ¬ 𝑣 ( ( 𝑃 𝑄 ) 𝑅 ) )
20 14 19 sylan ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → ¬ 𝑣 ( ( 𝑃 𝑄 ) 𝑅 ) )
21 breq1 ( 𝑠 = 𝑣 → ( 𝑠 ( ( 𝑃 𝑄 ) 𝑅 ) ↔ 𝑣 ( ( 𝑃 𝑄 ) 𝑅 ) ) )
22 21 notbid ( 𝑠 = 𝑣 → ( ¬ 𝑠 ( ( 𝑃 𝑄 ) 𝑅 ) ↔ ¬ 𝑣 ( ( 𝑃 𝑄 ) 𝑅 ) ) )
23 22 rspcev ( ( 𝑣𝐴 ∧ ¬ 𝑣 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ∃ 𝑠𝐴 ¬ 𝑠 ( ( 𝑃 𝑄 ) 𝑅 ) )
24 6 20 23 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → ∃ 𝑠𝐴 ¬ 𝑠 ( ( 𝑃 𝑄 ) 𝑅 ) )
25 simp2l ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → 𝑣𝐴 )
26 25 ad2antrr ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ 𝑃 ( 𝑄 𝑅 ) ) → 𝑣𝐴 )
27 7 ad2antrr ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ 𝑃 ( 𝑄 𝑅 ) ) → ¬ 𝑣 ( 𝑄 𝑅 ) )
28 1 3 hlatjass ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( 𝑃 ( 𝑄 𝑅 ) ) )
29 28 3ad2ant1 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( 𝑃 ( 𝑄 𝑅 ) ) )
30 29 ad2antrr ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ 𝑃 ( 𝑄 𝑅 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( 𝑃 ( 𝑄 𝑅 ) ) )
31 8 hllatd ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → 𝐾 ∈ Lat )
32 simp1r1 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → 𝑃𝐴 )
33 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
34 33 3 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
35 32 34 syl ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
36 simp1r3 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → 𝑅𝐴 )
37 33 1 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴 ) → ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
38 8 9 36 37 syl3anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
39 31 35 38 3jca ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) )
40 39 adantr ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) → ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) )
41 33 2 1 latleeqj1 ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ( 𝑄 𝑅 ) ↔ ( 𝑃 ( 𝑄 𝑅 ) ) = ( 𝑄 𝑅 ) ) )
42 40 41 syl ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) → ( 𝑃 ( 𝑄 𝑅 ) ↔ ( 𝑃 ( 𝑄 𝑅 ) ) = ( 𝑄 𝑅 ) ) )
43 42 biimpa ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ 𝑃 ( 𝑄 𝑅 ) ) → ( 𝑃 ( 𝑄 𝑅 ) ) = ( 𝑄 𝑅 ) )
44 30 43 eqtrd ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ 𝑃 ( 𝑄 𝑅 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( 𝑄 𝑅 ) )
45 44 breq2d ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ 𝑃 ( 𝑄 𝑅 ) ) → ( 𝑣 ( ( 𝑃 𝑄 ) 𝑅 ) ↔ 𝑣 ( 𝑄 𝑅 ) ) )
46 27 45 mtbird ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ 𝑃 ( 𝑄 𝑅 ) ) → ¬ 𝑣 ( ( 𝑃 𝑄 ) 𝑅 ) )
47 26 46 23 syl2anc ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ 𝑃 ( 𝑄 𝑅 ) ) → ∃ 𝑠𝐴 ¬ 𝑠 ( ( 𝑃 𝑄 ) 𝑅 ) )
48 simpl2r ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) → 𝑤𝐴 )
49 48 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) → 𝑤𝐴 )
50 8 32 9 3jca ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) )
51 50 ad3antrrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) → ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) )
52 36 25 jca ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → ( 𝑅𝐴𝑣𝐴 ) )
53 52 ad3antrrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) → ( 𝑅𝐴𝑣𝐴 ) )
54 simpl3r ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) → ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) )
55 54 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) → ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) )
56 simplr ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) → ¬ 𝑃 ( 𝑄 𝑅 ) )
57 simpr ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) → 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) )
58 1 2 3 3dimlem3a ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑣𝐴 ) ∧ ( ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → ¬ 𝑤 ( ( 𝑃 𝑄 ) 𝑅 ) )
59 51 53 55 56 57 58 syl113anc ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) → ¬ 𝑤 ( ( 𝑃 𝑄 ) 𝑅 ) )
60 breq1 ( 𝑠 = 𝑤 → ( 𝑠 ( ( 𝑃 𝑄 ) 𝑅 ) ↔ 𝑤 ( ( 𝑃 𝑄 ) 𝑅 ) ) )
61 60 notbid ( 𝑠 = 𝑤 → ( ¬ 𝑠 ( ( 𝑃 𝑄 ) 𝑅 ) ↔ ¬ 𝑤 ( ( 𝑃 𝑄 ) 𝑅 ) ) )
62 61 rspcev ( ( 𝑤𝐴 ∧ ¬ 𝑤 ( ( 𝑃 𝑄 ) 𝑅 ) ) → ∃ 𝑠𝐴 ¬ 𝑠 ( ( 𝑃 𝑄 ) 𝑅 ) )
63 49 59 62 syl2anc ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) → ∃ 𝑠𝐴 ¬ 𝑠 ( ( 𝑃 𝑄 ) 𝑅 ) )
64 simpl2l ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) → 𝑣𝐴 )
65 64 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) → 𝑣𝐴 )
66 50 ad3antrrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) → ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) )
67 52 ad3antrrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) → ( 𝑅𝐴𝑣𝐴 ) )
68 simpl3l ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) → ¬ 𝑣 ( 𝑄 𝑅 ) )
69 68 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) → ¬ 𝑣 ( 𝑄 𝑅 ) )
70 simplr ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) → ¬ 𝑃 ( 𝑄 𝑅 ) )
71 simpr ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) → ¬ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) )
72 1 2 3 3dimlem4a ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑣𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ ¬ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → ¬ 𝑣 ( ( 𝑃 𝑄 ) 𝑅 ) )
73 66 67 69 70 71 72 syl113anc ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) → ¬ 𝑣 ( ( 𝑃 𝑄 ) 𝑅 ) )
74 65 73 23 syl2anc ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑄 𝑅 ) 𝑣 ) ) → ∃ 𝑠𝐴 ¬ 𝑠 ( ( 𝑃 𝑄 ) 𝑅 ) )
75 63 74 pm2.61dan ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) → ∃ 𝑠𝐴 ¬ 𝑠 ( ( 𝑃 𝑄 ) 𝑅 ) )
76 47 75 pm2.61dan ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) ∧ 𝑃𝑄 ) → ∃ 𝑠𝐴 ¬ 𝑠 ( ( 𝑃 𝑄 ) 𝑅 ) )
77 24 76 pm2.61dane ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) ∧ ( 𝑣𝐴𝑤𝐴 ) ∧ ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) ) → ∃ 𝑠𝐴 ¬ 𝑠 ( ( 𝑃 𝑄 ) 𝑅 ) )
78 77 3exp ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( ( 𝑣𝐴𝑤𝐴 ) → ( ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) → ∃ 𝑠𝐴 ¬ 𝑠 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) )
79 78 rexlimdvv ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( ∃ 𝑣𝐴𝑤𝐴 ( ¬ 𝑣 ( 𝑄 𝑅 ) ∧ ¬ 𝑤 ( ( 𝑄 𝑅 ) 𝑣 ) ) → ∃ 𝑠𝐴 ¬ 𝑠 ( ( 𝑃 𝑄 ) 𝑅 ) ) )
80 5 79 mpd ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ∃ 𝑠𝐴 ¬ 𝑠 ( ( 𝑃 𝑄 ) 𝑅 ) )