cgracgr

Description: First direction of proposition 11.4 of Schwabhauser p. 95. Again, this is "half" of the proposition, i.e. only two additional points are used, while Schwabhauser has four. (Contributed by Thierry Arnoux, 31-Jul-2020)

	Ref	Expression
Hypotheses	iscgra.p	$⊢ P = {Base}_{G}$
	iscgra.i	$⊢ I = Itv (G)$
	iscgra.k	$⊢ K = {hl}_{𝒢} (G)$
	iscgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	iscgra.a	$⊢ φ \to A \in P$
	iscgra.b	$⊢ φ \to B \in P$
	iscgra.c	$⊢ φ \to C \in P$
	iscgra.d	$⊢ φ \to D \in P$
	iscgra.e	$⊢ φ \to E \in P$
	iscgra.f	$⊢ φ \to F \in P$
	cgrahl1.2	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
	cgrahl1.x	$⊢ φ \to X \in P$
	cgracgr.m	$⊢ \underset{˙}{-} = dist (G)$
	cgracgr.y	$⊢ φ \to Y \in P$
	cgracgr.1	$⊢ φ \to X K (B) A$
	cgracgr.2	$⊢ φ \to Y K (B) C$
	cgracgr.3	$⊢ φ \to B \underset{˙}{-} X = E \underset{˙}{-} D$
	cgracgr.4	$⊢ φ \to B \underset{˙}{-} Y = E \underset{˙}{-} F$
Assertion	cgracgr	$⊢ φ \to X \underset{˙}{-} Y = D \underset{˙}{-} F$

Proof

