Theorem tglinerflx1

Description: Reflexivity law for line membership. Part of theorem 6.17 of Schwabhauser p. 45. (Contributed by Thierry Arnoux, 17-May-2019)

	Ref	Expression
Hypotheses	tglineelsb2.p	|- B = ( Base ` G )
	tglineelsb2.i	|- I = ( Itv ` G )
	tglineelsb2.l	|- L = ( LineG ` G )
	tglineelsb2.g	|- ( ph -> G e. TarskiG )
	tglineelsb2.1	|- ( ph -> P e. B )
	tglineelsb2.2	|- ( ph -> Q e. B )
	tglineelsb2.4	|- ( ph -> P =/= Q )
Assertion	tglinerflx1	|- ( ph -> P e. ( P L Q ) )

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	|- B = ( Base ` G )
2		tglineelsb2.i	|- I = ( Itv ` G )
3		tglineelsb2.l	|- L = ( LineG ` G )
4		tglineelsb2.g	|- ( ph -> G e. TarskiG )
5		tglineelsb2.1	|- ( ph -> P e. B )
6		tglineelsb2.2	|- ( ph -> Q e. B )
7		tglineelsb2.4	|- ( ph -> P =/= Q )
8		eqid	|- ( dist ` G ) = ( dist ` G )
9	1 8 2 4 5 6	tgbtwntriv1	|- ( ph -> P e. ( P I Q ) )
10	1 2 3 4 5 6 5 7 9	btwnlng1	|- ( ph -> P e. ( P L Q ) )