trgcopyeu

Description: Triangle construction: a copy of a given triangle can always be constructed in such a way that one side is lying on a half-line, and the third vertex is on a given half-plane: uniqueness part. Second part of Theorem 10.16 of Schwabhauser p. 92. (Contributed by Thierry Arnoux, 8-Aug-2020)

	Ref	Expression
Hypotheses	trgcopy.p	$⊢ P = {Base}_{G}$
	trgcopy.m	$⊢ \underset{˙}{-} = dist (G)$
	trgcopy.i	$⊢ I = Itv (G)$
	trgcopy.l	$⊢ L = {Line}_{𝒢} (G)$
	trgcopy.k	$⊢ K = {hl}_{𝒢} (G)$
	trgcopy.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	trgcopy.a	$⊢ φ \to A \in P$
	trgcopy.b	$⊢ φ \to B \in P$
	trgcopy.c	$⊢ φ \to C \in P$
	trgcopy.d	$⊢ φ \to D \in P$
	trgcopy.e	$⊢ φ \to E \in P$
	trgcopy.f	$⊢ φ \to F \in P$
	trgcopy.1	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
	trgcopy.2	$⊢ φ \to \neg (D \in (E L F) \lor E = F)$
	trgcopy.3	$⊢ φ \to A \underset{˙}{-} B = D \underset{˙}{-} E$
Assertion	trgcopyeu	$⊢ φ \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		trgcopy.p	$⊢ P = {Base}_{G}$
2		trgcopy.m	$⊢ \underset{˙}{-} = dist (G)$
3		trgcopy.i	$⊢ I = Itv (G)$
4		trgcopy.l	$⊢ L = {Line}_{𝒢} (G)$
5		trgcopy.k	$⊢ K = {hl}_{𝒢} (G)$
6		trgcopy.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		trgcopy.a	$⊢ φ \to A \in P$
8		trgcopy.b	$⊢ φ \to B \in P$
9		trgcopy.c	$⊢ φ \to C \in P$
10		trgcopy.d	$⊢ φ \to D \in P$
11		trgcopy.e	$⊢ φ \to E \in P$
12		trgcopy.f	$⊢ φ \to F \in P$
13		trgcopy.1	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
14		trgcopy.2	$⊢ φ \to \neg (D \in (E L F) \lor E = F)$
15		trgcopy.3	$⊢ φ \to A \underset{˙}{-} B = D \underset{˙}{-} E$
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	trgcopy	$⊢ φ \to \exists f \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)$
17	6	ad5antr	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to G \in 𝒢_{Tarski}$
18	7	ad5antr	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to A \in P$
19	8	ad5antr	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to B \in P$
20	9	ad5antr	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to C \in P$
21	10	ad5antr	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to D \in P$
22	11	ad5antr	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to E \in P$
23	12	ad5antr	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to F \in P$
24	13	ad5antr	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to \neg (A \in (B L C) \lor B = C)$
25	14	ad5antr	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to \neg (D \in (E L F) \lor E = F)$
26	15	ad5antr	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to A \underset{˙}{-} B = D \underset{˙}{-} E$
27		simpl	$⊢ (x = a \land y = b) \to x = a$
28	27	eleq1d	$⊢ (x = a \land y = b) \to (x \in (P ∖ (D L E)) \leftrightarrow a \in (P ∖ (D L E)))$
29		simpr	$⊢ (x = a \land y = b) \to y = b$
30	29	eleq1d	$⊢ (x = a \land y = b) \to (y \in (P ∖ (D L E)) \leftrightarrow b \in (P ∖ (D L E)))$
31	28 30	anbi12d	$⊢ (x = a \land y = b) \to ((x \in (P ∖ (D L E)) \land y \in (P ∖ (D L E))) \leftrightarrow (a \in (P ∖ (D L E)) \land b \in (P ∖ (D L E))))$
32		simpr	$⊢ ((x = a \land y = b) \land z = t) \to z = t$
33		simpll	$⊢ ((x = a \land y = b) \land z = t) \to x = a$
34		simplr	$⊢ ((x = a \land y = b) \land z = t) \to y = b$
35	33 34	oveq12d	$⊢ ((x = a \land y = b) \land z = t) \to x I y = a I b$
36	32 35	eleq12d	$⊢ ((x = a \land y = b) \land z = t) \to (z \in (x I y) \leftrightarrow t \in (a I b))$
37	36	cbvrexdva	$⊢ (x = a \land y = b) \to (\exists z \in (D L E) z \in (x I y) \leftrightarrow \exists t \in (D L E) t \in (a I b))$
38	31 37	anbi12d	$⊢ (x = a \land y = b) \to (((x \in (P ∖ (D L E)) \land y \in (P ∖ (D L E))) \land \exists z \in (D L E) z \in (x I y)) \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)))$
39	38	cbvopabv	$⊢ \{⟨x, y⟩ \| ((x \in (P ∖ (D L E)) \land y \in (P ∖ (D L E))) \land \exists z \in (D L E) z \in (x I y))\} = \{⟨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))\}$
40		simp-5r	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to f \in P$
41		simp-4r	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to k \in P$
42		simpllr	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)$
43	42	simpld	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩$
44		simplr	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩$
45	42	simprd	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to f {hp}_{𝒢} (G) (D L E) F$
46		simpr	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to k {hp}_{𝒢} (G) (D L E) F$
47	1 2 3 4 5 17 18 19 20 21 22 23 24 25 26 39 40 41 43 44 45 46	trgcopyeulem	$⊢ (((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩) \land k {hp}_{𝒢} (G) (D L E) F) \to f = k$
48	47	anasss	$⊢ ((((φ \land f \in P) \land k \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F)) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩ \land k {hp}_{𝒢} (G) (D L E) F)) \to f = k$
49	48	expl	$⊢ ((φ \land f \in P) \land k \in P) \to (((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩ \land k {hp}_{𝒢} (G) (D L E) F)) \to f = k)$
50	49	anasss	$⊢ (φ \land (f \in P \land k \in P)) \to (((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩ \land k {hp}_{𝒢} (G) (D L E) F)) \to f = k)$
51	50	ralrimivva	$⊢ φ \to \forall f \in P \forall k \in P (((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩ \land k {hp}_{𝒢} (G) (D L E) F)) \to f = k)$
52		eqidd	$⊢ f = k \to D = D$
53		eqidd	$⊢ f = k \to E = E$
54		id	$⊢ f = k \to f = k$
55	52 53 54	s3eqd	$⊢ f = k \to ⟨“ D E f ”⟩ = ⟨“ D E k ”⟩$
56	55	breq2d	$⊢ f = k \to (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \leftrightarrow ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩)$
57		breq1	$⊢ f = k \to (f {hp}_{𝒢} (G) (D L E) F \leftrightarrow k {hp}_{𝒢} (G) (D L E) F)$
58	56 57	anbi12d	$⊢ f = k \to ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F) \leftrightarrow (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩ \land k {hp}_{𝒢} (G) (D L E) F))$
59	58	reu4	$⊢ \exists! f \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F) \leftrightarrow (\exists f \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F) \land \forall f \in P \forall k \in P (((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E f ”⟩ \land f {hp}_{𝒢} (G) (D L E) F) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E k ”⟩ \land k {hp}_{𝒢} (G) (D L E) F)) \to f = k))$
60	16 51 59	sylanbrc	$⊢ φ \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 trgcopyeu

Proof