Metamath Proof Explorer

Theorem linerflx1

Description: Reflexivity law for line membership. Part of theorem 6.17 of Schwabhauser p. 45. (Contributed by Scott Fenton, 28-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion linerflx1 
|- ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> P e. ( P Line Q ) )

Proof

Step Hyp Ref Expression
1 simpr1 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> P e. ( EE ` N ) )
2 colineartriv1 
 |-  ( ( N e. NN /\ P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) -> P Colinear <. P , Q >. )
3 2 3adant3r3 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> P Colinear <. P , Q >. )
4 breq1 
 |-  ( x = P -> ( x Colinear <. P , Q >. <-> P Colinear <. P , Q >. ) )
5 4 elrab 
 |-  ( P e. { x e. ( EE ` N ) | x Colinear <. P , Q >. } <-> ( P e. ( EE ` N ) /\ P Colinear <. P , Q >. ) )
6 1 3 5 sylanbrc 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> P e. { x e. ( EE ` N ) | x Colinear <. P , Q >. } )
7 fvline2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> ( P Line Q ) = { x e. ( EE ` N ) | x Colinear <. P , Q >. } )
8 6 7 eleqtrrd 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> P e. ( P Line Q ) )