Metamath Proof Explorer

Theorem atbtwn

Description: Property of a 3rd atom R on a line P .\/ Q intersecting element X at P . (Contributed by NM, 30-Jul-2012)

Ref Expression
Hypotheses atbtwn.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
atbtwn.l ⊢ ≤ = ( le ‘ 𝐾 )
atbtwn.j ⊢ ∨ = ( join ‘ 𝐾 )
atbtwn.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion atbtwn ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 ≠ 𝑃 ↔ ¬ 𝑅 ≤ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 atbtwn.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 atbtwn.l ⊢ ≤ = ( le ‘ 𝐾 )
3 atbtwn.j ⊢ ∨ = ( join ‘ 𝐾 )
4 atbtwn.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 simpl33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
6 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → 𝑅 ≤ 𝑋 )
7 simpl11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → 𝐾 ∈ HL )
8 7 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → 𝐾 ∈ Lat )
9 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → 𝑅 ∈ 𝐴 )
10 1 4 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ 𝐵 )
11 9 10 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → 𝑅 ∈ 𝐵 )
12 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
13 1 3 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
14 12 13 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
15 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → 𝑋 ∈ 𝐵 )
16 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
17 1 2 16 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ 𝑋 ) ↔ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ) )
18 8 11 14 15 17 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → ( ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ 𝑋 ) ↔ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) ) )
19 5 6 18 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) )
20 simpl12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → 𝑃 ∈ 𝐴 )
21 simpl13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → 𝑄 ∈ 𝐴 )
22 simpl31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → 𝑃 ≤ 𝑋 )
23 simpl32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → ¬ 𝑄 ≤ 𝑋 )
24 1 2 3 16 4 2atjm ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) = 𝑃 )
25 7 20 21 15 22 23 24 syl132anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → ( ( 𝑃 ∨ 𝑄 ) ( meet ‘ 𝐾 ) 𝑋 ) = 𝑃 )
26 19 25 breqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → 𝑅 ≤ 𝑃 )
27 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
28 7 27 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → 𝐾 ∈ AtLat )
29 2 4 atcmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑅 ≤ 𝑃 ↔ 𝑅 = 𝑃 ) )
30 28 9 20 29 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → ( 𝑅 ≤ 𝑃 ↔ 𝑅 = 𝑃 ) )
31 26 30 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≤ 𝑋 ) → 𝑅 = 𝑃 )
32 31 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 ≤ 𝑋 → 𝑅 = 𝑃 ) )
33 32 necon3ad ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 ≠ 𝑃 → ¬ 𝑅 ≤ 𝑋 ) )
34 simp31 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ≤ 𝑋 )
35 nbrne2 ⊢ ( ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑅 ≤ 𝑋 ) → 𝑃 ≠ 𝑅 )
36 35 necomd ⊢ ( ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑅 ≤ 𝑋 ) → 𝑅 ≠ 𝑃 )
37 36 ex ⊢ ( 𝑃 ≤ 𝑋 → ( ¬ 𝑅 ≤ 𝑋 → 𝑅 ≠ 𝑃 ) )
38 34 37 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ¬ 𝑅 ≤ 𝑋 → 𝑅 ≠ 𝑃 ) )
39 33 38 impbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 ≠ 𝑃 ↔ ¬ 𝑅 ≤ 𝑋 ) )