Metamath Proof Explorer


Theorem cdleme21a

Description: Part of proof of Lemma E in Crawley p. 115. (Contributed by NM, 28-Nov-2012)

Ref Expression
Hypotheses cdleme21a.l = ( le ‘ 𝐾 )
cdleme21a.j = ( join ‘ 𝐾 )
cdleme21a.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cdleme21a ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) → 𝑆𝑧 )

Proof

Step Hyp Ref Expression
1 cdleme21a.l = ( le ‘ 𝐾 )
2 cdleme21a.j = ( join ‘ 𝐾 )
3 cdleme21a.a 𝐴 = ( Atoms ‘ 𝐾 )
4 simp11 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) → 𝐾 ∈ HL )
5 hlcvl ( 𝐾 ∈ HL → 𝐾 ∈ CvLat )
6 4 5 syl ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) → 𝐾 ∈ CvLat )
7 simp12 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) → 𝑃𝐴 )
8 simp2l ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) → 𝑆𝐴 )
9 simp3l ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) → 𝑧𝐴 )
10 simp13 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) → 𝑄𝐴 )
11 simp2r ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) → ¬ 𝑆 ( 𝑃 𝑄 ) )
12 1 2 3 atnlej1 ( ( 𝐾 ∈ HL ∧ ( 𝑆𝐴𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → 𝑆𝑃 )
13 12 necomd ( ( 𝐾 ∈ HL ∧ ( 𝑆𝐴𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → 𝑃𝑆 )
14 4 8 7 10 11 13 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) → 𝑃𝑆 )
15 simp3r ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) → ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) )
16 3 2 cvlsupr6 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑆𝐴𝑧𝐴 ) ∧ ( 𝑃𝑆 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) → 𝑧𝑆 )
17 16 necomd ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑆𝐴𝑧𝐴 ) ∧ ( 𝑃𝑆 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) → 𝑆𝑧 )
18 6 7 8 9 14 15 17 syl132anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) → 𝑆𝑧 )