This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 ≤ 𝑋 ↔ 𝑅 = 𝑃 ) )