Metamath Proof Explorer


Theorem cdleme11h

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme11 . (Contributed by NM, 14-Jun-2012)

Ref Expression
Hypotheses cdleme11.l = ( le ‘ 𝐾 )
cdleme11.j = ( join ‘ 𝐾 )
cdleme11.m = ( meet ‘ 𝐾 )
cdleme11.a 𝐴 = ( Atoms ‘ 𝐾 )
cdleme11.h 𝐻 = ( LHyp ‘ 𝐾 )
cdleme11.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
cdleme11.c 𝐶 = ( ( 𝑃 𝑆 ) 𝑊 )
cdleme11.d 𝐷 = ( ( 𝑃 𝑇 ) 𝑊 )
cdleme11.f 𝐹 = ( ( 𝑆 𝑈 ) ( 𝑄 ( ( 𝑃 𝑆 ) 𝑊 ) ) )
Assertion cdleme11h ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐹𝑄 )

Proof

Step Hyp Ref Expression
1 cdleme11.l = ( le ‘ 𝐾 )
2 cdleme11.j = ( join ‘ 𝐾 )
3 cdleme11.m = ( meet ‘ 𝐾 )
4 cdleme11.a 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme11.h 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme11.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
7 cdleme11.c 𝐶 = ( ( 𝑃 𝑆 ) 𝑊 )
8 cdleme11.d 𝐷 = ( ( 𝑃 𝑇 ) 𝑊 )
9 cdleme11.f 𝐹 = ( ( 𝑆 𝑈 ) ( 𝑄 ( ( 𝑃 𝑆 ) 𝑊 ) ) )
10 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
11 simp21l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑃𝐴 )
12 simp23 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑆𝐴 )
13 simp22l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑄𝐴 )
14 simp22r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ¬ 𝑄 𝑊 )
15 1 2 3 4 5 7 cdleme0c ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑆𝐴 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) → 𝐶𝑄 )
16 10 11 12 13 14 15 syl122anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐶𝑄 )
17 16 necomd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑄𝐶 )
18 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ HL )
19 simp21 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
20 simp3r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ¬ 𝑆 ( 𝑃 𝑄 ) )
21 1 2 3 4 cdleme00a ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑆𝐴 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → 𝑆𝑃 )
22 18 11 13 12 20 21 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑆𝑃 )
23 22 necomd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑃𝑆 )
24 1 2 3 4 5 7 cdleme9a ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑆𝐴𝑃𝑆 ) ) → 𝐶𝐴 )
25 10 19 12 23 24 syl112anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐶𝐴 )
26 2 4 lnnat ( ( 𝐾 ∈ HL ∧ 𝑄𝐴𝐶𝐴 ) → ( 𝑄𝐶 ↔ ¬ ( 𝑄 𝐶 ) ∈ 𝐴 ) )
27 18 13 25 26 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑄𝐶 ↔ ¬ ( 𝑄 𝐶 ) ∈ 𝐴 ) )
28 17 27 mpbid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ¬ ( 𝑄 𝐶 ) ∈ 𝐴 )
29 2 4 hlatjidm ( ( 𝐾 ∈ HL ∧ 𝑄𝐴 ) → ( 𝑄 𝑄 ) = 𝑄 )
30 18 13 29 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑄 𝑄 ) = 𝑄 )
31 30 13 eqeltrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑄 𝑄 ) ∈ 𝐴 )
32 oveq2 ( 𝐹 = 𝑄 → ( 𝑄 𝐹 ) = ( 𝑄 𝑄 ) )
33 32 eleq1d ( 𝐹 = 𝑄 → ( ( 𝑄 𝐹 ) ∈ 𝐴 ↔ ( 𝑄 𝑄 ) ∈ 𝐴 ) )
34 31 33 syl5ibrcom ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝐹 = 𝑄 → ( 𝑄 𝐹 ) ∈ 𝐴 ) )
35 simp22 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) )
36 simp3l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑃𝑄 )
37 1 2 3 4 5 6 7 6 9 cdleme11g ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ 𝑃𝑄 ) → ( 𝑄 𝐹 ) = ( 𝑄 𝐶 ) )
38 10 11 35 12 36 37 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑄 𝐹 ) = ( 𝑄 𝐶 ) )
39 38 eleq1d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( ( 𝑄 𝐹 ) ∈ 𝐴 ↔ ( 𝑄 𝐶 ) ∈ 𝐴 ) )
40 34 39 sylibd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝐹 = 𝑄 → ( 𝑄 𝐶 ) ∈ 𝐴 ) )
41 40 necon3bd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( ¬ ( 𝑄 𝐶 ) ∈ 𝐴𝐹𝑄 ) )
42 28 41 mpd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐹𝑄 )