tgfscgr

Description: Congruence law for the general five segment configuration. Theorem 4.16 of Schwabhauser p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019)

	Ref	Expression
Hypotheses	tglngval.p	$⊢ P = {Base}_{G}$
	tglngval.l	$⊢ L = {Line}_{𝒢} (G)$
	tglngval.i	$⊢ I = Itv (G)$
	tglngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tglngval.x	$⊢ φ \to X \in P$
	tglngval.y	$⊢ φ \to Y \in P$
	tgcolg.z	$⊢ φ \to Z \in P$
	lnxfr.r	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
	lnxfr.a	$⊢ φ \to A \in P$
	lnxfr.b	$⊢ φ \to B \in P$
	lnxfr.d	$⊢ \underset{˙}{-} = dist (G)$
	tgfscgr.t	$⊢ φ \to T \in P$
	tgfscgr.c	$⊢ φ \to C \in P$
	tgfscgr.d	$⊢ φ \to D \in P$
	tgfscgr.1	$⊢ φ \to (Y \in (X L Z) \lor X = Z)$
	tgfscgr.2	$⊢ φ \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B C ”⟩$
	tgfscgr.3	$⊢ φ \to X \underset{˙}{-} T = A \underset{˙}{-} D$
	tgfscgr.4	$⊢ φ \to Y \underset{˙}{-} T = B \underset{˙}{-} D$
	tgfscgr.5	$⊢ φ \to X \neq Y$
Assertion	tgfscgr	$⊢ φ \to Z \underset{˙}{-} T = C \underset{˙}{-} D$

Proof

