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={\mathrm{Base}}_G$$
	tglineelsb2.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tglineelsb2.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	tglineelsb2.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tglineelsb2.1	$$⊢\phi \to P\in B$$
	tglineelsb2.2	$$⊢\phi \to Q\in B$$
	tglineelsb2.4	$$⊢\phi \to P\ne Q$$
Assertion	tglinerflx1	$$⊢\phi \to P\in \left(PLQ\right)$$

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	$$⊢B={\mathrm{Base}}_G$$
2		tglineelsb2.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
3		tglineelsb2.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
4		tglineelsb2.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		tglineelsb2.1	$$⊢\phi \to P\in B$$
6		tglineelsb2.2	$$⊢\phi \to Q\in B$$
7		tglineelsb2.4	$$⊢\phi \to P\ne Q$$
8		eqid	$$⊢\mathrm{dist}\left(G\right)=\mathrm{dist}\left(G\right)$$
9	1 8 2 4 5 6	tgbtwntriv1	$$⊢\phi \to P\in \left(PIQ\right)$$
10	1 2 3 4 5 6 5 7 9	btwnlng1	$$⊢\phi \to P\in \left(PLQ\right)$$