Metamath Proof Explorer


Theorem cdleme11j

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 cdleme11j ( ( ( 𝐾 ∈ 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 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ HL )
11 simp22l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑄𝐴 )
12 1 2 3 4 5 6 9 cdleme3fa ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐹𝐴 )
13 1 2 4 hlatlej2 ( ( 𝐾 ∈ HL ∧ 𝑄𝐴𝐹𝐴 ) → 𝐹 ( 𝑄 𝐹 ) )
14 10 11 12 13 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐹 ( 𝑄 𝐹 ) )
15 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
16 simp21l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑃𝐴 )
17 simp22 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) )
18 simp23l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑆𝐴 )
19 simp3l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑃𝑄 )
20 1 2 3 4 5 6 7 6 9 cdleme11g ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ 𝑃𝑄 ) → ( 𝑄 𝐹 ) = ( 𝑄 𝐶 ) )
21 15 16 17 18 19 20 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑄 𝐹 ) = ( 𝑄 𝐶 ) )
22 14 21 breqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐹 ( 𝑄 𝐶 ) )
23 simp21 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
24 simp3r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ¬ 𝑆 ( 𝑃 𝑄 ) )
25 1 2 3 4 cdleme00a ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑆𝐴 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → 𝑆𝑃 )
26 10 16 11 18 24 25 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑆𝑃 )
27 26 necomd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑃𝑆 )
28 1 2 3 4 5 7 cdleme9a ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑆𝐴𝑃𝑆 ) ) → 𝐶𝐴 )
29 15 23 18 27 28 syl112anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐶𝐴 )
30 simp3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) )
31 1 2 3 4 5 6 7 6 9 cdleme11h ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐹𝑄 )
32 15 23 17 18 30 31 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐹𝑄 )
33 1 2 4 hlatexch1 ( ( 𝐾 ∈ HL ∧ ( 𝐹𝐴𝐶𝐴𝑄𝐴 ) ∧ 𝐹𝑄 ) → ( 𝐹 ( 𝑄 𝐶 ) → 𝐶 ( 𝑄 𝐹 ) ) )
34 10 12 29 11 32 33 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝐹 ( 𝑄 𝐶 ) → 𝐶 ( 𝑄 𝐹 ) ) )
35 22 34 mpd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐶 ( 𝑄 𝐹 ) )