Step	Hyp	Ref	Expression
1		iscgra.p	$⊢ P = {Base}_{G}$
2		iscgra.i	$⊢ I = Itv (G)$
3		iscgra.k	$⊢ K = {hl}_{𝒢} (G)$
4		iscgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		iscgra.a	$⊢ φ \to A \in P$
6		iscgra.b	$⊢ φ \to B \in P$
7		iscgra.c	$⊢ φ \to C \in P$
8		iscgra.d	$⊢ φ \to D \in P$
9		iscgra.e	$⊢ φ \to E \in P$
10		iscgra.f	$⊢ φ \to F \in P$
11		cgrahl1.2	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
12		cgrahl1.x	$⊢ φ \to X \in P$
13		cgracgr.m	$⊢ \underset{˙}{-} = dist (G)$
14		cgracgr.y	$⊢ φ \to Y \in P$
15		cgracgr.1	$⊢ φ \to X K (B) A$
16		cgracgr.2	$⊢ φ \to Y K (B) C$
17		cgracgr.3	$⊢ φ \to B \underset{˙}{-} X = E \underset{˙}{-} D$
18		cgracgr.4	$⊢ φ \to B \underset{˙}{-} Y = E \underset{˙}{-} F$
19		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
20	4	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to G \in 𝒢_{Tarski}$
21	5	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to A \in P$
22	6	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to B \in P$
23	12	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to X \in P$
24		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
25		simpllr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to x \in P$
26	9	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to E \in P$
27	14	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to Y \in P$
28	8	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to D \in P$
29	10	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to F \in P$
30	1 2 3 12 5 6 4 15	hlne2	$⊢ φ \to A \neq B$
31	30	necomd	$⊢ φ \to B \neq A$
32	1 2 3 12 5 6 4 19 15	hlln	$⊢ φ \to X \in (A {Line}_{𝒢} (G) B)$
33	1 2 19 4 6 5 12 31 32	lncom	$⊢ φ \to X \in (B {Line}_{𝒢} (G) A)$
34	33	orcd	$⊢ φ \to (X \in (B {Line}_{𝒢} (G) A) \lor B = A)$
35	1 19 2 4 6 5 12 34	colrot1	$⊢ φ \to (B \in (A {Line}_{𝒢} (G) X) \lor A = X)$
36	35	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to (B \in (A {Line}_{𝒢} (G) X) \lor A = X)$
37	7	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to C \in P$
38		simplr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to y \in P$
39		simpr1	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩$
40	1 13 2 24 20 21 22 37 25 26 38 39	cgr3simp1	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to A \underset{˙}{-} B = x \underset{˙}{-} E$
41	17	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to B \underset{˙}{-} X = E \underset{˙}{-} D$
42		eqid	$⊢ \leq_{𝒢} (G) = \leq_{𝒢} (G)$
43		simpr2	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to x K (E) D$
44	1 2 3 25 28 26 20	ishlg	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to (x K (E) D \leftrightarrow (x \neq E \land D \neq E \land (x \in (E I D) \lor D \in (E I x))))$
45	43 44	mpbid	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to (x \neq E \land D \neq E \land (x \in (E I D) \lor D \in (E I x)))$
46	45	simp3d	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to (x \in (E I D) \lor D \in (E I x))$
47	1 2 3 12 5 6 4	ishlg	$⊢ φ \to (X K (B) A \leftrightarrow (X \neq B \land A \neq B \land (X \in (B I A) \lor A \in (B I X))))$
48	15 47	mpbid	$⊢ φ \to (X \neq B \land A \neq B \land (X \in (B I A) \lor A \in (B I X)))$
49	48	simp3d	$⊢ φ \to (X \in (B I A) \lor A \in (B I X))$
50	49	orcomd	$⊢ φ \to (A \in (B I X) \lor X \in (B I A))$
51	50	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to (A \in (B I X) \lor X \in (B I A))$
52	40	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to x \underset{˙}{-} E = A \underset{˙}{-} B$
53	1 13 2 20 25 26 21 22 52	tgcgrcomlr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to E \underset{˙}{-} x = B \underset{˙}{-} A$
54	41	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to E \underset{˙}{-} D = B \underset{˙}{-} X$
55	1 13 2 42 20 26 25 28 22 22 21 23 46 51 53 54	tgcgrsub2	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to x \underset{˙}{-} D = A \underset{˙}{-} X$
56	55	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to A \underset{˙}{-} X = x \underset{˙}{-} D$
57	1 13 2 20 21 23 25 28 56	tgcgrcomlr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to X \underset{˙}{-} A = D \underset{˙}{-} x$
58	1 13 24 20 21 22 23 25 26 28 40 41 57	trgcgr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to ⟨“ A B X ”⟩ \sim_{𝒢} (G) ⟨“ x E D ”⟩$
59	1 2 3 14 7 6 4 19 16	hlln	$⊢ φ \to Y \in (C {Line}_{𝒢} (G) B)$
60	59	orcd	$⊢ φ \to (Y \in (C {Line}_{𝒢} (G) B) \lor C = B)$
61	1 19 2 4 7 6 14 60	colrot1	$⊢ φ \to (C \in (B {Line}_{𝒢} (G) Y) \lor B = Y)$
62	61	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to (C \in (B {Line}_{𝒢} (G) Y) \lor B = Y)$
63	1 13 2 24 20 21 22 37 25 26 38 39	cgr3simp2	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to B \underset{˙}{-} C = E \underset{˙}{-} y$
64	1 2 3 14 7 6 4	ishlg	$⊢ φ \to (Y K (B) C \leftrightarrow (Y \neq B \land C \neq B \land (Y \in (B I C) \lor C \in (B I Y))))$
65	16 64	mpbid	$⊢ φ \to (Y \neq B \land C \neq B \land (Y \in (B I C) \lor C \in (B I Y)))$
66	65	simp3d	$⊢ φ \to (Y \in (B I C) \lor C \in (B I Y))$
67	66	orcomd	$⊢ φ \to (C \in (B I Y) \lor Y \in (B I C))$
68	67	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to (C \in (B I Y) \lor Y \in (B I C))$
69		simpr3	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to y K (E) F$
70	1 2 3 38 29 26 20	ishlg	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to (y K (E) F \leftrightarrow (y \neq E \land F \neq E \land (y \in (E I F) \lor F \in (E I y))))$
71	69 70	mpbid	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to (y \neq E \land F \neq E \land (y \in (E I F) \lor F \in (E I y)))$
72	71	simp3d	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to (y \in (E I F) \lor F \in (E I y))$
73	18	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to B \underset{˙}{-} Y = E \underset{˙}{-} F$
74	1 13 2 42 20 22 37 27 26 26 38 29 68 72 63 73	tgcgrsub2	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to C \underset{˙}{-} Y = y \underset{˙}{-} F$
75	1 13 2 20 22 27 26 29 73	tgcgrcomlr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to Y \underset{˙}{-} B = F \underset{˙}{-} E$
76	1 13 24 20 22 37 27 26 38 29 63 74 75	trgcgr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to ⟨“ B C Y ”⟩ \sim_{𝒢} (G) ⟨“ E y F ”⟩$
77	53	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to B \underset{˙}{-} A = E \underset{˙}{-} x$
78	1 13 2 24 20 21 22 37 25 26 38 39	cgr3simp3	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to C \underset{˙}{-} A = y \underset{˙}{-} x$
79	1 2 3 4 5 6 7 8 9 10 11	cgrane2	$⊢ φ \to B \neq C$
80	79	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to B \neq C$
81	1 19 2 20 22 37 27 24 26 38 13 21 29 25 62 76 77 78 80	tgfscgr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to Y \underset{˙}{-} A = F \underset{˙}{-} x$
82	1 13 2 20 27 21 29 25 81	tgcgrcomlr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to A \underset{˙}{-} Y = x \underset{˙}{-} F$
83	30	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to A \neq B$
84	1 19 2 20 21 22 23 24 25 26 13 27 28 29 36 58 82 73 83	tgfscgr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to X \underset{˙}{-} Y = D \underset{˙}{-} F$
85	1 2 3 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 K (E) D \land y K (E) F))$
86	11 85	mpbid	$⊢ φ \to \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)$
87	84 86	r19.29vva	$⊢ φ \to X \underset{˙}{-} Y = D \underset{˙}{-} F$

Metamath Proof Explorer

Theorem cgracgr

Proof