Metamath Proof Explorer


Theorem cdlemg10

Description: TODO: FIX COMMENT. (Contributed by NM, 4-May-2013)

Ref Expression
Hypotheses cdlemg8.l = ( le ‘ 𝐾 )
cdlemg8.j = ( join ‘ 𝐾 )
cdlemg8.m = ( meet ‘ 𝐾 )
cdlemg8.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemg8.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemg8.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemg10.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemg10 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) 𝑊 )

Proof

Step Hyp Ref Expression
1 cdlemg8.l = ( le ‘ 𝐾 )
2 cdlemg8.j = ( join ‘ 𝐾 )
3 cdlemg8.m = ( meet ‘ 𝐾 )
4 cdlemg8.a 𝐴 = ( Atoms ‘ 𝐾 )
5 cdlemg8.h 𝐻 = ( LHyp ‘ 𝐾 )
6 cdlemg8.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7 cdlemg10.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ HL )
10 9 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ Lat )
11 simp12l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → 𝑃𝐴 )
12 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
13 simp21 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → 𝐹𝑇 )
14 simp22 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → 𝐺𝑇 )
15 1 4 5 6 ltrnat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇𝑃𝐴 ) → ( 𝐺𝑃 ) ∈ 𝐴 )
16 12 14 11 15 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( 𝐺𝑃 ) ∈ 𝐴 )
17 1 4 5 6 ltrnat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝐺𝑃 ) ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝐺𝑃 ) ) ∈ 𝐴 )
18 12 13 16 17 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( 𝐹 ‘ ( 𝐺𝑃 ) ) ∈ 𝐴 )
19 8 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ∧ ( 𝐹 ‘ ( 𝐺𝑃 ) ) ∈ 𝐴 ) → ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) )
20 9 11 18 19 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) )
21 simp13l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → 𝑄𝐴 )
22 1 4 5 6 ltrnat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇𝑄𝐴 ) → ( 𝐺𝑄 ) ∈ 𝐴 )
23 12 14 21 22 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( 𝐺𝑄 ) ∈ 𝐴 )
24 1 4 5 6 ltrnat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝐺𝑄 ) ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝐺𝑄 ) ) ∈ 𝐴 )
25 12 13 23 24 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( 𝐹 ‘ ( 𝐺𝑄 ) ) ∈ 𝐴 )
26 8 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑄𝐴 ∧ ( 𝐹 ‘ ( 𝐺𝑄 ) ) ∈ 𝐴 ) → ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ∈ ( Base ‘ 𝐾 ) )
27 9 21 25 26 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ∈ ( Base ‘ 𝐾 ) )
28 8 3 latmcl ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) ∈ ( Base ‘ 𝐾 ) )
29 10 20 27 28 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) ∈ ( Base ‘ 𝐾 ) )
30 8 5 6 7 trlcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝑅𝐹 ) ∈ ( Base ‘ 𝐾 ) )
31 12 13 30 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( 𝑅𝐹 ) ∈ ( Base ‘ 𝐾 ) )
32 8 5 6 7 trlcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 ) → ( 𝑅𝐺 ) ∈ ( Base ‘ 𝐾 ) )
33 12 14 32 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( 𝑅𝐺 ) ∈ ( Base ‘ 𝐾 ) )
34 8 2 latjcl ( ( 𝐾 ∈ Lat ∧ ( 𝑅𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅𝐺 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅𝐹 ) ( 𝑅𝐺 ) ) ∈ ( Base ‘ 𝐾 ) )
35 10 31 33 34 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( ( 𝑅𝐹 ) ( 𝑅𝐺 ) ) ∈ ( Base ‘ 𝐾 ) )
36 simp11r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → 𝑊𝐻 )
37 8 5 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
38 36 37 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
39 1 2 3 4 5 6 7 cdlemg10a ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) ( ( 𝑅𝐹 ) ( 𝑅𝐺 ) ) )
40 1 5 6 7 trlle ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝑅𝐹 ) 𝑊 )
41 12 13 40 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( 𝑅𝐹 ) 𝑊 )
42 1 5 6 7 trlle ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 ) → ( 𝑅𝐺 ) 𝑊 )
43 12 14 42 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( 𝑅𝐺 ) 𝑊 )
44 8 1 2 latjle12 ( ( 𝐾 ∈ Lat ∧ ( ( 𝑅𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅𝐺 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑅𝐹 ) 𝑊 ∧ ( 𝑅𝐺 ) 𝑊 ) ↔ ( ( 𝑅𝐹 ) ( 𝑅𝐺 ) ) 𝑊 ) )
45 10 31 33 38 44 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( ( ( 𝑅𝐹 ) 𝑊 ∧ ( 𝑅𝐺 ) 𝑊 ) ↔ ( ( 𝑅𝐹 ) ( 𝑅𝐺 ) ) 𝑊 ) )
46 41 43 45 mpbi2and ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( ( 𝑅𝐹 ) ( 𝑅𝐺 ) ) 𝑊 )
47 8 1 10 29 35 38 39 46 lattrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑇𝐺𝑇𝑃𝑄 ) ∧ ( ( ( 𝐹 ‘ ( 𝐺𝑃 ) ) ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ≠ ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐹 ) ( 𝑃 𝑄 ) ∧ ¬ ( 𝑅𝐺 ) ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 ( 𝐹 ‘ ( 𝐺𝑃 ) ) ) ( 𝑄 ( 𝐹 ‘ ( 𝐺𝑄 ) ) ) ) 𝑊 )