Metamath Proof Explorer

Theorem atbtwnexOLDN

Description: There exists a 3rd atom r on a line P .\/ Q intersecting element X at P , such that r is different from Q and not in X . (Contributed by NM, 30-Jul-2012) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 atbtwn.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 atbtwn.l ⊢ ≤ = ( le ‘ 𝐾 )
3 atbtwn.j ⊢ ∨ = ( join ‘ 𝐾 )
4 atbtwn.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 simpr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑃 ≤ 𝑋 )
6 simpr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ¬ 𝑄 ≤ 𝑋 )
7 nbrne2 ⊢ ( ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) → 𝑃 ≠ 𝑄 )
8 5 6 7 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑃 ≠ 𝑄 )
9 2 3 4 hlsupr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )
10 8 9 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )
11 simp32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑟 ≠ 𝑄 )
12 simp31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑟 ≠ 𝑃 )
13 simp1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
14 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑟 ∈ 𝐴 )
15 simp1r1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑋 ∈ 𝐵 )
16 simp1r2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ≤ 𝑋 )
17 simp1r3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑄 ≤ 𝑋 )
18 simp33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) )
19 1 2 3 4 atbtwn ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑟 ≠ 𝑃 ↔ ¬ 𝑟 ≤ 𝑋 ) )
20 13 14 15 16 17 18 19 syl123anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑟 ≠ 𝑃 ↔ ¬ 𝑟 ≤ 𝑋 ) )
21 12 20 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑟 ≤ 𝑋 )
22 11 21 18 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑟 ≠ 𝑄 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )
23 22 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( 𝑟 ∈ 𝐴 → ( ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑟 ≠ 𝑄 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) )
24 23 reximdvai ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑄 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
25 10 24 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑄 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )