Metamath Proof Explorer


Theorem cdleme7c

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

Ref Expression
Hypotheses cdleme4.l = ( le ‘ 𝐾 )
cdleme4.j = ( join ‘ 𝐾 )
cdleme4.m = ( meet ‘ 𝐾 )
cdleme4.a 𝐴 = ( Atoms ‘ 𝐾 )
cdleme4.h 𝐻 = ( LHyp ‘ 𝐾 )
cdleme4.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
cdleme4.f 𝐹 = ( ( 𝑆 𝑈 ) ( 𝑄 ( ( 𝑃 𝑆 ) 𝑊 ) ) )
cdleme4.g 𝐺 = ( ( 𝑃 𝑄 ) ( 𝐹 ( ( 𝑅 𝑆 ) 𝑊 ) ) )
cdleme7.v 𝑉 = ( ( 𝑅 𝑆 ) 𝑊 )
Assertion cdleme7c ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑈𝑉 )

Proof

Step Hyp Ref Expression
1 cdleme4.l = ( le ‘ 𝐾 )
2 cdleme4.j = ( join ‘ 𝐾 )
3 cdleme4.m = ( meet ‘ 𝐾 )
4 cdleme4.a 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme4.h 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme4.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
7 cdleme4.f 𝐹 = ( ( 𝑆 𝑈 ) ( 𝑄 ( ( 𝑃 𝑆 ) 𝑊 ) ) )
8 cdleme4.g 𝐺 = ( ( 𝑃 𝑄 ) ( 𝐹 ( ( 𝑅 𝑆 ) 𝑊 ) ) )
9 cdleme7.v 𝑉 = ( ( 𝑅 𝑆 ) 𝑊 )
10 6 9 oveq12i ( 𝑈 𝑉 ) = ( ( ( 𝑃 𝑄 ) 𝑊 ) ( ( 𝑅 𝑆 ) 𝑊 ) )
11 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
12 simp12l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑃𝐴 )
13 simp13 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑄𝐴 )
14 simp2l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) )
15 simp32 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑅 ( 𝑃 𝑄 ) )
16 1 2 3 4 5 6 cdleme4 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝑃 𝑄 ) = ( 𝑅 𝑈 ) )
17 11 12 13 14 15 16 syl131anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑃 𝑄 ) = ( 𝑅 𝑈 ) )
18 17 oveq1d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) = ( ( 𝑅 𝑈 ) ( 𝑅 𝑆 ) ) )
19 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ HL )
20 simp12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
21 simp31 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑃𝑄 )
22 1 2 3 4 5 6 lhpat2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑃𝑄 ) ) → 𝑈𝐴 )
23 11 20 13 21 22 syl112anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑈𝐴 )
24 simp2rl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑆𝐴 )
25 simp2ll ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑅𝐴 )
26 19 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ Lat )
27 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
28 27 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
29 19 12 13 28 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
30 simp11r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑊𝐻 )
31 27 5 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
32 30 31 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
33 27 1 3 latmle2 ( ( 𝐾 ∈ Lat ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 𝑄 ) 𝑊 ) 𝑊 )
34 26 29 32 33 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 𝑄 ) 𝑊 ) 𝑊 )
35 6 34 eqbrtrid ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑈 𝑊 )
36 simp2rr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ¬ 𝑆 𝑊 )
37 nbrne2 ( ( 𝑈 𝑊 ∧ ¬ 𝑆 𝑊 ) → 𝑈𝑆 )
38 35 36 37 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑈𝑆 )
39 1 2 3 4 5 6 7 8 cdleme7aa ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ¬ 𝑅 ( 𝑈 𝑆 ) )
40 1 2 3 4 2llnma2 ( ( 𝐾 ∈ HL ∧ ( 𝑈𝐴𝑆𝐴𝑅𝐴 ) ∧ ( 𝑈𝑆 ∧ ¬ 𝑅 ( 𝑈 𝑆 ) ) ) → ( ( 𝑅 𝑈 ) ( 𝑅 𝑆 ) ) = 𝑅 )
41 19 23 24 25 38 39 40 syl132anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( ( 𝑅 𝑈 ) ( 𝑅 𝑆 ) ) = 𝑅 )
42 18 41 eqtrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) = 𝑅 )
43 42 oveq1d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) 𝑊 ) = ( 𝑅 𝑊 ) )
44 hlol ( 𝐾 ∈ HL → 𝐾 ∈ OL )
45 19 44 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ OL )
46 27 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴 ) → ( 𝑅 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
47 19 25 24 46 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑅 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
48 27 3 latmmdir ( ( 𝐾 ∈ OL ∧ ( ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) 𝑊 ) = ( ( ( 𝑃 𝑄 ) 𝑊 ) ( ( 𝑅 𝑆 ) 𝑊 ) ) )
49 45 29 47 32 48 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) 𝑊 ) = ( ( ( 𝑃 𝑄 ) 𝑊 ) ( ( 𝑅 𝑆 ) 𝑊 ) ) )
50 eqid ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
51 1 3 50 4 5 lhpmat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) → ( 𝑅 𝑊 ) = ( 0. ‘ 𝐾 ) )
52 11 14 51 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑅 𝑊 ) = ( 0. ‘ 𝐾 ) )
53 43 49 52 3eqtr3d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( ( ( 𝑃 𝑄 ) 𝑊 ) ( ( 𝑅 𝑆 ) 𝑊 ) ) = ( 0. ‘ 𝐾 ) )
54 10 53 syl5eq ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑈 𝑉 ) = ( 0. ‘ 𝐾 ) )
55 hlatl ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
56 19 55 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ AtLat )
57 simp33 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ¬ 𝑆 ( 𝑃 𝑄 ) )
58 1 2 3 4 5 6 7 8 9 cdleme7b ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑉𝐴 )
59 11 14 24 57 15 58 syl113anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑉𝐴 )
60 3 50 4 atnem0 ( ( 𝐾 ∈ AtLat ∧ 𝑈𝐴𝑉𝐴 ) → ( 𝑈𝑉 ↔ ( 𝑈 𝑉 ) = ( 0. ‘ 𝐾 ) ) )
61 56 23 59 60 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑈𝑉 ↔ ( 𝑈 𝑉 ) = ( 0. ‘ 𝐾 ) ) )
62 54 61 mpbird ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑈𝑉 )