Metamath Proof Explorer


Theorem cdlemd2

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 29-May-2012)

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

Proof

Step Hyp Ref Expression
1 cdlemd2.l = ( le ‘ 𝐾 )
2 cdlemd2.j = ( join ‘ 𝐾 )
3 cdlemd2.a 𝐴 = ( Atoms ‘ 𝐾 )
4 cdlemd2.h 𝐻 = ( LHyp ‘ 𝐾 )
5 cdlemd2.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6 simp3l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐹𝑃 ) = ( 𝐺𝑃 ) )
7 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
8 simp12l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → 𝐹𝑇 )
9 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → 𝐾 ∈ HL )
10 9 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → 𝐾 ∈ Lat )
11 simp21l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → 𝑃𝐴 )
12 simp13 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → 𝑅𝐴 )
13 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14 13 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑅𝐴 ) → ( 𝑃 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
15 9 11 12 14 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝑃 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
16 simp11r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → 𝑊𝐻 )
17 13 4 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
18 16 17 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
19 eqid ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
20 13 19 latmcl ( ( 𝐾 ∈ Lat ∧ ( 𝑃 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
21 10 15 18 20 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
22 13 1 19 latmle2 ( ( 𝐾 ∈ Lat ∧ ( 𝑃 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) 𝑊 )
23 10 15 18 22 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) 𝑊 )
24 13 1 4 5 ltrnval1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) 𝑊 ) ) → ( 𝐹 ‘ ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) )
25 7 8 21 23 24 syl112anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐹 ‘ ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) )
26 simp12r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → 𝐺𝑇 )
27 13 1 4 5 ltrnval1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 ∧ ( ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) 𝑊 ) ) → ( 𝐺 ‘ ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) )
28 7 26 21 23 27 syl112anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐺 ‘ ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) )
29 25 28 eqtr4d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐹 ‘ ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( 𝐺 ‘ ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) )
30 6 29 oveq12d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( ( 𝐹𝑃 ) ( 𝐹 ‘ ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐺𝑃 ) ( 𝐺 ‘ ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
31 13 3 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
32 11 31 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
33 13 2 4 5 ltrnj ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐹 ‘ ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐹𝑃 ) ( 𝐹 ‘ ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
34 7 8 32 21 33 syl112anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐹 ‘ ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐹𝑃 ) ( 𝐹 ‘ ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
35 13 2 4 5 ltrnj ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐺 ‘ ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐺𝑃 ) ( 𝐺 ‘ ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
36 7 26 32 21 35 syl112anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐺 ‘ ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐺𝑃 ) ( 𝐺 ‘ ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
37 30 34 36 3eqtr4d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐹 ‘ ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( 𝐺 ‘ ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
38 simp3r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐹𝑄 ) = ( 𝐺𝑄 ) )
39 simp22l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → 𝑄𝐴 )
40 13 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴 ) → ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
41 9 39 12 40 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
42 13 19 latmcl ( ( 𝐾 ∈ Lat ∧ ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
43 10 41 18 42 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
44 13 1 19 latmle2 ( ( 𝐾 ∈ Lat ∧ ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) 𝑊 )
45 10 41 18 44 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) 𝑊 )
46 13 1 4 5 ltrnval1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) 𝑊 ) ) → ( 𝐹 ‘ ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) )
47 7 8 43 45 46 syl112anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐹 ‘ ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) )
48 13 1 4 5 ltrnval1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 ∧ ( ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) 𝑊 ) ) → ( 𝐺 ‘ ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) )
49 7 26 43 45 48 syl112anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐺 ‘ ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) )
50 47 49 eqtr4d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐹 ‘ ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( 𝐺 ‘ ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) )
51 38 50 oveq12d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( ( 𝐹𝑄 ) ( 𝐹 ‘ ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐺𝑄 ) ( 𝐺 ‘ ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
52 13 3 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
53 39 52 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
54 13 2 4 5 ltrnj ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐹 ‘ ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐹𝑄 ) ( 𝐹 ‘ ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
55 7 8 53 43 54 syl112anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐹 ‘ ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐹𝑄 ) ( 𝐹 ‘ ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
56 13 2 4 5 ltrnj ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐺 ‘ ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐺𝑄 ) ( 𝐺 ‘ ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
57 7 26 53 43 56 syl112anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐺 ‘ ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐺𝑄 ) ( 𝐺 ‘ ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
58 51 55 57 3eqtr4d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐹 ‘ ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( 𝐺 ‘ ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
59 37 58 oveq12d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( ( 𝐹 ‘ ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ( meet ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) = ( ( 𝐺 ‘ ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ( meet ‘ 𝐾 ) ( 𝐺 ‘ ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
60 13 2 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
61 10 32 21 60 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
62 13 2 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
63 10 53 43 62 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
64 13 19 4 5 ltrnm ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐹 ‘ ( ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) = ( ( 𝐹 ‘ ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ( meet ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
65 7 8 61 63 64 syl112anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐹 ‘ ( ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) = ( ( 𝐹 ‘ ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ( meet ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
66 13 19 4 5 ltrnm ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 ∧ ( ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐺 ‘ ( ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) = ( ( 𝐺 ‘ ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ( meet ‘ 𝐾 ) ( 𝐺 ‘ ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
67 7 26 61 63 66 syl112anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐺 ‘ ( ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) = ( ( 𝐺 ‘ ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ( meet ‘ 𝐾 ) ( 𝐺 ‘ ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
68 59 65 67 3eqtr4d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐹 ‘ ( ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) = ( 𝐺 ‘ ( ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
69 simp21 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
70 simp22 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) )
71 simp23l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → 𝑃𝑄 )
72 simp23r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ¬ 𝑅 ( 𝑃 𝑄 ) )
73 12 71 72 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) )
74 1 2 19 3 4 cdlemd1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → 𝑅 = ( ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
75 7 69 70 73 74 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → 𝑅 = ( ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
76 75 fveq2d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐹𝑅 ) = ( 𝐹 ‘ ( ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
77 75 fveq2d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐺𝑅 ) = ( 𝐺 ‘ ( ( 𝑃 ( ( 𝑃 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ( ( 𝑄 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
78 68 76 77 3eqtr4d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐹𝑅 ) = ( 𝐺𝑅 ) )