acopyeu

Description: Angle construction. Theorem 11.15 of Schwabhauser p. 98. This is Hilbert's axiom III.4 for geometry. Akin to a uniqueness theorem, this states that if two points X and Y both fulfill the conditions, then they are on the same half-line. (Contributed by Thierry Arnoux, 9-Aug-2020)

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

Proof

Step	Hyp	Ref	Expression
1		dfcgra2.p	$⊢ P = {Base}_{G}$
2		dfcgra2.i	$⊢ I = Itv (G)$
3		dfcgra2.m	$⊢ \underset{˙}{-} = dist (G)$
4		dfcgra2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		dfcgra2.a	$⊢ φ \to A \in P$
6		dfcgra2.b	$⊢ φ \to B \in P$
7		dfcgra2.c	$⊢ φ \to C \in P$
8		dfcgra2.d	$⊢ φ \to D \in P$
9		dfcgra2.e	$⊢ φ \to E \in P$
10		dfcgra2.f	$⊢ φ \to F \in P$
11		acopy.l	$⊢ L = {Line}_{𝒢} (G)$
12		acopy.1	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
13		acopy.2	$⊢ φ \to \neg (D \in (E L F) \lor E = F)$
14		acopyeu.x	$⊢ φ \to X \in P$
15		acopyeu.y	$⊢ φ \to Y \in P$
16		acopyeu.k	$⊢ K = {hl}_{𝒢} (G)$
17		acopyeu.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E X ”⟩$
18		acopyeu.2	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E Y ”⟩$
19		acopyeu.3	$⊢ φ \to X {hp}_{𝒢} (G) (D L E) F$
20		acopyeu.4	$⊢ φ \to Y {hp}_{𝒢} (G) (D L E) F$
21	14	ad2antrr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to X \in P$
22	21	ad3antrrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to X \in P$
23		simplr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to y \in P$
24	15	ad2antrr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to Y \in P$
25	24	ad3antrrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to Y \in P$
26	4	ad2antrr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to G \in 𝒢_{Tarski}$
27	26	ad3antrrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to G \in 𝒢_{Tarski}$
28	9	ad2antrr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to E \in P$
29	28	ad3antrrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to E \in P$
30	5	ad2antrr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to A \in P$
31	30	ad3antrrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to A \in P$
32	6	ad2antrr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to B \in P$
33	32	ad3antrrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to B \in P$
34	7	ad2antrr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to C \in P$
35	34	ad3antrrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to C \in P$
36		simplr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to d \in P$
37	36	ad3antrrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to d \in P$
38	10	ad2antrr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to F \in P$
39	38	ad3antrrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to F \in P$
40	12	ad2antrr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to \neg (A \in (B L C) \lor B = C)$
41	40	ad3antrrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to \neg (A \in (B L C) \lor B = C)$
42	8	ad2antrr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to D \in P$
43	13	ad2antrr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to \neg (D \in (E L F) \lor E = F)$
44		simprl	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to d K (E) D$
45	1 2 16 36 42 28 26 11 44	hlln	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to d \in (D L E)$
46	1 2 16 36 42 28 26 44	hlne1	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to d \neq E$
47	1 2 11 26 42 28 38 36 43 45 46	ncolncol	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to \neg (d \in (E L F) \lor E = F)$
48	47	ad3antrrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to \neg (d \in (E L F) \lor E = F)$
49		simprr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to E \underset{˙}{-} d = B \underset{˙}{-} A$
50	1 3 2 26 28 36 32 30 49	tgcgrcomlr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to d \underset{˙}{-} E = A \underset{˙}{-} B$
51	50	eqcomd	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to A \underset{˙}{-} B = d \underset{˙}{-} E$
52	51	ad3antrrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to A \underset{˙}{-} B = d \underset{˙}{-} E$
53		simpl	$⊢ (u = a \land v = b) \to u = a$
54	53	eleq1d	$⊢ (u = a \land v = b) \to (u \in (P ∖ (d L E)) \leftrightarrow a \in (P ∖ (d L E)))$
55		simpr	$⊢ (u = a \land v = b) \to v = b$
56	55	eleq1d	$⊢ (u = a \land v = b) \to (v \in (P ∖ (d L E)) \leftrightarrow b \in (P ∖ (d L E)))$
57	54 56	anbi12d	$⊢ (u = a \land v = b) \to ((u \in (P ∖ (d L E)) \land v \in (P ∖ (d L E))) \leftrightarrow (a \in (P ∖ (d L E)) \land b \in (P ∖ (d L E))))$
58		simpr	$⊢ ((u = a \land v = b) \land w = t) \to w = t$
59		simpll	$⊢ ((u = a \land v = b) \land w = t) \to u = a$
60		simplr	$⊢ ((u = a \land v = b) \land w = t) \to v = b$
61	59 60	oveq12d	$⊢ ((u = a \land v = b) \land w = t) \to u I v = a I b$
62	58 61	eleq12d	$⊢ ((u = a \land v = b) \land w = t) \to (w \in (u I v) \leftrightarrow t \in (a I b))$
63	62	cbvrexdva	$⊢ (u = a \land v = b) \to (\exists w \in (d L E) w \in (u I v) \leftrightarrow \exists t \in (d L E) t \in (a I b))$
64	57 63	anbi12d	$⊢ (u = a \land v = b) \to (((u \in (P ∖ (d L E)) \land v \in (P ∖ (d L E))) \land \exists w \in (d L E) w \in (u I v)) \leftrightarrow ((a \in (P ∖ (d L E)) \land b \in (P ∖ (d L E))) \land \exists t \in (d L E) t \in (a I b)))$
65	64	cbvopabv	$⊢ \{⟨u, v⟩ \| ((u \in (P ∖ (d L E)) \land v \in (P ∖ (d L E))) \land \exists w \in (d L E) w \in (u I v))\} = \{⟨a, b⟩ \| ((a \in (P ∖ (d L E)) \land b \in (P ∖ (d L E))) \land \exists t \in (d L E) t \in (a I b))\}$
66		simpllr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to x \in P$
67		simprll	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩$
68		simprrl	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩$
69	1 2 11 26 36 28 46	tgelrnln	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to d L E \in ran L$
70	69	ad3antrrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to d L E \in ran L$
71	1 2 11 26 36 28 46	tglinerflx2	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to E \in (d L E)$
72	71	ad3antrrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to E \in (d L E)$
73	42	ad3antrrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to D \in P$
74	1 11 2 4 6 7 5 12	ncolrot2	$⊢ φ \to \neg (C \in (A L B) \lor A = B)$
75	1 2 3 4 5 6 7 8 9 14 17 11 74	cgrancol	$⊢ φ \to \neg (X \in (D L E) \lor D = E)$
76	1 11 2 4 8 9 14 75	ncolcom	$⊢ φ \to \neg (X \in (E L D) \lor E = D)$
77	76	ad5antr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to \neg (X \in (E L D) \lor E = D)$
78		simprlr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to x K (E) X$
79	1 2 16 66 22 29 27 11 78	hlln	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to x \in (X L E)$
80	1 2 16 66 22 29 27 78	hlne1	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to x \neq E$
81	1 2 11 27 22 29 73 66 77 79 80	ncolncol	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to \neg (x \in (E L D) \lor E = D)$
82	1 11 2 27 29 73 66 81	ncolcom	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to \neg (x \in (D L E) \lor D = E)$
83		pm2.45	$⊢ \neg (x \in (D L E) \lor D = E) \to \neg x \in (D L E)$
84	82 83	syl	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to \neg x \in (D L E)$
85	1 2 11 4 8 9 10 13	ncolne1	$⊢ φ \to D \neq E$
86	1 2 11 4 8 9 85	tgelrnln	$⊢ φ \to D L E \in ran L$
87	86	ad2antrr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to D L E \in ran L$
88	1 2 11 4 8 9 85	tglinerflx2	$⊢ φ \to E \in (D L E)$
89	88	ad2antrr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to E \in (D L E)$
90	1 2 11 26 36 28 46 46 87 45 89	tglinethru	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to D L E = d L E$
91	90	ad3antrrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to D L E = d L E$
92	84 91	neleqtrd	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to \neg x \in (d L E)$
93	1 2 11 27 70 29 65 16 72 66 22 92 78	hphl	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to x {hp}_{𝒢} (G) (d L E) X$
94	90	fveq2d	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to {hp}_{𝒢} (G) (D L E) = {hp}_{𝒢} (G) (d L E)$
95	94	ad3antrrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to {hp}_{𝒢} (G) (D L E) = {hp}_{𝒢} (G) (d L E)$
96	19	ad5antr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to X {hp}_{𝒢} (G) (D L E) F$
97	95 96	breqdi	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to X {hp}_{𝒢} (G) (d L E) F$
98	1 2 11 27 70 66 65 22 93 39 97	hpgtr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to x {hp}_{𝒢} (G) (d L E) F$
99	1 2 3 4 5 6 7 8 9 15 18 11 74	cgrancol	$⊢ φ \to \neg (Y \in (D L E) \lor D = E)$
100	1 11 2 4 8 9 15 99	ncolcom	$⊢ φ \to \neg (Y \in (E L D) \lor E = D)$
101	100	ad5antr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to \neg (Y \in (E L D) \lor E = D)$
102		simprrr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to y K (E) Y$
103	1 2 16 23 25 29 27 11 102	hlln	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to y \in (Y L E)$
104	1 2 16 23 25 29 27 102	hlne1	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to y \neq E$
105	1 2 11 27 25 29 73 23 101 103 104	ncolncol	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to \neg (y \in (E L D) \lor E = D)$
106	1 11 2 27 29 73 23 105	ncolcom	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to \neg (y \in (D L E) \lor D = E)$
107		pm2.45	$⊢ \neg (y \in (D L E) \lor D = E) \to \neg y \in (D L E)$
108	106 107	syl	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to \neg y \in (D L E)$
109	108 91	neleqtrd	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to \neg y \in (d L E)$
110	1 2 11 27 70 29 65 16 72 23 25 109 102	hphl	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to y {hp}_{𝒢} (G) (d L E) Y$
111	20	ad5antr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to Y {hp}_{𝒢} (G) (D L E) F$
112	95 111	breqdi	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to Y {hp}_{𝒢} (G) (d L E) F$
113	1 2 11 27 70 23 65 25 110 39 112	hpgtr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to y {hp}_{𝒢} (G) (d L E) F$
114	1 3 2 11 16 27 31 33 35 37 29 39 41 48 52 65 66 23 67 68 98 113	trgcopyeulem	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to x = y$
115	114 78	eqbrtrrd	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to y K (E) X$
116	1 2 16 23 22 29 27 115	hlcomd	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to X K (E) y$
117	1 2 16 22 23 25 27 29 116 102	hltr	$⊢ (((((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land x \in P) \land y \in P) \land ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))) \to X K (E) Y$
118	17	ad2antrr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E X ”⟩$
119	1 2 16 26 30 32 34 42 28 21 118 36 44	cgrahl1	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ d E X ”⟩$
120	1 2 11 4 5 6 7 12	ncolne1	$⊢ φ \to A \neq B$
121	120	ad2antrr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to A \neq B$
122	1 2 16 26 30 32 34 36 28 21 3 121 51	iscgra1	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ d E X ”⟩ \leftrightarrow \exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X))$
123	119 122	mpbid	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to \exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X)$
124	18	ad2antrr	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E Y ”⟩$
125	1 2 16 26 30 32 34 42 28 24 124 36 44	cgrahl1	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ d E Y ”⟩$
126	1 2 16 26 30 32 34 36 28 24 3 121 51	iscgra1	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ d E Y ”⟩ \leftrightarrow \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))$
127	125 126	mpbid	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y)$
128		reeanv	$⊢ \exists x \in P \exists y \in P ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y)) \leftrightarrow (\exists x \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))$
129	123 127 128	sylanbrc	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to \exists x \in P \exists y \in P ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E x ”⟩ \land x K (E) X) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E y ”⟩ \land y K (E) Y))$
130	117 129	r19.29vva	$⊢ ((φ \land d \in P) \land (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to X K (E) Y$
131	120	necomd	$⊢ φ \to B \neq A$
132	1 2 16 9 6 5 4 8 3 85 131	hlcgrex	$⊢ φ \to \exists d \in P (d K (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)$
133	130 132	r19.29a	$⊢ φ \to X K (E) Y$

Metamath Proof Explorer

Theorem acopyeu

Proof