Metamath Proof Explorer
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 |
⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 𝐿 𝑄 ) ) |