tgcgrsub2

Description: Removing identical parts from the end of a line segment preserves congruence. In this version the order of points is not known. (Contributed by Thierry Arnoux, 3-Apr-2019)

	Ref	Expression
Hypotheses	legval.p	$⊢ P = {Base}_{G}$
	legval.d	$⊢ \underset{˙}{-} = dist (G)$
	legval.i	$⊢ I = Itv (G)$
	legval.l	$⊢ \underset{˙}{\leq} = \leq_{𝒢} (G)$
	legval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	legid.a	$⊢ φ \to A \in P$
	legid.b	$⊢ φ \to B \in P$
	legtrd.c	$⊢ φ \to C \in P$
	legtrd.d	$⊢ φ \to D \in P$
	tgcgrsub2.d	$⊢ φ \to D \in P$
	tgcgrsub2.e	$⊢ φ \to E \in P$
	tgcgrsub2.f	$⊢ φ \to F \in P$
	tgcgrsub2.1	$⊢ φ \to (B \in (A I C) \lor C \in (A I B))$
	tgcgrsub2.2	$⊢ φ \to (E \in (D I F) \lor F \in (D I E))$
	tgcgrsub2.3	$⊢ φ \to A \underset{˙}{-} B = D \underset{˙}{-} E$
	tgcgrsub2.4	$⊢ φ \to A \underset{˙}{-} C = D \underset{˙}{-} F$
Assertion	tgcgrsub2	$⊢ φ \to B \underset{˙}{-} C = E \underset{˙}{-} F$

Proof

