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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tglineelsb2.1	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
	tglineelsb2.2	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
	tglineelsb2.4	⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
Assertion	tglinerflx1	⊢ ( 𝜑 → 𝑃 ∈ ( 𝑃 𝐿 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tglineelsb2.1	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
6		tglineelsb2.2	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
7		tglineelsb2.4	⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
8		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
9	1 8 2 4 5 6	tgbtwntriv1	⊢ ( 𝜑 → 𝑃 ∈ ( 𝑃 𝐼 𝑄 ) )
10	1 2 3 4 5 6 5 7 9	btwnlng1	⊢ ( 𝜑 → 𝑃 ∈ ( 𝑃 𝐿 𝑄 ) )