Metamath Proof Explorer


Theorem hilbert1.1

Description: There is a line through any two distinct points. Hilbert's axiom I.1 for geometry. (Contributed by Scott Fenton, 29-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion hilbert1.1 NP𝔼NQ𝔼NPQxLinesEEPxQx

Proof

Step Hyp Ref Expression
1 simp1 P𝔼NQ𝔼NPQP𝔼N
2 simp2 P𝔼NQ𝔼NPQQ𝔼N
3 simp3 P𝔼NQ𝔼NPQPQ
4 eqidd P𝔼NQ𝔼NPQPLineQ=PLineQ
5 neeq1 p=PpqPq
6 oveq1 p=PpLineq=PLineq
7 6 eqeq2d p=PPLineQ=pLineqPLineQ=PLineq
8 5 7 anbi12d p=PpqPLineQ=pLineqPqPLineQ=PLineq
9 neeq2 q=QPqPQ
10 oveq2 q=QPLineq=PLineQ
11 10 eqeq2d q=QPLineQ=PLineqPLineQ=PLineQ
12 9 11 anbi12d q=QPqPLineQ=PLineqPQPLineQ=PLineQ
13 8 12 rspc2ev P𝔼NQ𝔼NPQPLineQ=PLineQp𝔼Nq𝔼NpqPLineQ=pLineq
14 1 2 3 4 13 syl112anc P𝔼NQ𝔼NPQp𝔼Nq𝔼NpqPLineQ=pLineq
15 fveq2 n=N𝔼n=𝔼N
16 15 rexeqdv n=Nq𝔼npqPLineQ=pLineqq𝔼NpqPLineQ=pLineq
17 15 16 rexeqbidv n=Np𝔼nq𝔼npqPLineQ=pLineqp𝔼Nq𝔼NpqPLineQ=pLineq
18 17 rspcev Np𝔼Nq𝔼NpqPLineQ=pLineqnp𝔼nq𝔼npqPLineQ=pLineq
19 14 18 sylan2 NP𝔼NQ𝔼NPQnp𝔼nq𝔼npqPLineQ=pLineq
20 ellines PLineQLinesEEnp𝔼nq𝔼npqPLineQ=pLineq
21 19 20 sylibr NP𝔼NQ𝔼NPQPLineQLinesEE
22 linerflx1 NP𝔼NQ𝔼NPQPPLineQ
23 linerflx2 NP𝔼NQ𝔼NPQQPLineQ
24 eleq2 x=PLineQPxPPLineQ
25 eleq2 x=PLineQQxQPLineQ
26 24 25 anbi12d x=PLineQPxQxPPLineQQPLineQ
27 26 rspcev PLineQLinesEEPPLineQQPLineQxLinesEEPxQx
28 21 22 23 27 syl12anc NP𝔼NQ𝔼NPQxLinesEEPxQx