Metamath Proof Explorer


Theorem 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 B = Base K
atbtwn.l ˙ = K
atbtwn.j ˙ = join K
atbtwn.a A = Atoms K
Assertion atbtwnex K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r Q ¬ r ˙ X P ˙ Q ˙ r

Proof

Step Hyp Ref Expression
1 atbtwn.b B = Base K
2 atbtwn.l ˙ = K
3 atbtwn.j ˙ = join K
4 atbtwn.a A = Atoms K
5 simpr2 K HL P A Q A X B P ˙ X ¬ Q ˙ X P ˙ X
6 simpr3 K HL P A Q A X B P ˙ X ¬ Q ˙ X ¬ Q ˙ X
7 nbrne2 P ˙ X ¬ Q ˙ X P Q
8 5 6 7 syl2anc K HL P A Q A X B P ˙ X ¬ Q ˙ X P Q
9 2 3 4 hlsupr K HL P A Q A P Q r A r P r Q r ˙ P ˙ Q
10 8 9 syldan K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q
11 simp32 K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q r Q
12 simp31 K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q r P
13 simp1l K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q K HL P A Q A
14 simp2 K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q r A
15 simp1r1 K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q X B
16 simp1r2 K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q P ˙ X
17 simp1r3 K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q ¬ Q ˙ X
18 simp33 K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q r ˙ P ˙ Q
19 1 2 3 4 atbtwn K HL P A Q A r A X B P ˙ X ¬ Q ˙ X r ˙ P ˙ Q r P ¬ r ˙ X
20 13 14 15 16 17 18 19 syl123anc K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q r P ¬ r ˙ X
21 12 20 mpbid K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q ¬ r ˙ X
22 simp1l1 K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q K HL
23 simp1l2 K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q P A
24 simp1l3 K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q Q A
25 2 3 4 hlatexch2 K HL r A P A Q A r Q r ˙ P ˙ Q P ˙ r ˙ Q
26 22 14 23 24 11 25 syl131anc K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q r ˙ P ˙ Q P ˙ r ˙ Q
27 18 26 mpd K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q P ˙ r ˙ Q
28 3 4 hlatjcom K HL Q A r A Q ˙ r = r ˙ Q
29 22 24 14 28 syl3anc K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q Q ˙ r = r ˙ Q
30 27 29 breqtrrd K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q P ˙ Q ˙ r
31 11 21 30 3jca K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q r Q ¬ r ˙ X P ˙ Q ˙ r
32 31 3exp K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q r Q ¬ r ˙ X P ˙ Q ˙ r
33 32 reximdvai K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r P r Q r ˙ P ˙ Q r A r Q ¬ r ˙ X P ˙ Q ˙ r
34 10 33 mpd K HL P A Q A X B P ˙ X ¬ Q ˙ X r A r Q ¬ r ˙ X P ˙ Q ˙ r