tgbtwnxfr

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)

	Ref	Expression
Hypotheses	tgcgrxfr.p	$⊢ P = {Base}_{G}$
	tgcgrxfr.m	$⊢ \underset{˙}{-} = dist (G)$
	tgcgrxfr.i	$⊢ I = Itv (G)$
	tgcgrxfr.r	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
	tgcgrxfr.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgbtwnxfr.a	$⊢ φ \to A \in P$
	tgbtwnxfr.b	$⊢ φ \to B \in P$
	tgbtwnxfr.c	$⊢ φ \to C \in P$
	tgbtwnxfr.d	$⊢ φ \to D \in P$
	tgbtwnxfr.e	$⊢ φ \to E \in P$
	tgbtwnxfr.f	$⊢ φ \to F \in P$
	tgbtwnxfr.2	$⊢ φ \to ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D E F ”⟩$
	tgbtwnxfr.1	$⊢ φ \to B \in (A I C)$
Assertion	tgbtwnxfr	$⊢ φ \to E \in (D I F)$

Proof

Step	Hyp	Ref	Expression
1		tgcgrxfr.p	$⊢ P = {Base}_{G}$
2		tgcgrxfr.m	$⊢ \underset{˙}{-} = dist (G)$
3		tgcgrxfr.i	$⊢ I = Itv (G)$
4		tgcgrxfr.r	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
5		tgcgrxfr.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		tgbtwnxfr.a	$⊢ φ \to A \in P$
7		tgbtwnxfr.b	$⊢ φ \to B \in P$
8		tgbtwnxfr.c	$⊢ φ \to C \in P$
9		tgbtwnxfr.d	$⊢ φ \to D \in P$
10		tgbtwnxfr.e	$⊢ φ \to E \in P$
11		tgbtwnxfr.f	$⊢ φ \to F \in P$
12		tgbtwnxfr.2	$⊢ φ \to ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D E F ”⟩$
13		tgbtwnxfr.1	$⊢ φ \to B \in (A I C)$
14	5	ad2antrr	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to G \in 𝒢_{Tarski}$
15		simplr	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to e \in P$
16	10	ad2antrr	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to E \in P$
17	9	ad2antrr	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to D \in P$
18	11	ad2antrr	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to F \in P$
19		simprl	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to e \in (D I F)$
20		eqidd	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to D \underset{˙}{-} F = D \underset{˙}{-} F$
21		eqidd	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to e \underset{˙}{-} F = e \underset{˙}{-} F$
22	6	ad2antrr	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to A \in P$
23	7	ad2antrr	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to B \in P$
24	8	ad2antrr	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to C \in P$
25		simprr	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩$
26	1 2 3 4 14 22 23 24 17 15 18 25	trgcgrcom	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to ⟨“ D e F ”⟩ \underset{˙}{\sim} ⟨“ A B C ”⟩$
27	12	ad2antrr	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D E F ”⟩$
28	1 2 3 4 14 17 15 18 22 23 24 26 17 16 18 27	cgr3tr	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to ⟨“ D e F ”⟩ \underset{˙}{\sim} ⟨“ D E F ”⟩$
29	1 2 3 4 14 17 15 18 17 16 18 28	trgcgrcom	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to ⟨“ D E F ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩$
30	1 2 3 4 14 17 16 18 17 15 18 29	cgr3simp1	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to D \underset{˙}{-} E = D \underset{˙}{-} e$
31	1 2 3 4 14 17 16 18 17 15 18 29	cgr3simp2	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to E \underset{˙}{-} F = e \underset{˙}{-} F$
32	1 2 3 14 16 18 15 18 31	tgcgrcomlr	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to F \underset{˙}{-} E = F \underset{˙}{-} e$
33	1 2 3 14 17 15 18 16 17 15 18 15 19 19 20 21 30 32	tgifscgr	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to e \underset{˙}{-} E = e \underset{˙}{-} e$
34	1 2 3 14 15 16 15 33	axtgcgrid	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to e = E$
35	34 19	eqeltrrd	$⊢ ((φ \land e \in P) \land (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)) \to E \in (D I F)$
36	1 2 3 4 5 6 7 8 9 10 11 12	cgr3simp3	$⊢ φ \to C \underset{˙}{-} A = F \underset{˙}{-} D$
37	1 2 3 5 8 6 11 9 36	tgcgrcomlr	$⊢ φ \to A \underset{˙}{-} C = D \underset{˙}{-} F$
38	1 2 3 4 5 6 7 8 9 11 13 37	tgcgrxfr	$⊢ φ \to \exists e \in P (e \in (D I F) \land ⟨“ A B C ”⟩ \underset{˙}{\sim} ⟨“ D e F ”⟩)$
39	35 38	r19.29a	$⊢ φ \to E \in (D I F)$

Metamath Proof Explorer

Theorem tgbtwnxfr

Proof