Metamath Proof Explorer


Theorem cdlemg27b

Description: TODO: Fix comment. (Contributed by NM, 28-May-2013)

Ref Expression
Hypotheses cdlemg12.l = ( le ‘ 𝐾 )
cdlemg12.j = ( join ‘ 𝐾 )
cdlemg12.m = ( meet ‘ 𝐾 )
cdlemg12.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemg12.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemg12.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemg12b.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
cdlemg31.n 𝑁 = ( ( 𝑃 𝑣 ) ( 𝑄 ( 𝑅𝐹 ) ) )
Assertion cdlemg27b ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ¬ ( 𝑅𝐹 ) ( 𝑄 𝑧 ) )

Proof

Step Hyp Ref Expression
1 cdlemg12.l = ( le ‘ 𝐾 )
2 cdlemg12.j = ( join ‘ 𝐾 )
3 cdlemg12.m = ( meet ‘ 𝐾 )
4 cdlemg12.a 𝐴 = ( Atoms ‘ 𝐾 )
5 cdlemg12.h 𝐻 = ( LHyp ‘ 𝐾 )
6 cdlemg12.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7 cdlemg12b.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8 cdlemg31.n 𝑁 = ( ( 𝑃 𝑣 ) ( 𝑄 ( 𝑅𝐹 ) ) )
9 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
10 simp12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
11 simp13 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) )
12 simp22 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ( 𝑣𝐴𝑣 𝑊 ) )
13 simp23l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → 𝐹𝑇 )
14 simp31 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → 𝑣 ≠ ( 𝑅𝐹 ) )
15 1 2 3 4 5 6 7 8 cdlemg31b0a ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑣𝐴𝑣 𝑊 ) ) ∧ ( 𝐹𝑇𝑣 ≠ ( 𝑅𝐹 ) ) ) → ( 𝑁𝐴𝑁 = ( 0. ‘ 𝐾 ) ) )
16 9 10 11 12 13 14 15 syl132anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ( 𝑁𝐴𝑁 = ( 0. ‘ 𝐾 ) ) )
17 simp23r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → 𝑧𝑁 )
18 17 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ ( 𝑁𝐴𝑁 = ( 0. ‘ 𝐾 ) ) ) → 𝑧𝑁 )
19 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → 𝐾 ∈ HL )
20 19 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ 𝑁𝐴 ) → 𝐾 ∈ HL )
21 hlatl ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
22 20 21 syl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ 𝑁𝐴 ) → 𝐾 ∈ AtLat )
23 simpl21 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ 𝑁𝐴 ) → 𝑧𝐴 )
24 simpr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ 𝑁𝐴 ) → 𝑁𝐴 )
25 1 4 atcmp ( ( 𝐾 ∈ AtLat ∧ 𝑧𝐴𝑁𝐴 ) → ( 𝑧 𝑁𝑧 = 𝑁 ) )
26 22 23 24 25 syl3anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ 𝑁𝐴 ) → ( 𝑧 𝑁𝑧 = 𝑁 ) )
27 26 necon3bbid ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ 𝑁𝐴 ) → ( ¬ 𝑧 𝑁𝑧𝑁 ) )
28 19 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ 𝑁 = ( 0. ‘ 𝐾 ) ) → 𝐾 ∈ HL )
29 28 21 syl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ 𝑁 = ( 0. ‘ 𝐾 ) ) → 𝐾 ∈ AtLat )
30 simpl21 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ 𝑁 = ( 0. ‘ 𝐾 ) ) → 𝑧𝐴 )
31 eqid ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
32 1 31 4 atnle0 ( ( 𝐾 ∈ AtLat ∧ 𝑧𝐴 ) → ¬ 𝑧 ( 0. ‘ 𝐾 ) )
33 29 30 32 syl2anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ 𝑁 = ( 0. ‘ 𝐾 ) ) → ¬ 𝑧 ( 0. ‘ 𝐾 ) )
34 simpr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ 𝑁 = ( 0. ‘ 𝐾 ) ) → 𝑁 = ( 0. ‘ 𝐾 ) )
35 34 breq2d ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ 𝑁 = ( 0. ‘ 𝐾 ) ) → ( 𝑧 𝑁𝑧 ( 0. ‘ 𝐾 ) ) )
36 33 35 mtbird ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ 𝑁 = ( 0. ‘ 𝐾 ) ) → ¬ 𝑧 𝑁 )
37 17 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ 𝑁 = ( 0. ‘ 𝐾 ) ) → 𝑧𝑁 )
38 36 37 2thd ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ 𝑁 = ( 0. ‘ 𝐾 ) ) → ( ¬ 𝑧 𝑁𝑧𝑁 ) )
39 27 38 jaodan ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ ( 𝑁𝐴𝑁 = ( 0. ‘ 𝐾 ) ) ) → ( ¬ 𝑧 𝑁𝑧𝑁 ) )
40 18 39 mpbird ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) ∧ ( 𝑁𝐴𝑁 = ( 0. ‘ 𝐾 ) ) ) → ¬ 𝑧 𝑁 )
41 16 40 mpdan ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ¬ 𝑧 𝑁 )
42 simp32 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → 𝑧 ( 𝑃 𝑣 ) )
43 19 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → 𝐾 ∈ Lat )
44 simp21 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → 𝑧𝐴 )
45 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
46 45 4 atbase ( 𝑧𝐴𝑧 ∈ ( Base ‘ 𝐾 ) )
47 44 46 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → 𝑧 ∈ ( Base ‘ 𝐾 ) )
48 simp12l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → 𝑃𝐴 )
49 simp22l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → 𝑣𝐴 )
50 45 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑣𝐴 ) → ( 𝑃 𝑣 ) ∈ ( Base ‘ 𝐾 ) )
51 19 48 49 50 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ( 𝑃 𝑣 ) ∈ ( Base ‘ 𝐾 ) )
52 simp13l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → 𝑄𝐴 )
53 simp33 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ( 𝐹𝑃 ) ≠ 𝑃 )
54 1 4 5 6 7 trlat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝐹𝑇 ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ( 𝑅𝐹 ) ∈ 𝐴 )
55 9 10 13 53 54 syl112anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ( 𝑅𝐹 ) ∈ 𝐴 )
56 45 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑄𝐴 ∧ ( 𝑅𝐹 ) ∈ 𝐴 ) → ( 𝑄 ( 𝑅𝐹 ) ) ∈ ( Base ‘ 𝐾 ) )
57 19 52 55 56 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ( 𝑄 ( 𝑅𝐹 ) ) ∈ ( Base ‘ 𝐾 ) )
58 45 1 3 latlem12 ( ( 𝐾 ∈ Lat ∧ ( 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑣 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ( 𝑅𝐹 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑧 ( 𝑃 𝑣 ) ∧ 𝑧 ( 𝑄 ( 𝑅𝐹 ) ) ) ↔ 𝑧 ( ( 𝑃 𝑣 ) ( 𝑄 ( 𝑅𝐹 ) ) ) ) )
59 43 47 51 57 58 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ( ( 𝑧 ( 𝑃 𝑣 ) ∧ 𝑧 ( 𝑄 ( 𝑅𝐹 ) ) ) ↔ 𝑧 ( ( 𝑃 𝑣 ) ( 𝑄 ( 𝑅𝐹 ) ) ) ) )
60 8 breq2i ( 𝑧 𝑁𝑧 ( ( 𝑃 𝑣 ) ( 𝑄 ( 𝑅𝐹 ) ) ) )
61 59 60 bitr4di ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ( ( 𝑧 ( 𝑃 𝑣 ) ∧ 𝑧 ( 𝑄 ( 𝑅𝐹 ) ) ) ↔ 𝑧 𝑁 ) )
62 61 biimpd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ( ( 𝑧 ( 𝑃 𝑣 ) ∧ 𝑧 ( 𝑄 ( 𝑅𝐹 ) ) ) → 𝑧 𝑁 ) )
63 42 62 mpand ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ( 𝑧 ( 𝑄 ( 𝑅𝐹 ) ) → 𝑧 𝑁 ) )
64 41 63 mtod ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ¬ 𝑧 ( 𝑄 ( 𝑅𝐹 ) ) )
65 1 5 6 7 trlle ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝑅𝐹 ) 𝑊 )
66 9 13 65 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ( 𝑅𝐹 ) 𝑊 )
67 simp13r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ¬ 𝑄 𝑊 )
68 nbrne2 ( ( ( 𝑅𝐹 ) 𝑊 ∧ ¬ 𝑄 𝑊 ) → ( 𝑅𝐹 ) ≠ 𝑄 )
69 66 67 68 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ( 𝑅𝐹 ) ≠ 𝑄 )
70 1 2 4 hlatexch1 ( ( 𝐾 ∈ HL ∧ ( ( 𝑅𝐹 ) ∈ 𝐴𝑧𝐴𝑄𝐴 ) ∧ ( 𝑅𝐹 ) ≠ 𝑄 ) → ( ( 𝑅𝐹 ) ( 𝑄 𝑧 ) → 𝑧 ( 𝑄 ( 𝑅𝐹 ) ) ) )
71 19 55 44 52 69 70 syl131anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ( ( 𝑅𝐹 ) ( 𝑄 𝑧 ) → 𝑧 ( 𝑄 ( 𝑅𝐹 ) ) ) )
72 64 71 mtod ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑣𝐴𝑣 𝑊 ) ∧ ( 𝐹𝑇𝑧𝑁 ) ) ∧ ( 𝑣 ≠ ( 𝑅𝐹 ) ∧ 𝑧 ( 𝑃 𝑣 ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) ) → ¬ ( 𝑅𝐹 ) ( 𝑄 𝑧 ) )