angmgmaddeu2

Description: Existence of a unique point for building angle addition. Case where the second angle is a zero angle. (Contributed by Thierry Arnoux, 23-Aug-2026)

	Ref	Expression
Hypotheses	angmgmadd.p	$⊢ P = {Base}_{G}$
	angmgmadd.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
	angmgmadd.i	$⊢ I = Itv (G)$
	angmgmadd.d	$⊢ \underset{˙}{-} = dist (G)$
	angmgmadd.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
	angmgmadd.l	$⊢ L = {Line}_{𝒢} (G)$
	angmgmadd.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	angmgmaddov.u	$⊢ φ \to U \in P$
	angmgmaddov.v	$⊢ φ \to V \in P$
	angmgmaddov.w	$⊢ φ \to W \in P$
	angmgmaddov.x	$⊢ φ \to X \in P$
	angmgmaddov.y	$⊢ φ \to Y \in P$
	angmgmaddov.z	$⊢ φ \to Z \in P$
	angmgmaddeu.1	$⊢ φ \to U \neq V$
	angmgmaddeu.2	$⊢ φ \to V \neq W$
	angmgmaddeu.3	$⊢ φ \to X \neq Y$
	angmgmaddeu.4	$⊢ φ \to Y \neq Z$
	angmgmaddeu2.1	$⊢ φ \to \neg X \in (Y L Z)$
	angmgmaddeu2.2	$⊢ φ \to U {hl}_{𝒢} (G) (V) W$
