Metamath Proof Explorer


Theorem cdlemg12e

Description: TODO: FIX COMMENT. (Contributed by NM, 6-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 ‘ 𝐾 ) ‘ 𝑊 )
cdlemg12e.z 0 = ( 0. ‘ 𝐾 )
Assertion cdlemg12e ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) ≠ 0 )

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 cdlemg12e.z 0 = ( 0. ‘ 𝐾 )
9 simp33 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) )
10 simpl1 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) )
11 simpl21 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → 𝐹𝑇 )
12 simpl22 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → 𝐺𝑇 )
13 simpl23 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → 𝑃𝑄 )
14 simpl31 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) )
15 simpl32 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) )
16 1 2 3 4 5 6 7 cdlemg12d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ ( 𝑃𝑄 ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( 𝑅𝐺 ) ( ( 𝑅𝐹 ) ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) ) )
17 10 11 12 13 14 15 16 syl123anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( 𝑅𝐺 ) ( ( 𝑅𝐹 ) ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) ) )
18 simpr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 )
19 18 oveq2d ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( ( 𝑅𝐹 ) ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) ) = ( ( 𝑅𝐹 ) 0 ) )
20 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝐾 ∈ HL )
21 20 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → 𝐾 ∈ HL )
22 hlol ( 𝐾 ∈ HL → 𝐾 ∈ OL )
23 21 22 syl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → 𝐾 ∈ OL )
24 simpl11 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
25 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
26 25 5 6 7 trlcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝑅𝐹 ) ∈ ( Base ‘ 𝐾 ) )
27 24 11 26 syl2anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( 𝑅𝐹 ) ∈ ( Base ‘ 𝐾 ) )
28 25 2 8 olj01 ( ( 𝐾 ∈ OL ∧ ( 𝑅𝐹 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅𝐹 ) 0 ) = ( 𝑅𝐹 ) )
29 23 27 28 syl2anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( ( 𝑅𝐹 ) 0 ) = ( 𝑅𝐹 ) )
30 19 29 eqtrd ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( ( 𝑅𝐹 ) ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) ) = ( 𝑅𝐹 ) )
31 17 30 breqtrd ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( 𝑅𝐺 ) ( 𝑅𝐹 ) )
32 hlatl ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
33 21 32 syl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → 𝐾 ∈ AtLat )
34 hlop ( 𝐾 ∈ HL → 𝐾 ∈ OP )
35 21 34 syl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → 𝐾 ∈ OP )
36 25 5 6 7 trlcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 ) → ( 𝑅𝐺 ) ∈ ( Base ‘ 𝐾 ) )
37 24 12 36 syl2anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( 𝑅𝐺 ) ∈ ( Base ‘ 𝐾 ) )
38 simp12l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝑃𝐴 )
39 38 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → 𝑃𝐴 )
40 simp13l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝑄𝐴 )
41 40 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → 𝑄𝐴 )
42 25 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
43 21 39 41 42 syl3anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
44 25 1 8 opnlen0 ( ( ( 𝐾 ∈ OP ∧ ( 𝑅𝐺 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) → ( 𝑅𝐺 ) ≠ 0 )
45 35 37 43 15 44 syl31anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( 𝑅𝐺 ) ≠ 0 )
46 simp11r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → 𝑊𝐻 )
47 46 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → 𝑊𝐻 )
48 8 4 5 6 7 trlatn0 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 ) → ( ( 𝑅𝐺 ) ∈ 𝐴 ↔ ( 𝑅𝐺 ) ≠ 0 ) )
49 21 47 12 48 syl21anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( ( 𝑅𝐺 ) ∈ 𝐴 ↔ ( 𝑅𝐺 ) ≠ 0 ) )
50 45 49 mpbird ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( 𝑅𝐺 ) ∈ 𝐴 )
51 25 1 8 opnlen0 ( ( ( 𝐾 ∈ OP ∧ ( 𝑅𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ) → ( 𝑅𝐹 ) ≠ 0 )
52 35 27 43 14 51 syl31anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( 𝑅𝐹 ) ≠ 0 )
53 8 4 5 6 7 trlatn0 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( ( 𝑅𝐹 ) ∈ 𝐴 ↔ ( 𝑅𝐹 ) ≠ 0 ) )
54 21 47 11 53 syl21anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( ( 𝑅𝐹 ) ∈ 𝐴 ↔ ( 𝑅𝐹 ) ≠ 0 ) )
55 52 54 mpbird ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( 𝑅𝐹 ) ∈ 𝐴 )
56 1 4 atcmp ( ( 𝐾 ∈ AtLat ∧ ( 𝑅𝐺 ) ∈ 𝐴 ∧ ( 𝑅𝐹 ) ∈ 𝐴 ) → ( ( 𝑅𝐺 ) ( 𝑅𝐹 ) ↔ ( 𝑅𝐺 ) = ( 𝑅𝐹 ) ) )
57 33 50 55 56 syl3anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( ( 𝑅𝐺 ) ( 𝑅𝐹 ) ↔ ( 𝑅𝐺 ) = ( 𝑅𝐹 ) ) )
58 31 57 mpbid ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( 𝑅𝐺 ) = ( 𝑅𝐹 ) )
59 58 eqcomd ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 ) → ( 𝑅𝐹 ) = ( 𝑅𝐺 ) )
60 59 ex ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) = 0 → ( 𝑅𝐹 ) = ( 𝑅𝐺 ) ) )
61 60 necon3d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) → ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) ≠ 0 ) )
62 9 61 mpd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ) ) → ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) 𝑃 ) ( ( 𝐹 ‘ ( 𝐺𝑄 ) ) 𝑄 ) ) ≠ 0 )