Metamath Proof Explorer


Theorem lpni

Description: For any line in a planar incidence geometry, there exists a point not on the line. (Contributed by Jeff Hankins, 15-Aug-2009)

Ref Expression
Hypothesis l2p.1 P = G
Assertion lpni G Plig L G a P a L

Proof

Step Hyp Ref Expression
1 l2p.1 P = G
2 1 tncp G Plig b P c P d P l G ¬ b l c l d l
3 eleq2 l = L b l b L
4 eleq2 l = L c l c L
5 eleq2 l = L d l d L
6 3 4 5 3anbi123d l = L b l c l d l b L c L d L
7 6 notbid l = L ¬ b l c l d l ¬ b L c L d L
8 7 rspccv l G ¬ b l c l d l L G ¬ b L c L d L
9 eleq1w a = b a L b L
10 9 notbid a = b ¬ a L ¬ b L
11 10 rspcev b P ¬ b L a P ¬ a L
12 11 ex b P ¬ b L a P ¬ a L
13 eleq1w a = c a L c L
14 13 notbid a = c ¬ a L ¬ c L
15 14 rspcev c P ¬ c L a P ¬ a L
16 15 ex c P ¬ c L a P ¬ a L
17 eleq1w a = d a L d L
18 17 notbid a = d ¬ a L ¬ d L
19 18 rspcev d P ¬ d L a P ¬ a L
20 19 ex d P ¬ d L a P ¬ a L
21 12 16 20 3jaao b P c P d P ¬ b L ¬ c L ¬ d L a P ¬ a L
22 3ianor ¬ b L c L d L ¬ b L ¬ c L ¬ d L
23 df-nel a L ¬ a L
24 23 rexbii a P a L a P ¬ a L
25 21 22 24 3imtr4g b P c P d P ¬ b L c L d L a P a L
26 8 25 syl9r b P c P d P l G ¬ b l c l d l L G a P a L
27 26 3expia b P c P d P l G ¬ b l c l d l L G a P a L
28 27 rexlimdv b P c P d P l G ¬ b l c l d l L G a P a L
29 28 rexlimivv b P c P d P l G ¬ b l c l d l L G a P a L
30 2 29 syl G Plig L G a P a L
31 30 imp G Plig L G a P a L