Assertion	angmgmaddeu2	$⊢ φ \to \exists! s \in P (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U \land (Y L Z) \cap (s I X) \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		angmgmadd.p	$⊢ P = {Base}_{G}$
2		angmgmadd.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
3		angmgmadd.i	$⊢ I = Itv (G)$
4		angmgmadd.d	$⊢ \underset{˙}{-} = dist (G)$
5		angmgmadd.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
6		angmgmadd.l	$⊢ L = {Line}_{𝒢} (G)$
7		angmgmadd.g	$⊢ φ \to G \in 𝒢_{Tarski}$
8		angmgmaddov.u	$⊢ φ \to U \in P$
9		angmgmaddov.v	$⊢ φ \to V \in P$
10		angmgmaddov.w	$⊢ φ \to W \in P$
11		angmgmaddov.x	$⊢ φ \to X \in P$
12		angmgmaddov.y	$⊢ φ \to Y \in P$
13		angmgmaddov.z	$⊢ φ \to Z \in P$
14		angmgmaddeu.1	$⊢ φ \to U \neq V$
15		angmgmaddeu.2	$⊢ φ \to V \neq W$
16		angmgmaddeu.3	$⊢ φ \to X \neq Y$
17		angmgmaddeu.4	$⊢ φ \to Y \neq Z$
18		angmgmaddeu2.1	$⊢ φ \to \neg X \in (Y L Z)$
19		angmgmaddeu2.2	$⊢ φ \to U {hl}_{𝒢} (G) (V) W$
20		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
21	17	necomd	$⊢ φ \to Z \neq Y$
22	14	necomd	$⊢ φ \to V \neq U$
23	1 3 20 12 9 8 7 13 4 21 22	hlcgreu	$⊢ φ \to \exists! s \in P (s {hl}_{𝒢} (G) (Y) Z \land Y \underset{˙}{-} s = V \underset{˙}{-} U)$
24	7	ad3antrrr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to G \in 𝒢_{Tarski}$
25		simpllr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to s \in P$
26	13	ad3antrrr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Z \in P$
27	12	ad3antrrr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Y \in P$
28		simplr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to s {hl}_{𝒢} (G) (Y) Z$
29	1 3 20 25 26 27 24 28	hlcomd	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Z {hl}_{𝒢} (G) (Y) s$
30	19	ad3antrrr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to U {hl}_{𝒢} (G) (V) W$
31	9	ad3antrrr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to V \in P$
32	1 5 20 24 29 30 27 31	zerocgra	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
33		simpr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Y \underset{˙}{-} s = V \underset{˙}{-} U$
34	17	ad3antrrr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Y \neq Z$
35	1 3 20 26 25 27 24 6 29	hlln	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Z \in (s L Y)$
36	8	ad3antrrr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to U \in P$
37	33	eqcomd	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to V \underset{˙}{-} U = Y \underset{˙}{-} s$
38	22	ad3antrrr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to V \neq U$
39	1 4 3 24 31 36 27 25 37 38	tgcgrneq	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Y \neq s$
40	39	necomd	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to s \neq Y$
41	1 3 6 24 27 26 25 34 35 40	lnrot1	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to s \in (Y L Z)$
42	11	ad3antrrr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to X \in P$
43	1 4 3 24 25 42	tgbtwntriv1	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to s \in (s I X)$
44	41 43	elind	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to s \in ((Y L Z) \cap (s I X))$
45	44	ne0d	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to (Y L Z) \cap (s I X) \neq \emptyset$
46	32 33 45	3jca	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) Z) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U \land (Y L Z) \cap (s I X) \neq \emptyset)$
47	46	anasss	$⊢ ((φ \land s \in P) \land (s {hl}_{𝒢} (G) (Y) Z \land Y \underset{˙}{-} s = V \underset{˙}{-} U)) \to (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U \land (Y L Z) \cap (s I X) \neq \emptyset)$
48	13	ad4antr	$⊢ ((((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land (Y L Z) \cap (s I X) \neq \emptyset) \to Z \in P$
49		simp-4r	$⊢ ((((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land (Y L Z) \cap (s I X) \neq \emptyset) \to s \in P$
50	12	ad4antr	$⊢ ((((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land (Y L Z) \cap (s I X) \neq \emptyset) \to Y \in P$
51	7	ad4antr	$⊢ ((((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land (Y L Z) \cap (s I X) \neq \emptyset) \to G \in 𝒢_{Tarski}$
52	8	ad4antr	$⊢ ((((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land (Y L Z) \cap (s I X) \neq \emptyset) \to U \in P$
53	9	ad4antr	$⊢ ((((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land (Y L Z) \cap (s I X) \neq \emptyset) \to V \in P$
54	10	ad4antr	$⊢ ((((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land (Y L Z) \cap (s I X) \neq \emptyset) \to W \in P$
55	5	a1i	$⊢ ((((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land (Y L Z) \cap (s I X) \neq \emptyset) \to \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
56		simpllr	$⊢ ((((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land (Y L Z) \cap (s I X) \neq \emptyset) \to ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
57	55 56	breqdi	$⊢ ((((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land (Y L Z) \cap (s I X) \neq \emptyset) \to ⟨“ Z Y s ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
58	1 3 51 20 48 50 49 52 53 54 57	cgracom	$⊢ ((((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land (Y L Z) \cap (s I X) \neq \emptyset) \to ⟨“ U V W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Z Y s ”⟩$
59	19	ad4antr	$⊢ ((((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land (Y L Z) \cap (s I X) \neq \emptyset) \to U {hl}_{𝒢} (G) (V) W$
60	1 3 4 51 52 53 54 48 50 49 58 20 59	cgrahl	$⊢ ((((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land (Y L Z) \cap (s I X) \neq \emptyset) \to Z {hl}_{𝒢} (G) (Y) s$
61	1 3 20 48 49 50 51 60	hlcomd	$⊢ ((((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land (Y L Z) \cap (s I X) \neq \emptyset) \to s {hl}_{𝒢} (G) (Y) Z$
62		simplr	$⊢ ((((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land (Y L Z) \cap (s I X) \neq \emptyset) \to Y \underset{˙}{-} s = V \underset{˙}{-} U$
63	61 62	jca	$⊢ ((((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land (Y L Z) \cap (s I X) \neq \emptyset) \to (s {hl}_{𝒢} (G) (Y) Z \land Y \underset{˙}{-} s = V \underset{˙}{-} U)$
64	63	3anasss	$⊢ ((φ \land s \in P) \land (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U \land (Y L Z) \cap (s I X) \neq \emptyset)) \to (s {hl}_{𝒢} (G) (Y) Z \land Y \underset{˙}{-} s = V \underset{˙}{-} U)$
65	47 64	impbida	$⊢ (φ \land s \in P) \to ((s {hl}_{𝒢} (G) (Y) Z \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \leftrightarrow (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U \land (Y L Z) \cap (s I X) \neq \emptyset))$
66	65	reubidva	$⊢ φ \to (\exists! s \in P (s {hl}_{𝒢} (G) (Y) Z \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \leftrightarrow \exists! s \in P (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U \land (Y L Z) \cap (s I X) \neq \emptyset))$
67	23 66	mpbid	$⊢ φ \to \exists! s \in P (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U \land (Y L Z) \cap (s I X) \neq \emptyset)$

Metamath Proof Explorer

Theorem angmgmaddeu2

Proof