![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > tglinerflx2 | Structured version Visualization version GIF version |
Description: Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Thierry Arnoux, 17-May-2019.) |
Ref | Expression |
---|---|
tglineelsb2.p | ⊢ 𝐵 = (Base‘𝐺) |
tglineelsb2.i | ⊢ 𝐼 = (Itv‘𝐺) |
tglineelsb2.l | ⊢ 𝐿 = (LineG‘𝐺) |
tglineelsb2.g | ⊢ (𝜑 → 𝐺 ∈ TarskiG) |
tglineelsb2.1 | ⊢ (𝜑 → 𝑃 ∈ 𝐵) |
tglineelsb2.2 | ⊢ (𝜑 → 𝑄 ∈ 𝐵) |
tglineelsb2.4 | ⊢ (𝜑 → 𝑃 ≠ 𝑄) |
Ref | Expression |
---|---|
tglinerflx2 | ⊢ (𝜑 → 𝑄 ∈ (𝑃𝐿𝑄)) |
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 2824 | . . 3 ⊢ (dist‘𝐺) = (dist‘𝐺) | |
9 | 1, 8, 2, 4, 5, 6 | tgbtwntriv2 25798 | . 2 ⊢ (𝜑 → 𝑄 ∈ (𝑃𝐼𝑄)) |
10 | 1, 2, 3, 4, 5, 6, 6, 7, 9 | btwnlng1 25930 | 1 ⊢ (𝜑 → 𝑄 ∈ (𝑃𝐿𝑄)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1658 ∈ wcel 2166 ≠ wne 2998 ‘cfv 6122 (class class class)co 6904 Basecbs 16221 distcds 16313 TarskiGcstrkg 25741 Itvcitv 25747 LineGclng 25748 |
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 2390 ax-ext 2802 ax-sep 5004 ax-nul 5012 ax-pr 5126 |
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 2604 df-eu 2639 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ne 2999 df-ral 3121 df-rex 3122 df-rab 3125 df-v 3415 df-sbc 3662 df-dif 3800 df-un 3802 df-in 3804 df-ss 3811 df-nul 4144 df-if 4306 df-sn 4397 df-pr 4399 df-op 4403 df-uni 4658 df-br 4873 df-opab 4935 df-id 5249 df-xp 5347 df-rel 5348 df-cnv 5349 df-co 5350 df-dm 5351 df-iota 6085 df-fun 6124 df-fv 6130 df-ov 6907 df-oprab 6908 df-mpt2 6909 df-trkgc 25759 df-trkgcb 25761 df-trkg 25764 |
This theorem is referenced by: tghilberti1 25948 tglnpt2 25952 colline 25960 footex 26029 foot 26030 footne 26031 perprag 26034 colperpexlem3 26040 mideulem2 26042 opphllem 26043 opphllem5 26059 opphllem6 26060 opphl 26062 outpasch 26063 hlpasch 26064 lnopp2hpgb 26071 hypcgrlem1 26107 hypcgrlem2 26108 trgcopyeulem 26113 acopy 26141 acopyeu 26142 tgasa1 26156 |
Copyright terms: Public domain | W3C validator |