tgifscgr

Description: Inner five segment congruence. Take two triangles, A D C and E H K , with B between A and C and F between E and K . If the other components of the triangles are congruent, then so are B D and F H . Theorem 4.2 of Schwabhauser p. 34. (Contributed by Thierry Arnoux, 24-Mar-2019)

	Ref	Expression
Hypotheses	tgbtwncgr.p	$⊢ P = {Base}_{G}$
	tgbtwncgr.m	$⊢ \underset{˙}{-} = dist (G)$
	tgbtwncgr.i	$⊢ I = Itv (G)$
	tgbtwncgr.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgbtwncgr.a	$⊢ φ \to A \in P$
	tgbtwncgr.b	$⊢ φ \to B \in P$
	tgbtwncgr.c	$⊢ φ \to C \in P$
	tgbtwncgr.d	$⊢ φ \to D \in P$
	tgifscgr.e	$⊢ φ \to E \in P$
	tgifscgr.f	$⊢ φ \to F \in P$
	tgifscgr.g	$⊢ φ \to K \in P$
	tgifscgr.h	$⊢ φ \to H \in P$
	tgifscgr.1	$⊢ φ \to B \in (A I C)$
	tgifscgr.2	$⊢ φ \to F \in (E I K)$
	tgifscgr.3	$⊢ φ \to A \underset{˙}{-} C = E \underset{˙}{-} K$
	tgifscgr.4	$⊢ φ \to B \underset{˙}{-} C = F \underset{˙}{-} K$
	tgifscgr.5	$⊢ φ \to A \underset{˙}{-} D = E \underset{˙}{-} H$
	tgifscgr.6	$⊢ φ \to C \underset{˙}{-} D = K \underset{˙}{-} H$
Assertion	tgifscgr	$⊢ φ \to B \underset{˙}{-} D = F \underset{˙}{-} H$

Proof

