flatcgra

Description: Flat angles are congruent. (Contributed by Thierry Arnoux, 13-Feb-2023)

	Ref	Expression
Hypotheses	cgracol.p	$⊢ P = {Base}_{G}$
	cgracol.i	$⊢ I = Itv (G)$
	cgracol.m	$⊢ \underset{˙}{-} = dist (G)$
	cgracol.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	cgracol.a	$⊢ φ \to A \in P$
	cgracol.b	$⊢ φ \to B \in P$
	cgracol.c	$⊢ φ \to C \in P$
	cgracol.d	$⊢ φ \to D \in P$
	cgracol.e	$⊢ φ \to E \in P$
	cgracol.f	$⊢ φ \to F \in P$
	flatcgra.1	$⊢ φ \to B \in (A I C)$
	flatcgra.2	$⊢ φ \to E \in (D I F)$
	flatcgra.3	$⊢ φ \to A \neq B$
	flatcgra.4	$⊢ φ \to C \neq B$
	flatcgra.5	$⊢ φ \to D \neq E$
	flatcgra.6	$⊢ φ \to F \neq E$
Assertion	flatcgra	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$

Proof

Step	Hyp	Ref	Expression
1		cgracol.p	$⊢ P = {Base}_{G}$
2		cgracol.i	$⊢ I = Itv (G)$
3		cgracol.m	$⊢ \underset{˙}{-} = dist (G)$
4		cgracol.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		cgracol.a	$⊢ φ \to A \in P$
6		cgracol.b	$⊢ φ \to B \in P$
7		cgracol.c	$⊢ φ \to C \in P$
8		cgracol.d	$⊢ φ \to D \in P$
9		cgracol.e	$⊢ φ \to E \in P$
10		cgracol.f	$⊢ φ \to F \in P$
11		flatcgra.1	$⊢ φ \to B \in (A I C)$
12		flatcgra.2	$⊢ φ \to E \in (D I F)$
13		flatcgra.3	$⊢ φ \to A \neq B$
14		flatcgra.4	$⊢ φ \to C \neq B$
15		flatcgra.5	$⊢ φ \to D \neq E$
16		flatcgra.6	$⊢ φ \to F \neq E$
17		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
18	4	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to G \in 𝒢_{Tarski}$
19	5	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to A \in P$
20	6	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to B \in P$
21	7	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to C \in P$
22		simpllr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to x \in P$
23	9	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to E \in P$
24		simplr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to y \in P$
25		simprlr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to E \underset{˙}{-} x = B \underset{˙}{-} A$
26	1 3 2 18 23 22 20 19 25	tgcgrcomlr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to x \underset{˙}{-} E = A \underset{˙}{-} B$
27	26	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to A \underset{˙}{-} B = x \underset{˙}{-} E$
28		simprrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to E \underset{˙}{-} y = B \underset{˙}{-} C$
29	28	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to B \underset{˙}{-} C = E \underset{˙}{-} y$
30	10	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to F \in P$
31	8	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to D \in P$
32	16	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to F \neq E$
33	15	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to D \neq E$
34	1 3 2 4 8 9 10 12	tgbtwncom	$⊢ φ \to E \in (F I D)$
35	34	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to E \in (F I D)$
36		simprll	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to E \in (F I x)$
37		simprrl	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to E \in (D I y)$
38	1 2 18 30 23 31 22 24 32 33 35 36 37	tgbtwnconn22	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to E \in (x I y)$
39	11	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to B \in (A I C)$
40	1 3 2 18 22 23 24 19 20 21 38 39 26 28	tgcgrextend	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to x \underset{˙}{-} y = A \underset{˙}{-} C$
41	40	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to A \underset{˙}{-} C = x \underset{˙}{-} y$
42	1 3 2 18 19 21 22 24 41	tgcgrcomlr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to C \underset{˙}{-} A = y \underset{˙}{-} x$
43	1 3 17 18 19 20 21 22 23 24 27 29 42	trgcgr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩$
44	25	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to B \underset{˙}{-} A = E \underset{˙}{-} x$
45	13	necomd	$⊢ φ \to B \neq A$
46	45	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to B \neq A$
47	1 3 2 18 20 19 23 22 44 46	tgcgrneq	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to E \neq x$
48	47	necomd	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to x \neq E$
49	1 2 18 30 23 22 31 32 36 35	tgbtwnconn2	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to (x \in (E I D) \lor D \in (E I x))$
50	48 33 49	3jca	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to (x \neq E \land D \neq E \land (x \in (E I D) \lor D \in (E I x)))$
51		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
52	1 2 51 22 31 23 18	ishlg	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to (x {hl}_{𝒢} (G) (E) D \leftrightarrow (x \neq E \land D \neq E \land (x \in (E I D) \lor D \in (E I x))))$
53	50 52	mpbird	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to x {hl}_{𝒢} (G) (E) D$
54	14	necomd	$⊢ φ \to B \neq C$
55	54	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to B \neq C$
56	1 3 2 18 20 21 23 24 29 55	tgcgrneq	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to E \neq y$
57	56	necomd	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to y \neq E$
58	12	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to E \in (D I F)$
59	1 2 18 31 23 24 30 33 37 58	tgbtwnconn2	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to (y \in (E I F) \lor F \in (E I y))$
60	57 32 59	3jca	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to (y \neq E \land F \neq E \land (y \in (E I F) \lor F \in (E I y)))$
61	1 2 51 24 30 23 18	ishlg	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to (y {hl}_{𝒢} (G) (E) F \leftrightarrow (y \neq E \land F \neq E \land (y \in (E I F) \lor F \in (E I y))))$
62	60 61	mpbird	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to y {hl}_{𝒢} (G) (E) F$
63	43 53 62	3jca	$⊢ (((φ \land x \in P) \land y \in P) \land ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))) \to (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)$
64	1 3 2 4 10 9 6 5	axtgsegcon	$⊢ φ \to \exists x \in P (E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A)$
65	1 3 2 4 8 9 6 7	axtgsegcon	$⊢ φ \to \exists y \in P (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C)$
66		reeanv	$⊢ \exists x \in P \exists y \in P ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C)) \leftrightarrow (\exists x \in P (E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land \exists y \in P (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))$
67	64 65 66	sylanbrc	$⊢ φ \to \exists x \in P \exists y \in P ((E \in (F I x) \land E \underset{˙}{-} x = B \underset{˙}{-} A) \land (E \in (D I y) \land E \underset{˙}{-} y = B \underset{˙}{-} C))$
68	63 67	reximddv2	$⊢ φ \to \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)$
69	1 2 51 4 5 6 7 8 9 10	iscgra	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F))$
70	68 69	mpbird	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$

Metamath Proof Explorer

Theorem flatcgra

Proof