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 28514

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 726	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝐺 ∈ TarskiG)
6		simplr 768	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝑒 ∈ 𝑃)
7		tgbtwnxfr.e	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ 𝑃)
8	7	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝐸 ∈ 𝑃)
9		tgbtwnxfr.d	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
10	9	ad2antrr 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝐷 ∈ 𝑃)
11		tgbtwnxfr.f	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ 𝑃)
12	11	ad2antrr 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝐹 ∈ 𝑃)
13		simprl 770	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝑒 ∈ (𝐷𝐼𝐹))
14		eqidd 2732	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → (𝐷 − 𝐹) = (𝐷 − 𝐹))
15		eqidd 2732	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → (𝑒 − 𝐹) = (𝑒 − 𝐹))
16		tgcgrxfr.r	. . . . . 6 ⊢ ∼ = (cgrG‘𝐺)
17		tgbtwnxfr.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
18	17	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝐴 ∈ 𝑃)
19		tgbtwnxfr.b	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
20	19	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝐵 ∈ 𝑃)
21		tgbtwnxfr.c	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
22	21	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝐶 ∈ 𝑃)
23		simprr 772	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)
24	1, 2, 3, 16, 5, 18, 20, 22, 10, 6, 12, 23	trgcgrcom 28512	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → ⟨“𝐷𝑒𝐹”⟩ ∼ ⟨“𝐴𝐵𝐶”⟩)
25		tgbtwnxfr.2	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)
26	25	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)
27	1, 2, 3, 16, 5, 10, 6, 12, 18, 20, 22, 24, 10, 8, 12, 26	cgr3tr 28513	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → ⟨“𝐷𝑒𝐹”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)
28	1, 2, 3, 16, 5, 10, 6, 12, 10, 8, 12, 27	trgcgrcom 28512	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → ⟨“𝐷𝐸𝐹”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)
29	1, 2, 3, 16, 5, 10, 8, 12, 10, 6, 12, 28	cgr3simp1 28504	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → (𝐷 − 𝐸) = (𝐷 − 𝑒))
30	1, 2, 3, 16, 5, 10, 8, 12, 10, 6, 12, 28	cgr3simp2 28505	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → (𝐸 − 𝐹) = (𝑒 − 𝐹))
31	1, 2, 3, 5, 8, 12, 6, 12, 30	tgcgrcomlr 28464	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → (𝐹 − 𝐸) = (𝐹 − 𝑒))
32	1, 2, 3, 5, 10, 6, 12, 8, 10, 6, 12, 6, 13, 13, 14, 15, 29, 31	tgifscgr 28492	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → (𝑒 − 𝐸) = (𝑒 − 𝑒))
33	1, 2, 3, 5, 6, 8, 6, 32	axtgcgrid 28447	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝑒 = 𝐸)
34	33, 13	eqeltrrd 2832	. 2 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩)) → 𝐸 ∈ (𝐷𝐼𝐹))
35		tgbtwnxfr.1	. . 3 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))
36	1, 2, 3, 16, 4, 17, 19, 21, 9, 7, 11, 25	cgr3simp3 28506	. . . 4 ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷))
37	1, 2, 3, 4, 21, 17, 11, 9, 36	tgcgrcomlr 28464	. . 3 ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹))
38	1, 2, 3, 16, 4, 17, 19, 21, 9, 11, 35, 37	tgcgrxfr 28502	. 2 ⊢ (𝜑 → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝐹) ∧ ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝑒𝐹”⟩))
39	34, 38	r19.29a 3140	1 ⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2111 class class class wbr 5093 ‘cfv 6487 (class class class)co 7352 ⟨“cs3 14755 Basecbs 17126 distcds 17176 TarskiGcstrkg 28411 Itvcitv 28417 cgrGccgrg 28494

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5219 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-cnex 11068 ax-resscn 11069 ax-1cn 11070 ax-icn 11071 ax-addcl 11072 ax-addrcl 11073 ax-mulcl 11074 ax-mulrcl 11075 ax-mulcom 11076 ax-addass 11077 ax-mulass 11078 ax-distr 11079 ax-i2m1 11080 ax-1ne0 11081 ax-1rid 11082 ax-rnegex 11083 ax-rrecex 11084 ax-cnre 11085 ax-pre-lttri 11086 ax-pre-lttrn 11087 ax-pre-ltadd 11088 ax-pre-mulgt0 11089

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-tp 4580 df-op 4582 df-uni 4859 df-int 4898 df-iun 4943 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6254 df-ord 6315 df-on 6316 df-lim 6317 df-suc 6318 df-iota 6443 df-fun 6489 df-fn 6490 df-f 6491 df-f1 6492 df-fo 6493 df-f1o 6494 df-fv 6495 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-om 7803 df-1st 7927 df-2nd 7928 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-1o 8391 df-oadd 8395 df-er 8628 df-pm 8759 df-en 8876 df-dom 8877 df-sdom 8878 df-fin 8879 df-dju 9800 df-card 9838 df-pnf 11154 df-mnf 11155 df-xr 11156 df-ltxr 11157 df-le 11158 df-sub 11352 df-neg 11353 df-nn 12132 df-2 12194 df-3 12195 df-n0 12388 df-xnn0 12461 df-z 12475 df-uz 12739 df-fz 13414 df-fzo 13561 df-hash 14244 df-word 14427 df-concat 14484 df-s1 14510 df-s2 14761 df-s3 14762 df-trkgc 28432 df-trkgb 28433 df-trkgcb 28434 df-trkg 28437 df-cgrg 28495

This theorem is referenced by: lnxfr 28550 tgfscgr 28552 legov 28569 legov2 28570 legtrd 28573 mirbtwni 28655 cgrabtwn 28810 cgrahl 28811

W3C validator