Metamath Proof Explorer


Theorem cdlemg12f

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 ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemg12f ( ( ( ( 𝐾 ∈ 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 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ HL )
9 8 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ Lat )
10 simp12l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → 𝑃𝐴 )
11 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
12 simp21 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → 𝐹𝑇 )
13 simp22 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → 𝐺𝑇 )
14 1 4 5 6 ltrncoat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑃𝐴 ) → ( 𝐹 ‘ ( 𝐺𝑃 ) ) ∈ 𝐴 )
15 11 12 13 10 14 syl121anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → ( 𝐹 ‘ ( 𝐺𝑃 ) ) ∈ 𝐴 )
16 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17 16 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ∧ ( 𝐹 ‘ ( 𝐺𝑃 ) ) ∈ 𝐴 ) → ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) )
18 8 10 15 17 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) )
19 simp13l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → 𝑄𝐴 )
20 1 4 5 6 ltrncoat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑄𝐴 ) → ( 𝐹 ‘ ( 𝐺𝑄 ) ) ∈ 𝐴 )
21 11 12 13 19 20 syl121anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → ( 𝐹 ‘ ( 𝐺𝑄 ) ) ∈ 𝐴 )
22 16 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑄𝐴 ∧ ( 𝐹 ‘ ( 𝐺𝑄 ) ) ∈ 𝐴 ) → ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ∈ ( Base ‘ 𝐾 ) )
23 8 19 21 22 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ∈ ( Base ‘ 𝐾 ) )
24 16 1 3 latmle1 ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) )
25 9 18 23 24 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) )
26 simp1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) )
27 simp2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) )
28 simp33 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) )
29 simp31l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) )
30 simp31r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) )
31 1 2 3 4 5 6 7 cdlemg10 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) 𝑊 )
32 26 27 28 29 30 31 syl113anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) 𝑊 )
33 16 3 latmcl ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) ∈ ( Base ‘ 𝐾 ) )
34 9 18 23 33 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) ∈ ( Base ‘ 𝐾 ) )
35 simp11r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → 𝑊𝐻 )
36 16 5 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
37 35 36 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
38 16 1 3 latlem12 ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ∧ ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) 𝑊 ) ↔ ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) 𝑊 ) ) )
39 9 34 18 37 38 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → ( ( ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ∧ ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) 𝑊 ) ↔ ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) 𝑊 ) ) )
40 25 32 39 mpbi2and ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ∧ ( 𝑅𝐹 ) ≠ ( 𝑅𝐺 ) ∧ ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) 𝑊 ) )