Metamath Proof Explorer


Theorem exatleN

Description: A condition for an atom to be less than or equal to a lattice element. Part of proof of Lemma A in Crawley p. 112. (Contributed by NM, 28-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses atomle.b 𝐵 = ( Base ‘ 𝐾 )
atomle.l = ( le ‘ 𝐾 )
atomle.j = ( join ‘ 𝐾 )
atomle.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion exatleN ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑅 𝑋𝑅 = 𝑃 ) )

Proof

Step Hyp Ref Expression
1 atomle.b 𝐵 = ( Base ‘ 𝐾 )
2 atomle.l = ( le ‘ 𝐾 )
3 atomle.j = ( join ‘ 𝐾 )
4 atomle.a 𝐴 = ( Atoms ‘ 𝐾 )
5 simpl32 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃 ) → ¬ 𝑄 𝑋 )
6 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → 𝐾 ∈ HL )
7 6 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → 𝐾 ∈ Lat )
8 simp122 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → 𝑄𝐴 )
9 1 4 atbase ( 𝑄𝐴𝑄𝐵 )
10 8 9 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → 𝑄𝐵 )
11 simp121 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → 𝑃𝐴 )
12 1 4 atbase ( 𝑃𝐴𝑃𝐵 )
13 11 12 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → 𝑃𝐵 )
14 simp123 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → 𝑅𝐴 )
15 1 4 atbase ( 𝑅𝐴𝑅𝐵 )
16 14 15 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → 𝑅𝐵 )
17 1 3 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑃𝐵𝑅𝐵 ) → ( 𝑃 𝑅 ) ∈ 𝐵 )
18 7 13 16 17 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → ( 𝑃 𝑅 ) ∈ 𝐵 )
19 simp11r ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → 𝑋𝐵 )
20 14 8 11 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → ( 𝑅𝐴𝑄𝐴𝑃𝐴 ) )
21 simp2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → 𝑅𝑃 )
22 6 20 21 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → ( 𝐾 ∈ HL ∧ ( 𝑅𝐴𝑄𝐴𝑃𝐴 ) ∧ 𝑅𝑃 ) )
23 simp133 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → 𝑅 ( 𝑃 𝑄 ) )
24 2 3 4 hlatexch1 ( ( 𝐾 ∈ HL ∧ ( 𝑅𝐴𝑄𝐴𝑃𝐴 ) ∧ 𝑅𝑃 ) → ( 𝑅 ( 𝑃 𝑄 ) → 𝑄 ( 𝑃 𝑅 ) ) )
25 22 23 24 sylc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → 𝑄 ( 𝑃 𝑅 ) )
26 simp131 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → 𝑃 𝑋 )
27 simp3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → 𝑅 𝑋 )
28 1 2 3 latjle12 ( ( 𝐾 ∈ Lat ∧ ( 𝑃𝐵𝑅𝐵𝑋𝐵 ) ) → ( ( 𝑃 𝑋𝑅 𝑋 ) ↔ ( 𝑃 𝑅 ) 𝑋 ) )
29 7 13 16 19 28 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → ( ( 𝑃 𝑋𝑅 𝑋 ) ↔ ( 𝑃 𝑅 ) 𝑋 ) )
30 26 27 29 mpbi2and ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → ( 𝑃 𝑅 ) 𝑋 )
31 1 2 7 10 18 19 25 30 lattrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃𝑅 𝑋 ) → 𝑄 𝑋 )
32 31 3expia ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃 ) → ( 𝑅 𝑋𝑄 𝑋 ) )
33 5 32 mtod ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑅𝑃 ) → ¬ 𝑅 𝑋 )
34 33 ex ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑅𝑃 → ¬ 𝑅 𝑋 ) )
35 34 necon4ad ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑅 𝑋𝑅 = 𝑃 ) )
36 simp31 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) → 𝑃 𝑋 )
37 breq1 ( 𝑅 = 𝑃 → ( 𝑅 𝑋𝑃 𝑋 ) )
38 36 37 syl5ibrcom ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑅 = 𝑃𝑅 𝑋 ) )
39 35 38 impbid ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃 𝑋 ∧ ¬ 𝑄 𝑋𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑅 𝑋𝑅 = 𝑃 ) )