Metamath Proof Explorer


Theorem 2atjlej

Description: Two atoms are different if their join majorizes the join of two different atoms. (Contributed by NM, 4-Jun-2013)

Ref Expression
Hypotheses ps1.l = ( le ‘ 𝐾 )
ps1.j = ( join ‘ 𝐾 )
ps1.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 2atjlej ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑃𝑄 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ) → 𝑅𝑆 )

Proof

Step Hyp Ref Expression
1 ps1.l = ( le ‘ 𝐾 )
2 ps1.j = ( join ‘ 𝐾 )
3 ps1.a 𝐴 = ( Atoms ‘ 𝐾 )
4 simp33 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑃𝑄 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ) → ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) )
5 simp1 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑃𝑄 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ) → 𝐾 ∈ HL )
6 simp21 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑃𝑄 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ) → 𝑃𝐴 )
7 simp22 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑃𝑄 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ) → 𝑄𝐴 )
8 simp23 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑃𝑄 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ) → 𝑃𝑄 )
9 simp31 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑃𝑄 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ) → 𝑅𝐴 )
10 simp32 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑃𝑄 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ) → 𝑆𝐴 )
11 1 2 3 ps-1 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑃𝑄 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ↔ ( 𝑃 𝑄 ) = ( 𝑅 𝑆 ) ) )
12 5 6 7 8 9 10 11 syl132anc ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑃𝑄 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ) → ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ↔ ( 𝑃 𝑄 ) = ( 𝑅 𝑆 ) ) )
13 4 12 mpbid ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑃𝑄 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ) → ( 𝑃 𝑄 ) = ( 𝑅 𝑆 ) )
14 2 3 lnnat ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃𝑄 ↔ ¬ ( 𝑃 𝑄 ) ∈ 𝐴 ) )
15 5 6 7 14 syl3anc ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑃𝑄 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ) → ( 𝑃𝑄 ↔ ¬ ( 𝑃 𝑄 ) ∈ 𝐴 ) )
16 8 15 mpbid ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑃𝑄 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ) → ¬ ( 𝑃 𝑄 ) ∈ 𝐴 )
17 13 16 eqneltrrd ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑃𝑄 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ) → ¬ ( 𝑅 𝑆 ) ∈ 𝐴 )
18 2 3 lnnat ( ( 𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴 ) → ( 𝑅𝑆 ↔ ¬ ( 𝑅 𝑆 ) ∈ 𝐴 ) )
19 5 9 10 18 syl3anc ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑃𝑄 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ) → ( 𝑅𝑆 ↔ ¬ ( 𝑅 𝑆 ) ∈ 𝐴 ) )
20 17 19 mpbird ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑃𝑄 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) ) → 𝑅𝑆 )