tgbtwnxfr - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tgbtwnxfr		Structured version Visualization version GIF version

Theorem tgbtwnxfr 28607

Description: A condition for extending betweenness to a new set of points based on congruence with another set of points. Theorem 4.6 of [Schwabhauser] p. 36. (Contributed by Thierry Arnoux, 27-Apr-2019.)

**Hypotheses**
Ref	Expression
tgcgrxfr.p	⊢ 𝑃 = (Base‘𝐺)
tgcgrxfr.m	⊢ − = (dist‘𝐺)
tgcgrxfr.i	⊢ 𝐼 = (Itv‘𝐺)
tgcgrxfr.r	⊢ ∼ = (cgrG‘𝐺)
tgcgrxfr.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
tgbtwnxfr.a	⊢ (𝜑 → 𝐴 ∈ 𝑃)
tgbtwnxfr.b	⊢ (𝜑 → 𝐵 ∈ 𝑃)
tgbtwnxfr.c	⊢ (𝜑 → 𝐶 ∈ 𝑃)
tgbtwnxfr.d	⊢ (𝜑 → 𝐷 ∈ 𝑃)
tgbtwnxfr.e	⊢ (𝜑 → 𝐸 ∈ 𝑃)
tgbtwnxfr.f	⊢ (𝜑 → 𝐹 ∈ 𝑃)
tgbtwnxfr.2	⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)
tgbtwnxfr.1	⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))

**Assertion**
Ref	Expression
tgbtwnxfr	⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐹))

