atbtwnex

Description: Given atoms P in X and Q not in X , there exists an atom r not in X such that the line Q .\/ r intersects X at P . (Contributed by NM, 1-Aug-2012)

	Ref	Expression
Hypotheses	atbtwn.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	atbtwn.l	⊢ ≤ = ( le ‘ 𝐾 )
	atbtwn.j	⊢ ∨ = ( join ‘ 𝐾 )
	atbtwn.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	atbtwnex	⊢ ( ( ( 𝐾 ∈ 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		simp1l1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ HL )
23		simp1l2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ∈ 𝐴 )
24		simp1l3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑄 ∈ 𝐴 )
25	2 3 4	hlatexch2	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ≠ 𝑄 ) → ( 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑃 ≤ ( 𝑟 ∨ 𝑄 ) ) )
26	22 14 23 24 11 25	syl131anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑃 ≤ ( 𝑟 ∨ 𝑄 ) ) )
27	18 26	mpd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ≤ ( 𝑟 ∨ 𝑄 ) )
28	3 4	hlatjcom	⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑟 ) = ( 𝑟 ∨ 𝑄 ) )
29	22 24 14 28	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑄 ∨ 𝑟 ) = ( 𝑟 ∨ 𝑄 ) )
30	27 29	breqtrrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) )
31	11 21 30	3jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑟 ≠ 𝑄 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) )
32	31	3exp	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( 𝑟 ∈ 𝐴 → ( ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑟 ≠ 𝑄 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) ) )
33	32	reximdvai	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑄 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) )
34	10 33	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑄 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) )

Metamath Proof Explorer

Theorem atbtwnex

Proof