Theorem tglinerflx1 25945

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

Hypotheses

Ref	Expression
tglineelsb2.p	⊢ 𝐵 = (Base‘𝐺)
tglineelsb2.i	⊢ 𝐼 = (Itv‘𝐺)
tglineelsb2.l	⊢ 𝐿 = (LineG‘𝐺)
tglineelsb2.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
tglineelsb2.1	⊢ (𝜑 → 𝑃 ∈ 𝐵)
tglineelsb2.2	⊢ (𝜑 → 𝑄 ∈ 𝐵)
tglineelsb2.4	⊢ (𝜑 → 𝑃 ≠ 𝑄)

Assertion

Ref	Expression
tglinerflx1	⊢ (𝜑 → 𝑃 ∈ (𝑃𝐿𝑄))

Proof of Theorem tglinerflx1

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

Syntax hints:   → wi 4   = wceq 1658   ∈ wcel 2166   ≠ wne 2999  ‘cfv 6123  (class class class)co 6905  Basecbs 16222  distcds 16314  TarskiGcstrkg 25742  Itvcitv 25748  LineGclng 25749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-iota 6086  df-fun 6125  df-fv 6131  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-trkgc 25760  df-trkgb 25761  df-trkgcb 25762  df-trkg 25765

This theorem is referenced by:  tghilberti1  25949  tglnne0  25952  tglnpt2  25953  tglineneq  25956  coltr  25959  colline  25961  footex  26030  foot  26031  footne  26032  perprag  26035  colperp  26038  colperpexlem3  26041  mideulem2  26043  outpasch  26064  hlpasch  26065  lnopp2hpgb  26072  colopp  26078  lmieu  26093  lmimid  26103  hypcgrlem1  26108  hypcgrlem2  26109  trgcopyeulem  26114  tgasa1  26157