Step	Hyp	Ref	Expression
1		tglngval.p	$⊢ P = {Base}_{G}$
2		tglngval.l	$⊢ L = {Line}_{𝒢} (G)$
3		tglngval.i	$⊢ I = Itv (G)$
4		tglngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tglngval.x	$⊢ φ \to X \in P$
6		tglngval.y	$⊢ φ \to Y \in P$
7		tgcolg.z	$⊢ φ \to Z \in P$
8		lnxfr.r	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
9		lnxfr.a	$⊢ φ \to A \in P$
10		lnxfr.b	$⊢ φ \to B \in P$
11		lnxfr.d	$⊢ \underset{˙}{-} = dist (G)$
12		tgfscgr.t	$⊢ φ \to T \in P$
13		tgfscgr.c	$⊢ φ \to C \in P$
14		tgfscgr.d	$⊢ φ \to D \in P$
15		tgfscgr.1	$⊢ φ \to (Y \in (X L Z) \lor X = Z)$
16		tgfscgr.2	$⊢ φ \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B C ”⟩$
17		tgfscgr.3	$⊢ φ \to X \underset{˙}{-} T = A \underset{˙}{-} D$
18		tgfscgr.4	$⊢ φ \to Y \underset{˙}{-} T = B \underset{˙}{-} D$
19		tgfscgr.5	$⊢ φ \to X \neq Y$
20	4	adantr	$⊢ (φ \land Y \in (X I Z)) \to G \in 𝒢_{Tarski}$
21	5	adantr	$⊢ (φ \land Y \in (X I Z)) \to X \in P$
22	6	adantr	$⊢ (φ \land Y \in (X I Z)) \to Y \in P$
23	7	adantr	$⊢ (φ \land Y \in (X I Z)) \to Z \in P$
24	9	adantr	$⊢ (φ \land Y \in (X I Z)) \to A \in P$
25	10	adantr	$⊢ (φ \land Y \in (X I Z)) \to B \in P$
26	13	adantr	$⊢ (φ \land Y \in (X I Z)) \to C \in P$
27	12	adantr	$⊢ (φ \land Y \in (X I Z)) \to T \in P$
28	14	adantr	$⊢ (φ \land Y \in (X I Z)) \to D \in P$
29	19	adantr	$⊢ (φ \land Y \in (X I Z)) \to X \neq Y$
30		simpr	$⊢ (φ \land Y \in (X I Z)) \to Y \in (X I Z)$
31	16	adantr	$⊢ (φ \land Y \in (X I Z)) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B C ”⟩$
32	1 11 3 8 20 21 22 23 24 25 26 31 30	tgbtwnxfr	$⊢ (φ \land Y \in (X I Z)) \to B \in (A I C)$
33	1 11 3 8 20 21 22 23 24 25 26 31	cgr3simp1	$⊢ (φ \land Y \in (X I Z)) \to X \underset{˙}{-} Y = A \underset{˙}{-} B$
34	1 11 3 8 20 21 22 23 24 25 26 31	cgr3simp2	$⊢ (φ \land Y \in (X I Z)) \to Y \underset{˙}{-} Z = B \underset{˙}{-} C$
35	17	adantr	$⊢ (φ \land Y \in (X I Z)) \to X \underset{˙}{-} T = A \underset{˙}{-} D$
36	18	adantr	$⊢ (φ \land Y \in (X I Z)) \to Y \underset{˙}{-} T = B \underset{˙}{-} D$
37	1 11 3 20 21 22 23 24 25 26 27 28 29 30 32 33 34 35 36	axtg5seg	$⊢ (φ \land Y \in (X I Z)) \to Z \underset{˙}{-} T = C \underset{˙}{-} D$
38	4	adantr	$⊢ (φ \land X \in (Y I Z)) \to G \in 𝒢_{Tarski}$
39	6	adantr	$⊢ (φ \land X \in (Y I Z)) \to Y \in P$
40	5	adantr	$⊢ (φ \land X \in (Y I Z)) \to X \in P$
41	7	adantr	$⊢ (φ \land X \in (Y I Z)) \to Z \in P$
42	10	adantr	$⊢ (φ \land X \in (Y I Z)) \to B \in P$
43	9	adantr	$⊢ (φ \land X \in (Y I Z)) \to A \in P$
44	13	adantr	$⊢ (φ \land X \in (Y I Z)) \to C \in P$
45	12	adantr	$⊢ (φ \land X \in (Y I Z)) \to T \in P$
46	14	adantr	$⊢ (φ \land X \in (Y I Z)) \to D \in P$
47	19	necomd	$⊢ φ \to Y \neq X$
48	47	adantr	$⊢ (φ \land X \in (Y I Z)) \to Y \neq X$
49		simpr	$⊢ (φ \land X \in (Y I Z)) \to X \in (Y I Z)$
50	16	adantr	$⊢ (φ \land X \in (Y I Z)) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B C ”⟩$
51	1 11 3 8 38 40 39 41 43 42 44 50	cgr3swap12	$⊢ (φ \land X \in (Y I Z)) \to ⟨“ Y X Z ”⟩ \underset{˙}{\sim} ⟨“ B A C ”⟩$
52	1 11 3 8 38 39 40 41 42 43 44 51 49	tgbtwnxfr	$⊢ (φ \land X \in (Y I Z)) \to A \in (B I C)$
53	1 11 3 8 38 39 40 41 42 43 44 51	cgr3simp1	$⊢ (φ \land X \in (Y I Z)) \to Y \underset{˙}{-} X = B \underset{˙}{-} A$
54	1 11 3 8 38 39 40 41 42 43 44 51	cgr3simp2	$⊢ (φ \land X \in (Y I Z)) \to X \underset{˙}{-} Z = A \underset{˙}{-} C$
55	18	adantr	$⊢ (φ \land X \in (Y I Z)) \to Y \underset{˙}{-} T = B \underset{˙}{-} D$
56	17	adantr	$⊢ (φ \land X \in (Y I Z)) \to X \underset{˙}{-} T = A \underset{˙}{-} D$
57	1 11 3 38 39 40 41 42 43 44 45 46 48 49 52 53 54 55 56	axtg5seg	$⊢ (φ \land X \in (Y I Z)) \to Z \underset{˙}{-} T = C \underset{˙}{-} D$
58	4	adantr	$⊢ (φ \land Z \in (X I Y)) \to G \in 𝒢_{Tarski}$
59	5	adantr	$⊢ (φ \land Z \in (X I Y)) \to X \in P$
60	7	adantr	$⊢ (φ \land Z \in (X I Y)) \to Z \in P$
61	6	adantr	$⊢ (φ \land Z \in (X I Y)) \to Y \in P$
62	12	adantr	$⊢ (φ \land Z \in (X I Y)) \to T \in P$
63	9	adantr	$⊢ (φ \land Z \in (X I Y)) \to A \in P$
64	13	adantr	$⊢ (φ \land Z \in (X I Y)) \to C \in P$
65	10	adantr	$⊢ (φ \land Z \in (X I Y)) \to B \in P$
66	14	adantr	$⊢ (φ \land Z \in (X I Y)) \to D \in P$
67		simpr	$⊢ (φ \land Z \in (X I Y)) \to Z \in (X I Y)$
68	16	adantr	$⊢ (φ \land Z \in (X I Y)) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B C ”⟩$
69	1 11 3 8 58 59 61 60 63 65 64 68	cgr3swap23	$⊢ (φ \land Z \in (X I Y)) \to ⟨“ X Z Y ”⟩ \underset{˙}{\sim} ⟨“ A C B ”⟩$
70	1 11 3 8 58 59 60 61 63 64 65 69 67	tgbtwnxfr	$⊢ (φ \land Z \in (X I Y)) \to C \in (A I B)$
71	1 11 3 8 58 59 61 60 63 65 64 68	cgr3simp1	$⊢ (φ \land Z \in (X I Y)) \to X \underset{˙}{-} Y = A \underset{˙}{-} B$
72	1 11 3 8 58 59 60 61 63 64 65 69	cgr3simp2	$⊢ (φ \land Z \in (X I Y)) \to Z \underset{˙}{-} Y = C \underset{˙}{-} B$
73	17	adantr	$⊢ (φ \land Z \in (X I Y)) \to X \underset{˙}{-} T = A \underset{˙}{-} D$
74	18	adantr	$⊢ (φ \land Z \in (X I Y)) \to Y \underset{˙}{-} T = B \underset{˙}{-} D$
75	1 11 3 58 59 60 61 62 63 64 65 66 67 70 71 72 73 74	tgifscgr	$⊢ (φ \land Z \in (X I Y)) \to Z \underset{˙}{-} T = C \underset{˙}{-} D$
76	1 2 3 4 5 7 6	tgcolg	$⊢ φ \to ((Y \in (X L Z) \lor X = Z) \leftrightarrow (Y \in (X I Z) \lor X \in (Y I Z) \lor Z \in (X I Y)))$
77	15 76	mpbid	$⊢ φ \to (Y \in (X I Z) \lor X \in (Y I Z) \lor Z \in (X I Y))$
78	37 57 75 77	mpjao3dan	$⊢ φ \to Z \underset{˙}{-} T = C \underset{˙}{-} D$

Metamath Proof Explorer

Theorem tgfscgr

Proof