Metamath Proof Explorer


Theorem cdleme3g

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme3fa and cdleme3 . (Contributed by NM, 7-Jun-2012)

Ref Expression
Hypotheses cdleme1.l = ( le ‘ 𝐾 )
cdleme1.j = ( join ‘ 𝐾 )
cdleme1.m = ( meet ‘ 𝐾 )
cdleme1.a 𝐴 = ( Atoms ‘ 𝐾 )
cdleme1.h 𝐻 = ( LHyp ‘ 𝐾 )
cdleme1.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
cdleme1.f 𝐹 = ( ( 𝑅 𝑈 ) ( 𝑄 ( ( 𝑃 𝑅 ) 𝑊 ) ) )
cdleme3.3 𝑉 = ( ( 𝑃 𝑅 ) 𝑊 )
Assertion cdleme3g ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝐹𝑈 )

Proof

Step Hyp Ref Expression
1 cdleme1.l = ( le ‘ 𝐾 )
2 cdleme1.j = ( join ‘ 𝐾 )
3 cdleme1.m = ( meet ‘ 𝐾 )
4 cdleme1.a 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme1.h 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme1.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
7 cdleme1.f 𝐹 = ( ( 𝑅 𝑈 ) ( 𝑄 ( ( 𝑃 𝑅 ) 𝑊 ) ) )
8 cdleme3.3 𝑉 = ( ( 𝑃 𝑅 ) 𝑊 )
9 1 2 3 4 5 6 7 8 cdleme3d 𝐹 = ( ( 𝑅 𝑈 ) ( 𝑄 𝑉 ) )
10 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ HL )
11 10 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ Lat )
12 simp23l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑅𝐴 )
13 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
14 simp21 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
15 simp22l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑄𝐴 )
16 simp3l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑃𝑄 )
17 1 2 3 4 5 6 lhpat2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑃𝑄 ) ) → 𝑈𝐴 )
18 13 14 15 16 17 syl112anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑈𝐴 )
19 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
20 19 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑅𝐴𝑈𝐴 ) → ( 𝑅 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
21 10 12 18 20 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑅 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
22 simp3r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ¬ 𝑅 ( 𝑃 𝑄 ) )
23 12 22 jca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑅𝐴 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) )
24 1 2 3 4 5 6 7 8 cdleme3e ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → 𝑉𝐴 )
25 13 14 15 23 24 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑉𝐴 )
26 19 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑄𝐴𝑉𝐴 ) → ( 𝑄 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
27 10 15 25 26 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑄 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
28 19 1 3 latmle2 ( ( 𝐾 ∈ Lat ∧ ( 𝑅 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 𝑉 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 𝑈 ) ( 𝑄 𝑉 ) ) ( 𝑄 𝑉 ) )
29 11 21 27 28 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( 𝑅 𝑈 ) ( 𝑄 𝑉 ) ) ( 𝑄 𝑉 ) )
30 9 29 eqbrtrid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝐹 ( 𝑄 𝑉 ) )
31 simp22r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ¬ 𝑄 𝑊 )
32 simp23 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) )
33 simp3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) )
34 1 2 3 4 5 6 8 cdleme0e ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑈𝑉 )
35 13 14 15 32 33 34 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑈𝑉 )
36 1 2 4 hlatexch2 ( ( 𝐾 ∈ HL ∧ ( 𝑈𝐴𝑄𝐴𝑉𝐴 ) ∧ 𝑈𝑉 ) → ( 𝑈 ( 𝑄 𝑉 ) → 𝑄 ( 𝑈 𝑉 ) ) )
37 10 18 15 25 35 36 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑈 ( 𝑄 𝑉 ) → 𝑄 ( 𝑈 𝑉 ) ) )
38 simp21l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑃𝐴 )
39 19 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
40 10 38 15 39 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
41 simp1r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑊𝐻 )
42 19 5 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
43 41 42 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
44 19 1 3 latmle2 ( ( 𝐾 ∈ Lat ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 𝑄 ) 𝑊 ) 𝑊 )
45 11 40 43 44 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 𝑄 ) 𝑊 ) 𝑊 )
46 6 45 eqbrtrid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑈 𝑊 )
47 19 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑅𝐴 ) → ( 𝑃 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
48 10 38 12 47 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑃 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
49 19 1 3 latmle2 ( ( 𝐾 ∈ Lat ∧ ( 𝑃 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 𝑅 ) 𝑊 ) 𝑊 )
50 11 48 43 49 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 𝑅 ) 𝑊 ) 𝑊 )
51 8 50 eqbrtrid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑉 𝑊 )
52 19 4 atbase ( 𝑈𝐴𝑈 ∈ ( Base ‘ 𝐾 ) )
53 18 52 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑈 ∈ ( Base ‘ 𝐾 ) )
54 19 4 atbase ( 𝑉𝐴𝑉 ∈ ( Base ‘ 𝐾 ) )
55 25 54 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑉 ∈ ( Base ‘ 𝐾 ) )
56 19 1 2 latjle12 ( ( 𝐾 ∈ Lat ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑉 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑈 𝑊𝑉 𝑊 ) ↔ ( 𝑈 𝑉 ) 𝑊 ) )
57 11 53 55 43 56 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( 𝑈 𝑊𝑉 𝑊 ) ↔ ( 𝑈 𝑉 ) 𝑊 ) )
58 46 51 57 mpbi2and ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑈 𝑉 ) 𝑊 )
59 19 4 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
60 15 59 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
61 19 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑈𝐴𝑉𝐴 ) → ( 𝑈 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
62 10 18 25 61 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑈 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
63 19 1 lattr ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑈 𝑉 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑄 ( 𝑈 𝑉 ) ∧ ( 𝑈 𝑉 ) 𝑊 ) → 𝑄 𝑊 ) )
64 11 60 62 43 63 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( 𝑄 ( 𝑈 𝑉 ) ∧ ( 𝑈 𝑉 ) 𝑊 ) → 𝑄 𝑊 ) )
65 58 64 mpan2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑄 ( 𝑈 𝑉 ) → 𝑄 𝑊 ) )
66 37 65 syld ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑈 ( 𝑄 𝑉 ) → 𝑄 𝑊 ) )
67 31 66 mtod ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ¬ 𝑈 ( 𝑄 𝑉 ) )
68 nbrne2 ( ( 𝐹 ( 𝑄 𝑉 ) ∧ ¬ 𝑈 ( 𝑄 𝑉 ) ) → 𝐹𝑈 )
69 30 67 68 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝐹𝑈 )