Step	Hyp	Ref	Expression
1		legval.p	$⊢ P = {Base}_{G}$
2		legval.d	$⊢ \underset{˙}{-} = dist (G)$
3		legval.i	$⊢ I = Itv (G)$
4		legval.l	$⊢ \underset{˙}{\leq} = \leq_{𝒢} (G)$
5		legval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		legid.a	$⊢ φ \to A \in P$
7		legid.b	$⊢ φ \to B \in P$
8		legtrd.c	$⊢ φ \to C \in P$
9		legtrd.d	$⊢ φ \to D \in P$
10		tgcgrsub2.d	$⊢ φ \to D \in P$
11		tgcgrsub2.e	$⊢ φ \to E \in P$
12		tgcgrsub2.f	$⊢ φ \to F \in P$
13		tgcgrsub2.1	$⊢ φ \to (B \in (A I C) \lor C \in (A I B))$
14		tgcgrsub2.2	$⊢ φ \to (E \in (D I F) \lor F \in (D I E))$
15		tgcgrsub2.3	$⊢ φ \to A \underset{˙}{-} B = D \underset{˙}{-} E$
16		tgcgrsub2.4	$⊢ φ \to A \underset{˙}{-} C = D \underset{˙}{-} F$
17	5	adantr	$⊢ (φ \land B \in (A I C)) \to G \in 𝒢_{Tarski}$
18	8	adantr	$⊢ (φ \land B \in (A I C)) \to C \in P$
19	7	adantr	$⊢ (φ \land B \in (A I C)) \to B \in P$
20	12	adantr	$⊢ (φ \land B \in (A I C)) \to F \in P$
21	11	adantr	$⊢ (φ \land B \in (A I C)) \to E \in P$
22	6	adantr	$⊢ (φ \land B \in (A I C)) \to A \in P$
23	9	adantr	$⊢ (φ \land B \in (A I C)) \to D \in P$
24		simpr	$⊢ (φ \land B \in (A I C)) \to B \in (A I C)$
25	1 2 3 17 22 19 18 24	tgbtwncom	$⊢ (φ \land B \in (A I C)) \to B \in (C I A)$
26	14	adantr	$⊢ (φ \land B \in (A I C)) \to (E \in (D I F) \lor F \in (D I E))$
27	1 2 3 4 17 22 19 18 24	btwnleg	$⊢ (φ \land B \in (A I C)) \to (A \underset{˙}{-} B) \underset{˙}{\leq} (A \underset{˙}{-} C)$
28	15	adantr	$⊢ (φ \land B \in (A I C)) \to A \underset{˙}{-} B = D \underset{˙}{-} E$
29	16	adantr	$⊢ (φ \land B \in (A I C)) \to A \underset{˙}{-} C = D \underset{˙}{-} F$
30	27 28 29	3brtr3d	$⊢ (φ \land B \in (A I C)) \to (D \underset{˙}{-} E) \underset{˙}{\leq} (D \underset{˙}{-} F)$
31	1 2 3 4 17 21 20 23 23 26 30	legbtwn	$⊢ (φ \land B \in (A I C)) \to E \in (D I F)$
32	1 2 3 17 23 21 20 31	tgbtwncom	$⊢ (φ \land B \in (A I C)) \to E \in (F I D)$
33	1 2 3 5 6 8 9 12 16	tgcgrcomlr	$⊢ φ \to C \underset{˙}{-} A = F \underset{˙}{-} D$
34	33	adantr	$⊢ (φ \land B \in (A I C)) \to C \underset{˙}{-} A = F \underset{˙}{-} D$
35	1 2 3 5 6 7 9 11 15	tgcgrcomlr	$⊢ φ \to B \underset{˙}{-} A = E \underset{˙}{-} D$
36	35	adantr	$⊢ (φ \land B \in (A I C)) \to B \underset{˙}{-} A = E \underset{˙}{-} D$
37	1 2 3 17 18 19 22 20 21 23 25 32 34 36	tgcgrsub	$⊢ (φ \land B \in (A I C)) \to C \underset{˙}{-} B = F \underset{˙}{-} E$
38	1 2 3 17 18 19 20 21 37	tgcgrcomlr	$⊢ (φ \land B \in (A I C)) \to B \underset{˙}{-} C = E \underset{˙}{-} F$
39	5	adantr	$⊢ (φ \land C \in (A I B)) \to G \in 𝒢_{Tarski}$
40	7	adantr	$⊢ (φ \land C \in (A I B)) \to B \in P$
41	8	adantr	$⊢ (φ \land C \in (A I B)) \to C \in P$
42	6	adantr	$⊢ (φ \land C \in (A I B)) \to A \in P$
43	11	adantr	$⊢ (φ \land C \in (A I B)) \to E \in P$
44	12	adantr	$⊢ (φ \land C \in (A I B)) \to F \in P$
45	9	adantr	$⊢ (φ \land C \in (A I B)) \to D \in P$
46		simpr	$⊢ (φ \land C \in (A I B)) \to C \in (A I B)$
47	1 2 3 39 42 41 40 46	tgbtwncom	$⊢ (φ \land C \in (A I B)) \to C \in (B I A)$
48	14	orcomd	$⊢ φ \to (F \in (D I E) \lor E \in (D I F))$
49	48	adantr	$⊢ (φ \land C \in (A I B)) \to (F \in (D I E) \lor E \in (D I F))$
50	1 2 3 4 39 42 41 40 46	btwnleg	$⊢ (φ \land C \in (A I B)) \to (A \underset{˙}{-} C) \underset{˙}{\leq} (A \underset{˙}{-} B)$
51	16	adantr	$⊢ (φ \land C \in (A I B)) \to A \underset{˙}{-} C = D \underset{˙}{-} F$
52	15	adantr	$⊢ (φ \land C \in (A I B)) \to A \underset{˙}{-} B = D \underset{˙}{-} E$
53	50 51 52	3brtr3d	$⊢ (φ \land C \in (A I B)) \to (D \underset{˙}{-} F) \underset{˙}{\leq} (D \underset{˙}{-} E)$
54	1 2 3 4 39 44 43 45 45 49 53	legbtwn	$⊢ (φ \land C \in (A I B)) \to F \in (D I E)$
55	1 2 3 39 45 44 43 54	tgbtwncom	$⊢ (φ \land C \in (A I B)) \to F \in (E I D)$
56	35	adantr	$⊢ (φ \land C \in (A I B)) \to B \underset{˙}{-} A = E \underset{˙}{-} D$
57	33	adantr	$⊢ (φ \land C \in (A I B)) \to C \underset{˙}{-} A = F \underset{˙}{-} D$
58	1 2 3 39 40 41 42 43 44 45 47 55 56 57	tgcgrsub	$⊢ (φ \land C \in (A I B)) \to B \underset{˙}{-} C = E \underset{˙}{-} F$
59	38 58 13	mpjaodan	$⊢ φ \to B \underset{˙}{-} C = E \underset{˙}{-} F$

Metamath Proof Explorer

Theorem tgcgrsub2

Proof