Step	Hyp	Ref	Expression
1		tgbtwncgr.p	$⊢ P = {Base}_{G}$
2		tgbtwncgr.m	$⊢ \underset{˙}{-} = dist (G)$
3		tgbtwncgr.i	$⊢ I = Itv (G)$
4		tgbtwncgr.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tgbtwncgr.a	$⊢ φ \to A \in P$
6		tgbtwncgr.b	$⊢ φ \to B \in P$
7		tgbtwncgr.c	$⊢ φ \to C \in P$
8		tgbtwncgr.d	$⊢ φ \to D \in P$
9		tgifscgr.e	$⊢ φ \to E \in P$
10		tgifscgr.f	$⊢ φ \to F \in P$
11		tgifscgr.g	$⊢ φ \to K \in P$
12		tgifscgr.h	$⊢ φ \to H \in P$
13		tgifscgr.1	$⊢ φ \to B \in (A I C)$
14		tgifscgr.2	$⊢ φ \to F \in (E I K)$
15		tgifscgr.3	$⊢ φ \to A \underset{˙}{-} C = E \underset{˙}{-} K$
16		tgifscgr.4	$⊢ φ \to B \underset{˙}{-} C = F \underset{˙}{-} K$
17		tgifscgr.5	$⊢ φ \to A \underset{˙}{-} D = E \underset{˙}{-} H$
18		tgifscgr.6	$⊢ φ \to C \underset{˙}{-} D = K \underset{˙}{-} H$
19	4	adantr	$⊢ (φ \land \|P\| = 1) \to G \in 𝒢_{Tarski}$
20	6	adantr	$⊢ (φ \land \|P\| = 1) \to B \in P$
21	8	adantr	$⊢ (φ \land \|P\| = 1) \to D \in P$
22	10	adantr	$⊢ (φ \land \|P\| = 1) \to F \in P$
23		simpr	$⊢ (φ \land \|P\| = 1) \to \|P\| = 1$
24	12	adantr	$⊢ (φ \land \|P\| = 1) \to H \in P$
25	1 2 3 19 20 21 22 23 24	tgldim0cgr	$⊢ (φ \land \|P\| = 1) \to B \underset{˙}{-} D = F \underset{˙}{-} H$
26	18	ad2antrr	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to C \underset{˙}{-} D = K \underset{˙}{-} H$
27	4	ad2antrr	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to G \in 𝒢_{Tarski}$
28	7	ad2antrr	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to C \in P$
29	6	ad2antrr	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to B \in P$
30	13	ad2antrr	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to B \in (A I C)$
31		simpr	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to A = C$
32	31	oveq1d	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to A I C = C I C$
33	30 32	eleqtrd	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to B \in (C I C)$
34	1 2 3 27 28 29 33	axtgbtwnid	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to C = B$
35	34	oveq1d	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to C \underset{˙}{-} D = B \underset{˙}{-} D$
36	11	ad2antrr	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to K \in P$
37	10	ad2antrr	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to F \in P$
38	14	ad2antrr	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to F \in (E I K)$
39	9	ad2antrr	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to E \in P$
40	5	ad2antrr	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to A \in P$
41	31	oveq2d	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to A \underset{˙}{-} A = A \underset{˙}{-} C$
42	15	ad2antrr	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to A \underset{˙}{-} C = E \underset{˙}{-} K$
43	41 42	eqtr2d	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to E \underset{˙}{-} K = A \underset{˙}{-} A$
44	1 2 3 27 39 36 40 43	axtgcgrid	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to E = K$
45	44	oveq1d	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to E I K = K I K$
46	38 45	eleqtrd	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to F \in (K I K)$
47	1 2 3 27 36 37 46	axtgbtwnid	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to K = F$
48	47	oveq1d	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to K \underset{˙}{-} H = F \underset{˙}{-} H$
49	26 35 48	3eqtr3d	$⊢ ((φ \land 2 \leq \|P\|) \land A = C) \to B \underset{˙}{-} D = F \underset{˙}{-} H$
50	4	ad2antrr	$⊢ ((φ \land 2 \leq \|P\|) \land A \neq C) \to G \in 𝒢_{Tarski}$
51	50	ad2antrr	$⊢ ((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \to G \in 𝒢_{Tarski}$
52	51	ad2antrr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to G \in 𝒢_{Tarski}$
53		simp-4r	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to e \in P$
54	7	ad2antrr	$⊢ ((φ \land 2 \leq \|P\|) \land A \neq C) \to C \in P$
55	54	ad2antrr	$⊢ ((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \to C \in P$
56	55	ad2antrr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to C \in P$
57	6	ad6antr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to B \in P$
58		simplr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to f \in P$
59	11	ad4antr	$⊢ ((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \to K \in P$
60	59	ad2antrr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to K \in P$
61	10	ad6antr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to F \in P$
62	8	ad6antr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to D \in P$
63	12	ad6antr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to H \in P$
64		simpllr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to (C \in (A I e) \land C \neq e)$
65	64	simprd	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to C \neq e$
66	65	necomd	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to e \neq C$
67	5	ad2antrr	$⊢ ((φ \land 2 \leq \|P\|) \land A \neq C) \to A \in P$
68	67	ad4antr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to A \in P$
69	13	ad6antr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to B \in (A I C)$
70	64	simpld	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to C \in (A I e)$
71	1 2 3 52 68 57 56 53 69 70	tgbtwnexch3	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to C \in (B I e)$
72	1 2 3 52 57 56 53 71	tgbtwncom	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to C \in (e I B)$
73	9	ad6antr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to E \in P$
74	14	ad6antr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to F \in (E I K)$
75		simprl	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to K \in (E I f)$
76	1 2 3 52 73 61 60 58 74 75	tgbtwnexch3	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to K \in (F I f)$
77	1 2 3 52 61 60 58 76	tgbtwncom	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to K \in (f I F)$
78		simprr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to K \underset{˙}{-} f = C \underset{˙}{-} e$
79	78	eqcomd	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to C \underset{˙}{-} e = K \underset{˙}{-} f$
80	1 2 3 52 56 53 60 58 79	tgcgrcomlr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to e \underset{˙}{-} C = f \underset{˙}{-} K$
81	16	ad6antr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to B \underset{˙}{-} C = F \underset{˙}{-} K$
82	1 2 3 52 57 56 61 60 81	tgcgrcomlr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to C \underset{˙}{-} B = K \underset{˙}{-} F$
83		simp-5r	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to A \neq C$
84	15	ad6antr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to A \underset{˙}{-} C = E \underset{˙}{-} K$
85	17	ad6antr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to A \underset{˙}{-} D = E \underset{˙}{-} H$
86	18	ad6antr	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to C \underset{˙}{-} D = K \underset{˙}{-} H$
87	1 2 3 52 68 56 53 73 60 58 62 63 83 70 75 84 79 85 86	axtg5seg	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to e \underset{˙}{-} D = f \underset{˙}{-} H$
88	1 2 3 52 53 56 57 58 60 61 62 63 66 72 77 80 82 87 86	axtg5seg	$⊢ ((((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \land f \in P) \land (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)) \to B \underset{˙}{-} D = F \underset{˙}{-} H$
89	9	ad4antr	$⊢ ((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \to E \in P$
90		simplr	$⊢ ((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \to e \in P$
91	1 2 3 51 89 59 55 90	axtgsegcon	$⊢ ((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \to \exists f \in P (K \in (E I f) \land K \underset{˙}{-} f = C \underset{˙}{-} e)$
92	88 91	r19.29a	$⊢ ((((φ \land 2 \leq \|P\|) \land A \neq C) \land e \in P) \land (C \in (A I e) \land C \neq e)) \to B \underset{˙}{-} D = F \underset{˙}{-} H$
93		simplr	$⊢ ((φ \land 2 \leq \|P\|) \land A \neq C) \to 2 \leq \|P\|$
94	1 2 3 50 67 54 93	tgbtwndiff	$⊢ ((φ \land 2 \leq \|P\|) \land A \neq C) \to \exists e \in P (C \in (A I e) \land C \neq e)$
95	92 94	r19.29a	$⊢ ((φ \land 2 \leq \|P\|) \land A \neq C) \to B \underset{˙}{-} D = F \underset{˙}{-} H$
96	49 95	pm2.61dane	$⊢ (φ \land 2 \leq \|P\|) \to B \underset{˙}{-} D = F \underset{˙}{-} H$
97	1 5	tgldimor	$⊢ φ \to (\|P\| = 1 \lor 2 \leq \|P\|)$
98	25 96 97	mpjaodan	$⊢ φ \to B \underset{˙}{-} D = F \underset{˙}{-} H$

Metamath Proof Explorer

Theorem tgifscgr

Proof