Metamath Proof Explorer


Theorem tglinerflx2

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 tglinerflx2 ( 𝜑𝑄 ∈ ( 𝑃 𝐿 𝑄 ) )

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 tgbtwntriv2 ( 𝜑𝑄 ∈ ( 𝑃 𝐼 𝑄 ) )
10 1 2 3 4 5 6 6 7 9 btwnlng1 ( 𝜑𝑄 ∈ ( 𝑃 𝐿 𝑄 ) )