cgratr

Description: Angle congruence is transitive. Theorem 11.8 of Schwabhauser p. 97. (Contributed by Thierry Arnoux, 5-Mar-2020)

	Ref	Expression
Hypotheses	cgraid.p	$⊢ P = {Base}_{G}$
	cgraid.i	$⊢ I = Itv (G)$
	cgraid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	cgraid.k	$⊢ K = {hl}_{𝒢} (G)$
	cgraid.a	$⊢ φ \to A \in P$
	cgraid.b	$⊢ φ \to B \in P$
	cgraid.c	$⊢ φ \to C \in P$
	cgracom.d	$⊢ φ \to D \in P$
	cgracom.e	$⊢ φ \to E \in P$
	cgracom.f	$⊢ φ \to F \in P$
	cgracom.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
	cgratr.h	$⊢ φ \to H \in P$
	cgratr.i	$⊢ φ \to U \in P$
	cgratr.j	$⊢ φ \to J \in P$
	cgratr.1	$⊢ φ \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ H U J ”⟩$
Assertion	cgratr	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ H U J ”⟩$

Proof

Step	Hyp	Ref	Expression
1		cgraid.p	$⊢ P = {Base}_{G}$
2		cgraid.i	$⊢ I = Itv (G)$
3		cgraid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
4		cgraid.k	$⊢ K = {hl}_{𝒢} (G)$
5		cgraid.a	$⊢ φ \to A \in P$
6		cgraid.b	$⊢ φ \to B \in P$
7		cgraid.c	$⊢ φ \to C \in P$
8		cgracom.d	$⊢ φ \to D \in P$
9		cgracom.e	$⊢ φ \to E \in P$
10		cgracom.f	$⊢ φ \to F \in P$
11		cgracom.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
12		cgratr.h	$⊢ φ \to H \in P$
13		cgratr.i	$⊢ φ \to U \in P$
14		cgratr.j	$⊢ φ \to J \in P$
15		cgratr.1	$⊢ φ \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ H U J ”⟩$
16		eqid	$⊢ dist (G) = dist (G)$
17		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
18	3	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to G \in 𝒢_{Tarski}$
19	5	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to A \in P$
20	6	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to B \in P$
21	7	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to C \in P$
22		simpllr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to x \in P$
23	13	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to U \in P$
24		simplr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to y \in P$
25		simprlr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to U dist (G) x = B dist (G) A$
26	25	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to B dist (G) A = U dist (G) x$
27	1 16 2 18 20 19 23 22 26	tgcgrcomlr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to A dist (G) B = x dist (G) U$
28		simprrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to U dist (G) y = B dist (G) C$
29	28	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to B dist (G) C = U dist (G) y$
30	18	ad3antrrr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to G \in 𝒢_{Tarski}$
31	19	ad3antrrr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to A \in P$
32	20	ad3antrrr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to B \in P$
33	21	ad3antrrr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to C \in P$
34		simpllr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to u \in P$
35	9	ad6antr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to E \in P$
36		simplr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to v \in P$
37		simpr1	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩$
38	1 16 2 17 30 31 32 33 34 35 36 37	cgr3simp3	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to C dist (G) A = v dist (G) u$
39	22	ad3antrrr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to x \in P$
40	24	ad3antrrr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to y \in P$
41	8	ad6antr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to D \in P$
42	10	ad6antr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to F \in P$
43	23	ad3antrrr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to U \in P$
44	14	ad6antr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to J \in P$
45	12	ad6antr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to H \in P$
46	15	ad6antr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ H U J ”⟩$
47		simprll	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to x K (U) H$
48	47	ad3antrrr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to x K (U) H$
49	1 2 4 30 41 35 42 45 43 44 46 39 48	cgrahl1	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ x U J ”⟩$
50		simprrl	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to y K (U) J$
51	50	ad3antrrr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to y K (U) J$
52	1 2 4 30 41 35 42 39 43 44 49 40 51	cgrahl2	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ x U y ”⟩$
53		simpr2	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to u K (E) D$
54		simpr3	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to v K (E) F$
55	1 16 2 17 30 31 32 33 34 35 36 37	cgr3simp1	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to A dist (G) B = u dist (G) E$
56	55	eqcomd	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to u dist (G) E = A dist (G) B$
57	1 16 2 30 34 35 31 32 56	tgcgrcomlr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to E dist (G) u = B dist (G) A$
58	26	ad3antrrr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to B dist (G) A = U dist (G) x$
59	57 58	eqtrd	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to E dist (G) u = U dist (G) x$
60	1 16 2 17 30 31 32 33 34 35 36 37	cgr3simp2	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to B dist (G) C = E dist (G) v$
61	29	ad3antrrr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to B dist (G) C = U dist (G) y$
62	60 61	eqtr3d	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to E dist (G) v = U dist (G) y$
63	1 2 4 30 41 35 42 39 43 40 52 34 16 36 53 54 59 62	cgracgr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to u dist (G) v = x dist (G) y$
64	1 16 2 30 34 36 39 40 63	tgcgrcomlr	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to v dist (G) u = y dist (G) x$
65	38 64	eqtrd	$⊢ ((((((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \land u \in P) \land v \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)) \to C dist (G) A = y dist (G) x$
66	1 2 4 3 5 6 7 8 9 10	iscgra	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow \exists u \in P \exists v \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F))$
67	11 66	mpbid	$⊢ φ \to \exists u \in P \exists v \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)$
68	67	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to \exists u \in P \exists v \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ u E v ”⟩ \land u K (E) D \land v K (E) F)$
69	65 68	r19.29vva	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to C dist (G) A = y dist (G) x$
70	1 16 17 18 19 20 21 22 23 24 27 29 69	trgcgr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x U y ”⟩$
71	70 47 50	3jca	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))) \to (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x U y ”⟩ \land x K (U) H \land y K (U) J)$
72	1 2 4 3 8 9 10 12 13 14 15	cgrane3	$⊢ φ \to U \neq H$
73	72	necomd	$⊢ φ \to H \neq U$
74	1 2 4 3 5 6 7 8 9 10 11	cgrane1	$⊢ φ \to A \neq B$
75	74	necomd	$⊢ φ \to B \neq A$
76	1 2 4 13 6 5 3 12 16 73 75	hlcgrex	$⊢ φ \to \exists x \in P (x K (U) H \land U dist (G) x = B dist (G) A)$
77	1 2 4 3 8 9 10 12 13 14 15	cgrane4	$⊢ φ \to U \neq J$
78	77	necomd	$⊢ φ \to J \neq U$
79	1 2 4 3 5 6 7 8 9 10 11	cgrane2	$⊢ φ \to B \neq C$
80	1 2 4 13 6 7 3 14 16 78 79	hlcgrex	$⊢ φ \to \exists y \in P (y K (U) J \land U dist (G) y = B dist (G) C)$
81		reeanv	$⊢ \exists x \in P \exists y \in P ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C)) \leftrightarrow (\exists x \in P (x K (U) H \land U dist (G) x = B dist (G) A) \land \exists y \in P (y K (U) J \land U dist (G) y = B dist (G) C))$
82	76 80 81	sylanbrc	$⊢ φ \to \exists x \in P \exists y \in P ((x K (U) H \land U dist (G) x = B dist (G) A) \land (y K (U) J \land U dist (G) y = B dist (G) C))$
83	71 82	reximddv2	$⊢ φ \to \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x U y ”⟩ \land x K (U) H \land y K (U) J)$
84	1 2 4 3 5 6 7 12 13 14	iscgra	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ H U J ”⟩ \leftrightarrow \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x U y ”⟩ \land x K (U) H \land y K (U) J))$
85	83 84	mpbird	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ H U J ”⟩$

Metamath Proof Explorer

Theorem cgratr

Proof