Proof of Theorem tgbtwnxfr Dummy variable 𝑒 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		tgcgrxfr.p	. . . 4 ⊢ 𝑃 = (Base‘𝐺)
2		tgcgrxfr.m	. . . 4 ⊢ − = (dist‘𝐺)
3		tgcgrxfr.i	. . . 4 ⊢ 𝐼 = (Itv‘𝐺)
4		tgcgrxfr.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
5	4	ad2antrr 727	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝐺 ∈ TarskiG)
6		simplr 769	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝑒 ∈ 𝑃)
7		tgbtwnxfr.e	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ 𝑃)
8	7	ad2antrr 727	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝐸 ∈ 𝑃)
9		tgbtwnxfr.d	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
10	9	ad2antrr 727	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝐷 ∈ 𝑃)
11		tgbtwnxfr.f	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ 𝑃)
12	11	ad2antrr 727	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝐹 ∈ 𝑃)
13		simprl 771	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝑒 ∈ (𝐷𝐼𝐹))
14		eqidd 2738	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → (𝐷 − 𝐹) = (𝐷 − 𝐹))
15		eqidd 2738	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → (𝑒 − 𝐹) = (𝑒 − 𝐹))
16		tgcgrxfr.r	. . . . . 6 ⊢ ∼ = (cgrG‘𝐺)
17		tgbtwnxfr.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
18	17	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝐴 ∈ 𝑃)
19		tgbtwnxfr.b	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
20	19	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝐵 ∈ 𝑃)
21		tgbtwnxfr.c	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
22	21	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝐶 ∈ 𝑃)
23		simprr 773	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)
24	1, 2, 3, 16, 5, 18, 20, 22, 10, 6, 12, 23	trgcgrcom 28605	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → ⟨“𝐷𝑒𝐹”⟩ ∼ ⟨“𝐴𝐵𝐶”⟩)
25		tgbtwnxfr.2	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)
26	25	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)
27	1, 2, 3, 16, 5, 10, 6, 12, 18, 20, 22, 24, 10, 8, 12, 26	cgr3tr 28606	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → ⟨“𝐷𝑒𝐹”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)
28	1, 2, 3, 16, 5, 10, 6, 12, 10, 8, 12, 27	trgcgrcom 28605	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → ⟨“𝐷𝐸𝐹”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)
29	1, 2, 3, 16, 5, 10, 8, 12, 10, 6, 12, 28	cgr3simp1 28597	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → (𝐷 − 𝐸) = (𝐷 − 𝑒))
30	1, 2, 3, 16, 5, 10, 8, 12, 10, 6, 12, 28	cgr3simp2 28598	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → (𝐸 − 𝐹) = (𝑒 − 𝐹))
31	1, 2, 3, 5, 8, 12, 6, 12, 30	tgcgrcomlr 28557	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → (𝐹 − 𝐸) = (𝐹 − 𝑒))
32	1, 2, 3, 5, 10, 6, 12, 8, 10, 6, 12, 6, 13, 13, 14, 15, 29, 31	tgifscgr 28585	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → (𝑒 − 𝐸) = (𝑒 − 𝑒))
33	1, 2, 3, 5, 6, 8, 6, 32	axtgcgrid 28540	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝑒 = 𝐸)
34	33, 13	eqeltrrd 2838	. 2 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝐸 ∈ (𝐷𝐼𝐹))
35		tgbtwnxfr.1	. . 3 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))
36	1, 2, 3, 16, 4, 17, 19, 21, 9, 7, 11, 25	cgr3simp3 28599	. . . 4 ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷))
37	1, 2, 3, 4, 21, 17, 11, 9, 36	tgcgrcomlr 28557	. . 3 ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹))
38	1, 2, 3, 16, 4, 17, 19, 21, 9, 11, 35, 37	tgcgrxfr 28595	. 2 ⊢ (𝜑 → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩))
39	34, 38	r19.29a 3145	1 ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 class class class wbr 5099 ‘cfv 6493 (class class class)co 7361 ⟨“cs3 14770 Basecbs 17141 distcds 17191 TarskiGcstrkg 28504 Itvcitv 28510 cgrGccgrg 28587

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5225 ax-sep 5242 ax-nul 5252 ax-pow 5311 ax-pr 5378 ax-un 7683 ax-cnex 11087 ax-resscn 11088 ax-1cn 11089 ax-icn 11090 ax-addcl 11091 ax-addrcl 11092 ax-mulcl 11093 ax-mulrcl 11094 ax-mulcom 11095 ax-addass 11096 ax-mulass 11097 ax-distr 11098 ax-i2m1 11099 ax-1ne0 11100 ax-1rid 11101 ax-rnegex 11102 ax-rrecex 11103 ax-cnre 11104 ax-pre-lttri 11105 ax-pre-lttrn 11106 ax-pre-ltadd 11107 ax-pre-mulgt0 11108

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-reu 3352 df-rab 3401 df-v 3443 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4287 df-if 4481 df-pw 4557 df-sn 4582 df-pr 4584 df-tp 4586 df-op 4588 df-uni 4865 df-int 4904 df-iun 4949 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-om 7812 df-1st 7936 df-2nd 7937 df-frecs 8226 df-wrecs 8257 df-recs 8306 df-rdg 8344 df-1o 8400 df-oadd 8404 df-er 8638 df-pm 8771 df-en 8889 df-dom 8890 df-sdom 8891 df-fin 8892 df-dju 9818 df-card 9856 df-pnf 11173 df-mnf 11174 df-xr 11175 df-ltxr 11176 df-le 11177 df-sub 11371 df-neg 11372 df-nn 12151 df-2 12213 df-3 12214 df-n0 12407 df-xnn0 12480 df-z 12494 df-uz 12757 df-fz 13429 df-fzo 13576 df-hash 14259 df-word 14442 df-concat 14499 df-s1 14525 df-s2 14776 df-s3 14777 df-trkgc 28525 df-trkgb 28526 df-trkgcb 28527 df-trkg 28530 df-cgrg 28588

This theorem is referenced by: lnxfr 28643 tgfscgr 28645 legov 28662 legov2 28663 legtrd 28666 mirbtwni 28748 cgrabtwn 28903 cgrahl 28904

W3C validator