cgrg3col4

Description: Lemma 11.28 of Schwabhauser p. 102. Extend a congruence of three points with a fourth colinear point. (Contributed by Thierry Arnoux, 8-Oct-2020)

	Ref	Expression
Hypotheses	isleag.p	$⊢ P = {Base}_{G}$
	isleag.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	isleag.a	$⊢ φ \to A \in P$
	isleag.b	$⊢ φ \to B \in P$
	isleag.c	$⊢ φ \to C \in P$
	isleag.d	$⊢ φ \to D \in P$
	isleag.e	$⊢ φ \to E \in P$
	isleag.f	$⊢ φ \to F \in P$
	cgrg3col4.l	$⊢ L = {Line}_{𝒢} (G)$
	cgrg3col4.x	$⊢ φ \to X \in P$
	cgrg3col4.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E F ”⟩$
	cgrg3col4.2	$⊢ φ \to (X \in (A L C) \lor A = C)$
Assertion	cgrg3col4	$⊢ φ \to \exists y \in P ⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩$

Proof

Step	Hyp	Ref	Expression
1		isleag.p	$⊢ P = {Base}_{G}$
2		isleag.g	$⊢ φ \to G \in 𝒢_{Tarski}$
3		isleag.a	$⊢ φ \to A \in P$
4		isleag.b	$⊢ φ \to B \in P$
5		isleag.c	$⊢ φ \to C \in P$
6		isleag.d	$⊢ φ \to D \in P$
7		isleag.e	$⊢ φ \to E \in P$
8		isleag.f	$⊢ φ \to F \in P$
9		cgrg3col4.l	$⊢ L = {Line}_{𝒢} (G)$
10		cgrg3col4.x	$⊢ φ \to X \in P$
11		cgrg3col4.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E F ”⟩$
12		cgrg3col4.2	$⊢ φ \to (X \in (A L C) \lor A = C)$
13		eqid	$⊢ Itv (G) = Itv (G)$
14	2	ad2antrr	$⊢ ((φ \land A = C) \land (B \in (A L X) \lor A = X)) \to G \in 𝒢_{Tarski}$
15	3	ad2antrr	$⊢ ((φ \land A = C) \land (B \in (A L X) \lor A = X)) \to A \in P$
16	4	ad2antrr	$⊢ ((φ \land A = C) \land (B \in (A L X) \lor A = X)) \to B \in P$
17	10	ad2antrr	$⊢ ((φ \land A = C) \land (B \in (A L X) \lor A = X)) \to X \in P$
18		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
19	6	ad2antrr	$⊢ ((φ \land A = C) \land (B \in (A L X) \lor A = X)) \to D \in P$
20	7	ad2antrr	$⊢ ((φ \land A = C) \land (B \in (A L X) \lor A = X)) \to E \in P$
21		eqid	$⊢ dist (G) = dist (G)$
22		simpr	$⊢ ((φ \land A = C) \land (B \in (A L X) \lor A = X)) \to (B \in (A L X) \lor A = X)$
23	1 21 13 18 2 3 4 5 6 7 8 11	cgr3simp1	$⊢ φ \to A dist (G) B = D dist (G) E$
24	23	ad2antrr	$⊢ ((φ \land A = C) \land (B \in (A L X) \lor A = X)) \to A dist (G) B = D dist (G) E$
25	1 9 13 14 15 16 17 18 19 20 21 22 24	lnext	$⊢ ((φ \land A = C) \land (B \in (A L X) \lor A = X)) \to \exists y \in P ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩$
26	11	ad4antr	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E F ”⟩$
27	14	ad2antrr	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to G \in 𝒢_{Tarski}$
28	17	ad2antrr	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to X \in P$
29	15	ad2antrr	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to A \in P$
30		simplr	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to y \in P$
31	19	ad2antrr	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to D \in P$
32	16	ad2antrr	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to B \in P$
33	20	ad2antrr	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to E \in P$
34		simpr	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩$
35	1 21 13 18 27 29 32 28 31 33 30 34	cgr3simp3	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to X dist (G) A = y dist (G) D$
36	1 21 13 27 28 29 30 31 35	tgcgrcomlr	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to A dist (G) X = D dist (G) y$
37	1 21 13 18 27 29 32 28 31 33 30 34	cgr3simp2	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to B dist (G) X = E dist (G) y$
38	5	ad4antr	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to C \in P$
39	8	ad4antr	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to F \in P$
40		simpr	$⊢ (φ \land A = C) \to A = C$
41	40	ad3antrrr	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to A = C$
42	41	oveq2d	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to X dist (G) A = X dist (G) C$
43	2	adantr	$⊢ (φ \land A = C) \to G \in 𝒢_{Tarski}$
44	3	adantr	$⊢ (φ \land A = C) \to A \in P$
45	5	adantr	$⊢ (φ \land A = C) \to C \in P$
46	6	adantr	$⊢ (φ \land A = C) \to D \in P$
47	8	adantr	$⊢ (φ \land A = C) \to F \in P$
48	1 21 13 18 2 3 4 5 6 7 8 11	cgr3simp3	$⊢ φ \to C dist (G) A = F dist (G) D$
49	1 21 13 2 5 3 8 6 48	tgcgrcomlr	$⊢ φ \to A dist (G) C = D dist (G) F$
50	49	adantr	$⊢ (φ \land A = C) \to A dist (G) C = D dist (G) F$
51	1 21 13 43 44 45 46 47 50 40	tgcgreq	$⊢ (φ \land A = C) \to D = F$
52	51	ad3antrrr	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to D = F$
53	52	oveq2d	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to y dist (G) D = y dist (G) F$
54	35 42 53	3eqtr3d	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to X dist (G) C = y dist (G) F$
55	1 21 13 27 28 38 30 39 54	tgcgrcomlr	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to C dist (G) X = F dist (G) y$
56	36 37 55	3jca	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to (A dist (G) X = D dist (G) y \land B dist (G) X = E dist (G) y \land C dist (G) X = F dist (G) y)$
57	1 21 13 18 27 29 32 38 28 31 33 39 30	tgcgr4	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to (⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩ \leftrightarrow (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E F ”⟩ \land (A dist (G) X = D dist (G) y \land B dist (G) X = E dist (G) y \land C dist (G) X = F dist (G) y)))$
58	26 56 57	mpbir2and	$⊢ ((((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \land ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩) \to ⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩$
59	58	ex	$⊢ (((φ \land A = C) \land (B \in (A L X) \lor A = X)) \land y \in P) \to (⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩ \to ⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩)$
60	59	reximdva	$⊢ ((φ \land A = C) \land (B \in (A L X) \lor A = X)) \to (\exists y \in P ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ D E y ”⟩ \to \exists y \in P ⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩)$
61	25 60	mpd	$⊢ ((φ \land A = C) \land (B \in (A L X) \lor A = X)) \to \exists y \in P ⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩$
62		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
63	2	ad2antrr	$⊢ ((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \to G \in 𝒢_{Tarski}$
64	63	ad2antrr	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to G \in 𝒢_{Tarski}$
65	4	ad2antrr	$⊢ ((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \to B \in P$
66	65	ad2antrr	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to B \in P$
67	3	ad2antrr	$⊢ ((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \to A \in P$
68	67	ad2antrr	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to A \in P$
69	10	ad2antrr	$⊢ ((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \to X \in P$
70	69	ad2antrr	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to X \in P$
71	7	ad2antrr	$⊢ ((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \to E \in P$
72	71	ad2antrr	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to E \in P$
73	6	ad2antrr	$⊢ ((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \to D \in P$
74	73	ad2antrr	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to D \in P$
75		simplr	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to x \in P$
76		simpllr	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to \neg (B \in (A L X) \lor A = X)$
77		simpr	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to \neg x \in (D L E)$
78	23	ad2antrr	$⊢ ((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \to A dist (G) B = D dist (G) E$
79		simpr	$⊢ ((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \to \neg (B \in (A L X) \lor A = X)$
80	1 13 9 63 65 67 69 79	ncolne1	$⊢ ((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \to B \neq A$
81	80	necomd	$⊢ ((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \to A \neq B$
82	1 21 13 63 67 65 73 71 78 81	tgcgrneq	$⊢ ((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \to D \neq E$
83	82	ad2antrr	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to D \neq E$
84	83	neneqd	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to \neg D = E$
85		ioran	$⊢ \neg (x \in (D L E) \lor D = E) \leftrightarrow (\neg x \in (D L E) \land \neg D = E)$
86	77 84 85	sylanbrc	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to \neg (x \in (D L E) \lor D = E)$
87	1 9 13 64 74 72 75 86	ncolcom	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to \neg (x \in (E L D) \lor E = D)$
88	1 9 13 64 72 74 75 87	ncolrot1	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to \neg (E \in (D L x) \lor D = x)$
89	1 21 13 2 3 4 6 7 23	tgcgrcomlr	$⊢ φ \to B dist (G) A = E dist (G) D$
90	89	ad4antr	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to B dist (G) A = E dist (G) D$
91	1 21 13 9 62 64 66 68 70 72 74 75 76 88 90	trgcopy	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to \exists y \in P (⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩ \land y {hp}_{𝒢} (G) (E L D) x)$
92	11	ad6antr	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E F ”⟩$
93	64	ad2antrr	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to G \in 𝒢_{Tarski}$
94	66	ad2antrr	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to B \in P$
95	68	ad2antrr	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to A \in P$
96	70	ad2antrr	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to X \in P$
97	72	ad2antrr	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to E \in P$
98	74	ad2antrr	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to D \in P$
99		simplr	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to y \in P$
100		simpr	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩$
101	1 21 13 18 93 94 95 96 97 98 99 100	cgr3simp2	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to A dist (G) X = D dist (G) y$
102	1 21 13 18 93 94 95 96 97 98 99 100	cgr3simp3	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to X dist (G) B = y dist (G) E$
103	1 21 13 93 96 94 99 97 102	tgcgrcomlr	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to B dist (G) X = E dist (G) y$
104	45	ad5antr	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to C \in P$
105	47	ad5antr	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to F \in P$
106	1 21 13 93 95 96 98 99 101	tgcgrcomlr	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to X dist (G) A = y dist (G) D$
107		simp-6r	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to A = C$
108	107	oveq2d	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to X dist (G) A = X dist (G) C$
109	51	ad5antr	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to D = F$
110	109	oveq2d	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to y dist (G) D = y dist (G) F$
111	106 108 110	3eqtr3d	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to X dist (G) C = y dist (G) F$
112	1 21 13 93 96 104 99 105 111	tgcgrcomlr	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to C dist (G) X = F dist (G) y$
113	101 103 112	3jca	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to (A dist (G) X = D dist (G) y \land B dist (G) X = E dist (G) y \land C dist (G) X = F dist (G) y)$
114	1 21 13 18 93 95 94 104 96 98 97 105 99	tgcgr4	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to (⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩ \leftrightarrow (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E F ”⟩ \land (A dist (G) X = D dist (G) y \land B dist (G) X = E dist (G) y \land C dist (G) X = F dist (G) y)))$
115	92 113 114	mpbir2and	$⊢ ((((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \land ⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩) \to ⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩$
116	115	ex	$⊢ (((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \to (⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩ \to ⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩)$
117	116	adantrd	$⊢ (((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \land y \in P) \to ((⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩ \land y {hp}_{𝒢} (G) (E L D) x) \to ⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩)$
118	117	reximdva	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to (\exists y \in P (⟨“ B A X ”⟩ \sim_{𝒢} (G) ⟨“ E D y ”⟩ \land y {hp}_{𝒢} (G) (E L D) x) \to \exists y \in P ⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩)$
119	91 118	mpd	$⊢ ((((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \land x \in P) \land \neg x \in (D L E)) \to \exists y \in P ⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩$
120	1 9 13 63 67 69 65 79	ncoltgdim2	$⊢ ((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \to G {Dim}_{𝒢} \geq 2$
121	1 13 9 63 120 73 71 82	tglowdim2ln	$⊢ ((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \to \exists x \in P \neg x \in (D L E)$
122	119 121	r19.29a	$⊢ ((φ \land A = C) \land \neg (B \in (A L X) \lor A = X)) \to \exists y \in P ⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩$
123	61 122	pm2.61dan	$⊢ (φ \land A = C) \to \exists y \in P ⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩$
124	1 9 13 2 3 5 10 12	colcom	$⊢ φ \to (X \in (C L A) \lor C = A)$
125	1 9 13 2 5 3 10 124	colrot1	$⊢ φ \to (C \in (A L X) \lor A = X)$
126	1 9 13 2 3 5 10 18 6 8 21 125 49	lnext	$⊢ φ \to \exists y \in P ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩$
127	126	adantr	$⊢ (φ \land A \neq C) \to \exists y \in P ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩$
128	11	ad3antrrr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E F ”⟩$
129	2	ad3antrrr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to G \in 𝒢_{Tarski}$
130	10	ad3antrrr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to X \in P$
131	3	ad3antrrr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to A \in P$
132		simplr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to y \in P$
133	6	ad3antrrr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to D \in P$
134	5	ad3antrrr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to C \in P$
135	8	ad3antrrr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to F \in P$
136		simpr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩$
137	1 21 13 18 129 131 134 130 133 135 132 136	cgr3simp3	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to X dist (G) A = y dist (G) D$
138	1 21 13 129 130 131 132 133 137	tgcgrcomlr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to A dist (G) X = D dist (G) y$
139	4	ad3antrrr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to B \in P$
140	7	ad3antrrr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to E \in P$
141	125	ad3antrrr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to (C \in (A L X) \lor A = X)$
142	23	ad3antrrr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to A dist (G) B = D dist (G) E$
143	1 21 13 18 2 3 4 5 6 7 8 11	cgr3simp2	$⊢ φ \to B dist (G) C = E dist (G) F$
144	1 21 13 2 4 5 7 8 143	tgcgrcomlr	$⊢ φ \to C dist (G) B = F dist (G) E$
145	144	ad3antrrr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to C dist (G) B = F dist (G) E$
146		simpllr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to A \neq C$
147	1 9 13 129 131 134 130 18 133 135 21 139 132 140 141 136 142 145 146	tgfscgr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to X dist (G) B = y dist (G) E$
148	1 21 13 129 130 139 132 140 147	tgcgrcomlr	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to B dist (G) X = E dist (G) y$
149	1 21 13 18 129 131 134 130 133 135 132 136	cgr3simp2	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to C dist (G) X = F dist (G) y$
150	138 148 149	3jca	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to (A dist (G) X = D dist (G) y \land B dist (G) X = E dist (G) y \land C dist (G) X = F dist (G) y)$
151	1 21 13 18 129 131 139 134 130 133 140 135 132	tgcgr4	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to (⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩ \leftrightarrow (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E F ”⟩ \land (A dist (G) X = D dist (G) y \land B dist (G) X = E dist (G) y \land C dist (G) X = F dist (G) y)))$
152	128 150 151	mpbir2and	$⊢ (((φ \land A \neq C) \land y \in P) \land ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩) \to ⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩$
153	152	ex	$⊢ ((φ \land A \neq C) \land y \in P) \to (⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩ \to ⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩)$
154	153	reximdva	$⊢ (φ \land A \neq C) \to (\exists y \in P ⟨“ A C X ”⟩ \sim_{𝒢} (G) ⟨“ D F y ”⟩ \to \exists y \in P ⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩)$
155	127 154	mpd	$⊢ (φ \land A \neq C) \to \exists y \in P ⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩$
156	123 155	pm2.61dane	$⊢ φ \to \exists y \in P ⟨“ A B C X ”⟩ \sim_{𝒢} (G) ⟨“ D E F y ”⟩$

Metamath Proof Explorer

Theorem cgrg3col4

Proof