Metamath Proof Explorer


Theorem cdlemh

Description: Lemma H of Crawley p. 118. (Contributed by NM, 17-Jun-2013)

Ref Expression
Hypotheses cdlemh.b 𝐵 = ( Base ‘ 𝐾 )
cdlemh.l = ( le ‘ 𝐾 )
cdlemh.j = ( join ‘ 𝐾 )
cdlemh.m = ( meet ‘ 𝐾 )
cdlemh.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemh.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemh.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemh.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
cdlemh.s 𝑆 = ( ( 𝑃 ( 𝑅𝐺 ) ) ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) )
Assertion cdlemh ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) )

Proof

Step Hyp Ref Expression
1 cdlemh.b 𝐵 = ( Base ‘ 𝐾 )
2 cdlemh.l = ( le ‘ 𝐾 )
3 cdlemh.j = ( join ‘ 𝐾 )
4 cdlemh.m = ( meet ‘ 𝐾 )
5 cdlemh.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemh.h 𝐻 = ( LHyp ‘ 𝐾 )
7 cdlemh.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8 cdlemh.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
9 cdlemh.s 𝑆 = ( ( 𝑃 ( 𝑅𝐺 ) ) ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) )
10 simp1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) )
11 simp21l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝑃𝐴 )
12 simp22l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝑄𝐴 )
13 simp23 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) )
14 simp33 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) )
15 1 2 3 4 5 6 7 8 9 cdlemh1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑆 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) = ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) )
16 10 11 12 13 14 15 syl122anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑆 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) = ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) )
17 oveq1 ( 𝑆 = ( 0. ‘ 𝐾 ) → ( 𝑆 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) = ( ( 0. ‘ 𝐾 ) ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) )
18 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝐾 ∈ HL )
19 hlol ( 𝐾 ∈ HL → 𝐾 ∈ OL )
20 18 19 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝐾 ∈ OL )
21 simp11r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝑊𝐻 )
22 18 21 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
23 simp13 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝐺𝑇 )
24 simp12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝐹𝑇 )
25 6 7 ltrncnv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝐹𝑇 )
26 22 24 25 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝐹𝑇 )
27 23 26 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝐺𝑇 𝐹𝑇 ) )
28 14 necomd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑅𝐺 ) ≠ ( 𝑅𝐹 ) )
29 6 7 8 trlcnv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝑅 𝐹 ) = ( 𝑅𝐹 ) )
30 22 24 29 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑅 𝐹 ) = ( 𝑅𝐹 ) )
31 28 30 neeqtrrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑅𝐺 ) ≠ ( 𝑅 𝐹 ) )
32 5 6 7 8 trlcoat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐺𝑇 𝐹𝑇 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅 𝐹 ) ) → ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ∈ 𝐴 )
33 22 27 31 32 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ∈ 𝐴 )
34 1 5 atbase ( ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ∈ 𝐴 → ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ∈ 𝐵 )
35 33 34 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ∈ 𝐵 )
36 eqid ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
37 1 3 36 olj02 ( ( 𝐾 ∈ OL ∧ ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ∈ 𝐵 ) → ( ( 0. ‘ 𝐾 ) ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) = ( 𝑅 ‘ ( 𝐺 𝐹 ) ) )
38 20 35 37 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( ( 0. ‘ 𝐾 ) ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) = ( 𝑅 ‘ ( 𝐺 𝐹 ) ) )
39 17 38 sylan9eqr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) → ( 𝑆 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) = ( 𝑅 ‘ ( 𝐺 𝐹 ) ) )
40 6 7 ltrnco ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 𝐹𝑇 ) → ( 𝐺 𝐹 ) ∈ 𝑇 )
41 22 23 26 40 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝐺 𝐹 ) ∈ 𝑇 )
42 2 6 7 8 trlle ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐺 𝐹 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝐺 𝐹 ) ) 𝑊 )
43 22 41 42 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐺 𝐹 ) ) 𝑊 )
44 simp22r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ¬ 𝑄 𝑊 )
45 nbrne2 ( ( ( 𝑅 ‘ ( 𝐺 𝐹 ) ) 𝑊 ∧ ¬ 𝑄 𝑊 ) → ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ≠ 𝑄 )
46 45 necomd ( ( ( 𝑅 ‘ ( 𝐺 𝐹 ) ) 𝑊 ∧ ¬ 𝑄 𝑊 ) → 𝑄 ≠ ( 𝑅 ‘ ( 𝐺 𝐹 ) ) )
47 43 44 46 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝑄 ≠ ( 𝑅 ‘ ( 𝐺 𝐹 ) ) )
48 eqid ( LLines ‘ 𝐾 ) = ( LLines ‘ 𝐾 )
49 3 5 48 llni2 ( ( ( 𝐾 ∈ HL ∧ 𝑄𝐴 ∧ ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ∈ 𝐴 ) ∧ 𝑄 ≠ ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) → ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ∈ ( LLines ‘ 𝐾 ) )
50 18 12 33 47 49 syl31anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ∈ ( LLines ‘ 𝐾 ) )
51 5 48 llnneat ( ( 𝐾 ∈ HL ∧ ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ∈ ( LLines ‘ 𝐾 ) ) → ¬ ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ∈ 𝐴 )
52 18 50 51 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ¬ ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ∈ 𝐴 )
53 nelne2 ( ( ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ∈ 𝐴 ∧ ¬ ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ∈ 𝐴 ) → ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ≠ ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) )
54 33 52 53 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ≠ ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) )
55 54 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) → ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ≠ ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) )
56 39 55 eqnetrd ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ 𝑆 = ( 0. ‘ 𝐾 ) ) → ( 𝑆 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ≠ ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) )
57 56 ex ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑆 = ( 0. ‘ 𝐾 ) → ( 𝑆 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ≠ ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ) )
58 57 necon2d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( ( 𝑆 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) = ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) → 𝑆 ≠ ( 0. ‘ 𝐾 ) ) )
59 16 58 mpd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝑆 ≠ ( 0. ‘ 𝐾 ) )
60 simp32 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝐺 ≠ ( I ↾ 𝐵 ) )
61 1 5 6 7 8 trlnidat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) → ( 𝑅𝐺 ) ∈ 𝐴 )
62 22 23 60 61 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑅𝐺 ) ∈ 𝐴 )
63 2 3 5 hlatlej2 ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ∧ ( 𝑅𝐺 ) ∈ 𝐴 ) → ( 𝑅𝐺 ) ( 𝑃 ( 𝑅𝐺 ) ) )
64 18 11 62 63 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑅𝐺 ) ( 𝑃 ( 𝑅𝐺 ) ) )
65 simp22 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) )
66 simp31 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
67 1 6 7 ltrncnvnid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
68 22 24 66 67 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
69 1 6 7 8 trlcone ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐺𝑇 𝐹𝑇 ) ∧ ( ( 𝑅𝐺 ) ≠ ( 𝑅 𝐹 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑅𝐺 ) ≠ ( 𝑅 ‘ ( 𝐺 𝐹 ) ) )
70 69 necomd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐺𝑇 𝐹𝑇 ) ∧ ( ( 𝑅𝐺 ) ≠ ( 𝑅 𝐹 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ≠ ( 𝑅𝐺 ) )
71 22 23 26 31 68 70 syl122anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ≠ ( 𝑅𝐺 ) )
72 2 6 7 8 trlle ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 ) → ( 𝑅𝐺 ) 𝑊 )
73 22 23 72 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑅𝐺 ) 𝑊 )
74 2 3 5 6 lhp2atnle ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ≠ ( 𝑅𝐺 ) ) ∧ ( ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ∈ 𝐴 ∧ ( 𝑅 ‘ ( 𝐺 𝐹 ) ) 𝑊 ) ∧ ( ( 𝑅𝐺 ) ∈ 𝐴 ∧ ( 𝑅𝐺 ) 𝑊 ) ) → ¬ ( 𝑅𝐺 ) ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) )
75 22 65 71 33 43 62 73 74 syl322anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ¬ ( 𝑅𝐺 ) ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) )
76 nbrne1 ( ( ( 𝑅𝐺 ) ( 𝑃 ( 𝑅𝐺 ) ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ) → ( 𝑃 ( 𝑅𝐺 ) ) ≠ ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) )
77 64 75 76 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑃 ( 𝑅𝐺 ) ) ≠ ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) )
78 3 4 36 5 2atmat0 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ∧ ( 𝑅𝐺 ) ∈ 𝐴 ) ∧ ( 𝑄𝐴 ∧ ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ∈ 𝐴 ∧ ( 𝑃 ( 𝑅𝐺 ) ) ≠ ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ) ) → ( ( ( 𝑃 ( 𝑅𝐺 ) ) ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ) ∈ 𝐴 ∨ ( ( 𝑃 ( 𝑅𝐺 ) ) ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ) = ( 0. ‘ 𝐾 ) ) )
79 18 11 62 12 33 77 78 syl33anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( ( ( 𝑃 ( 𝑅𝐺 ) ) ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ) ∈ 𝐴 ∨ ( ( 𝑃 ( 𝑅𝐺 ) ) ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ) = ( 0. ‘ 𝐾 ) ) )
80 9 eleq1i ( 𝑆𝐴 ↔ ( ( 𝑃 ( 𝑅𝐺 ) ) ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ) ∈ 𝐴 )
81 9 eqeq1i ( 𝑆 = ( 0. ‘ 𝐾 ) ↔ ( ( 𝑃 ( 𝑅𝐺 ) ) ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ) = ( 0. ‘ 𝐾 ) )
82 80 81 orbi12i ( ( 𝑆𝐴𝑆 = ( 0. ‘ 𝐾 ) ) ↔ ( ( ( 𝑃 ( 𝑅𝐺 ) ) ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ) ∈ 𝐴 ∨ ( ( 𝑃 ( 𝑅𝐺 ) ) ( 𝑄 ( 𝑅 ‘ ( 𝐺 𝐹 ) ) ) ) = ( 0. ‘ 𝐾 ) ) )
83 79 82 sylibr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑆𝐴𝑆 = ( 0. ‘ 𝐾 ) ) )
84 83 ord ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( ¬ 𝑆𝐴𝑆 = ( 0. ‘ 𝐾 ) ) )
85 84 necon1ad ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑆 ≠ ( 0. ‘ 𝐾 ) → 𝑆𝐴 ) )
86 59 85 mpd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝑆𝐴 )
87 simp21 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
88 87 65 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) )
89 1 2 3 4 5 6 7 8 9 36 cdlemh2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑆 𝑊 ) = ( 0. ‘ 𝐾 ) )
90 88 89 syld3an2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑆 𝑊 ) = ( 0. ‘ 𝐾 ) )
91 2 4 36 5 6 lhpmatb ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐴 ) → ( ¬ 𝑆 𝑊 ↔ ( 𝑆 𝑊 ) = ( 0. ‘ 𝐾 ) ) )
92 18 21 86 91 syl21anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( ¬ 𝑆 𝑊 ↔ ( 𝑆 𝑊 ) = ( 0. ‘ 𝐾 ) ) )
93 90 92 mpbird ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ¬ 𝑆 𝑊 )
94 86 93 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 ( 𝑃 ( 𝑅𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) )