acopy

Description: Angle construction. Theorem 11.15 of Schwabhauser p. 98. This is Hilbert's axiom III.4 for geometry. (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)$
Assertion	acopy	$⊢ φ \to \exists f \in P (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)$

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		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
15	4	ad2antrr	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to G \in 𝒢_{Tarski}$
16	5	ad2antrr	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to A \in P$
17	6	ad2antrr	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to B \in P$
18	7	ad2antrr	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to C \in P$
19		simplr	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to d \in P$
20	9	ad2antrr	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to E \in P$
21	10	ad2antrr	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to F \in P$
22	12	ad2antrr	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to \neg (A \in (B L C) \lor B = C)$
23	8	ad2antrr	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to D \in P$
24	13	ad2antrr	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to \neg (D \in (E L F) \lor E = F)$
25		simprl	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to d {hl}_{𝒢} (G) (E) D$
26	1 2 14 19 23 20 15 11 25	hlln	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to d \in (D L E)$
27	1 2 14 19 23 20 15 25	hlne1	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to d \neq E$
28	1 2 11 15 23 20 21 19 24 26 27	ncolncol	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to \neg (d \in (E L F) \lor E = F)$
29		simprr	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to E \underset{˙}{-} d = B \underset{˙}{-} A$
30	29	eqcomd	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to B \underset{˙}{-} A = E \underset{˙}{-} d$
31	1 3 2 15 17 16 20 19 30	tgcgrcomlr	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to A \underset{˙}{-} B = d \underset{˙}{-} E$
32	1 3 2 11 14 15 16 17 18 19 20 21 22 28 31	trgcopy	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to \exists f \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩ \land f {hp}_{𝒢} (G) (d L E) F)$
33	15	ad2antrr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩) \to G \in 𝒢_{Tarski}$
34	16	ad2antrr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩) \to A \in P$
35	17	ad2antrr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩) \to B \in P$
36	18	ad2antrr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩) \to C \in P$
37	19	ad2antrr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩) \to d \in P$
38	20	ad2antrr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩) \to E \in P$
39		simplr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩) \to f \in P$
40	1 2 11 4 5 6 7 12	ncolne1	$⊢ φ \to A \neq B$
41	40	ad4antr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩) \to A \neq B$
42	1 11 2 4 6 7 5 12	ncolrot1	$⊢ φ \to \neg (B \in (C L A) \lor C = A)$
43	1 2 11 4 6 7 5 42	ncolne1	$⊢ φ \to B \neq C$
44	43	ad4antr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩) \to B \neq C$
45		simpr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩$
46	1 2 33 14 34 35 36 37 38 39 41 44 45	cgrcgra	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ d E f ”⟩$
47	23	ad2antrr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩) \to D \in P$
48	25	ad2antrr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩) \to d {hl}_{𝒢} (G) (E) D$
49	1 2 14 37 47 38 33 48	hlcomd	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩) \to D {hl}_{𝒢} (G) (E) d$
50	1 2 14 33 34 35 36 37 38 39 46 47 49	cgrahl1	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E f ”⟩$
51	50	ex	$⊢ (((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \to (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E f ”⟩)$
52		simpr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land f {hp}_{𝒢} (G) (d L E) F) \to f {hp}_{𝒢} (G) (d L E) F$
53	15	ad2antrr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land f {hp}_{𝒢} (G) (d L E) F) \to G \in 𝒢_{Tarski}$
54	19	ad2antrr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land f {hp}_{𝒢} (G) (d L E) F) \to d \in P$
55	20	ad2antrr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land f {hp}_{𝒢} (G) (d L E) F) \to E \in P$
56	27	ad2antrr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land f {hp}_{𝒢} (G) (d L E) F) \to d \neq E$
57	1 2 11 4 8 9 10 13	ncolne1	$⊢ φ \to D \neq E$
58	1 2 11 4 8 9 57	tgelrnln	$⊢ φ \to D L E \in ran L$
59	58	ad4antr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land f {hp}_{𝒢} (G) (d L E) F) \to D L E \in ran L$
60	26	ad2antrr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land f {hp}_{𝒢} (G) (d L E) F) \to d \in (D L E)$
61	1 2 11 4 8 9 57	tglinerflx2	$⊢ φ \to E \in (D L E)$
62	61	ad4antr	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land f {hp}_{𝒢} (G) (d L E) F) \to E \in (D L E)$
63	1 2 11 53 54 55 56 56 59 60 62	tglinethru	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land f {hp}_{𝒢} (G) (d L E) F) \to D L E = d L E$
64	63	fveq2d	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land f {hp}_{𝒢} (G) (d L E) F) \to {hp}_{𝒢} (G) (D L E) = {hp}_{𝒢} (G) (d L E)$
65	64	breqd	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land f {hp}_{𝒢} (G) (d L E) F) \to (f {hp}_{𝒢} (G) (D L E) F \leftrightarrow f {hp}_{𝒢} (G) (d L E) F)$
66	52 65	mpbird	$⊢ ((((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \land f {hp}_{𝒢} (G) (d L E) F) \to f {hp}_{𝒢} (G) (D L E) F$
67	66	ex	$⊢ (((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \to (f {hp}_{𝒢} (G) (d L E) F \to f {hp}_{𝒢} (G) (D L E) F)$
68	51 67	anim12d	$⊢ (((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \land f \in P) \to ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩ \land f {hp}_{𝒢} (G) (d L E) F) \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F))$
69	68	reximdva	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to (\exists f \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ d E f ”⟩ \land f {hp}_{𝒢} (G) (d L E) F) \to \exists f \in P (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F))$
70	32 69	mpd	$⊢ ((φ \land d \in P) \land (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)) \to \exists f \in P (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)$
71	40	necomd	$⊢ φ \to B \neq A$
72	1 2 14 9 6 5 4 8 3 57 71	hlcgrex	$⊢ φ \to \exists d \in P (d {hl}_{𝒢} (G) (E) D \land E \underset{˙}{-} d = B \underset{˙}{-} A)$
73	70 72	r19.29a	$⊢ φ \to \exists f \in P (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)$

Metamath Proof Explorer

Theorem acopy

Proof