Metamath Proof Explorer


Theorem cdleme7aa

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 𝐺 = ( ( 𝑃 𝑄 ) ( 𝐹 ( ( 𝑅 𝑆 ) 𝑊 ) ) )
Assertion cdleme7aa ( ( ( ( 𝐾 ∈ 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 simp33 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ¬ 𝑆 ( 𝑃 𝑄 ) )
10 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ HL )
11 simp2ll ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑅𝐴 )
12 simp2rl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑆𝐴 )
13 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
14 simp12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
15 simp13 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑄𝐴 )
16 simp31 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑃𝑄 )
17 1 2 3 4 5 6 lhpat2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑃𝑄 ) ) → 𝑈𝐴 )
18 13 14 15 16 17 syl112anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑈𝐴 )
19 10 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ Lat )
20 simp12l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑃𝐴 )
21 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
22 21 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
23 10 20 15 22 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
24 simp11r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑊𝐻 )
25 21 5 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
26 24 25 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
27 21 1 3 latmle2 ( ( 𝐾 ∈ Lat ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 𝑄 ) 𝑊 ) 𝑊 )
28 19 23 26 27 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 𝑄 ) 𝑊 ) 𝑊 )
29 6 28 eqbrtrid ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑈 𝑊 )
30 simp2lr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ¬ 𝑅 𝑊 )
31 nbrne2 ( ( 𝑈 𝑊 ∧ ¬ 𝑅 𝑊 ) → 𝑈𝑅 )
32 31 necomd ( ( 𝑈 𝑊 ∧ ¬ 𝑅 𝑊 ) → 𝑅𝑈 )
33 29 30 32 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑅𝑈 )
34 1 2 4 hlatexch1 ( ( 𝐾 ∈ HL ∧ ( 𝑅𝐴𝑆𝐴𝑈𝐴 ) ∧ 𝑅𝑈 ) → ( 𝑅 ( 𝑈 𝑆 ) → 𝑆 ( 𝑈 𝑅 ) ) )
35 10 11 12 18 33 34 syl131anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑅 ( 𝑈 𝑆 ) → 𝑆 ( 𝑈 𝑅 ) ) )
36 simp2l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) )
37 simp32 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑅 ( 𝑃 𝑄 ) )
38 1 2 3 4 5 6 cdleme4 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝑃 𝑄 ) = ( 𝑅 𝑈 ) )
39 13 20 15 36 37 38 syl131anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑃 𝑄 ) = ( 𝑅 𝑈 ) )
40 2 4 hlatjcom ( ( 𝐾 ∈ HL ∧ 𝑅𝐴𝑈𝐴 ) → ( 𝑅 𝑈 ) = ( 𝑈 𝑅 ) )
41 10 11 18 40 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑅 𝑈 ) = ( 𝑈 𝑅 ) )
42 39 41 eqtrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑃 𝑄 ) = ( 𝑈 𝑅 ) )
43 42 breq2d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑆 ( 𝑃 𝑄 ) ↔ 𝑆 ( 𝑈 𝑅 ) ) )
44 35 43 sylibrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑅 ( 𝑈 𝑆 ) → 𝑆 ( 𝑃 𝑄 ) ) )
45 9 44 mtod ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ¬ 𝑅 ( 𝑈 𝑆 ) )