angmndaddeu3

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

	Ref	Expression
Hypotheses	angmndadd.p	$⊢ P = {Base}_{G}$
	angmndadd.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
	angmndadd.i	$⊢ I = Itv (G)$
	angmndadd.d	$⊢ \underset{˙}{-} = dist (G)$
	angmndadd.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
	angmndadd.l	$⊢ L = {Line}_{𝒢} (G)$
	angmndadd.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	angmndaddov.u	$⊢ φ \to U \in P$
	angmndaddov.v	$⊢ φ \to V \in P$
	angmndaddov.w	$⊢ φ \to W \in P$
	angmndaddov.x	$⊢ φ \to X \in P$
	angmndaddov.y	$⊢ φ \to Y \in P$
	angmndaddov.z	$⊢ φ \to Z \in P$
	angmndaddeu.1	$⊢ φ \to U \neq V$
	angmndaddeu.2	$⊢ φ \to V \neq W$
	angmndaddeu.3	$⊢ φ \to X \neq Y$
	angmndaddeu.4	$⊢ φ \to Y \neq Z$
	angmndaddeu3.1	$⊢ φ \to \neg X \in (Y L Z)$
	angmndaddeu3.2	$⊢ φ \to V \in (U I W)$
Assertion	angmndaddeu3	$⊢ φ \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		angmndadd.p	$⊢ P = {Base}_{G}$
2		angmndadd.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
3		angmndadd.i	$⊢ I = Itv (G)$
4		angmndadd.d	$⊢ \underset{˙}{-} = dist (G)$
5		angmndadd.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
6		angmndadd.l	$⊢ L = {Line}_{𝒢} (G)$
7		angmndadd.g	$⊢ φ \to G \in 𝒢_{Tarski}$
8		angmndaddov.u	$⊢ φ \to U \in P$
9		angmndaddov.v	$⊢ φ \to V \in P$
10		angmndaddov.w	$⊢ φ \to W \in P$
11		angmndaddov.x	$⊢ φ \to X \in P$
12		angmndaddov.y	$⊢ φ \to Y \in P$
13		angmndaddov.z	$⊢ φ \to Z \in P$
14		angmndaddeu.1	$⊢ φ \to U \neq V$
15		angmndaddeu.2	$⊢ φ \to V \neq W$
16		angmndaddeu.3	$⊢ φ \to X \neq Y$
17		angmndaddeu.4	$⊢ φ \to Y \neq Z$
18		angmndaddeu3.1	$⊢ φ \to \neg X \in (Y L Z)$
19		angmndaddeu3.2	$⊢ φ \to V \in (U I W)$
20	17	necomd	$⊢ φ \to Z \neq Y$
21	1 4 3 7 13 12 9 8 20	tgsegconeu	$⊢ φ \to \exists! s \in P (Y \in (Z I s) \land Y \underset{˙}{-} s = V \underset{˙}{-} U)$
22	5	eqcomi	$⊢ \sim_{𝒢}^{∠} (G) = \underset{˙}{\sim}$
23	22	a1i	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to \sim_{𝒢}^{∠} (G) = \underset{˙}{\sim}$
24	7	ad3antrrr	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to G \in 𝒢_{Tarski}$
25	13	ad3antrrr	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Z \in P$
26	12	ad3antrrr	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Y \in P$
27		simpllr	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to s \in P$
28	8	ad3antrrr	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to U \in P$
29	9	ad3antrrr	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to V \in P$
30	10	ad3antrrr	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to W \in P$
31		simplr	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Y \in (Z I s)$
32	19	ad3antrrr	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to V \in (U I W)$
33	20	ad3antrrr	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Z \neq Y$
34		simpr	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Y \underset{˙}{-} s = V \underset{˙}{-} U$
35	34	eqcomd	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to V \underset{˙}{-} U = Y \underset{˙}{-} s$
36	14	necomd	$⊢ φ \to V \neq U$
37	36	ad3antrrr	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to V \neq U$
38	1 4 3 24 29 28 26 27 35 37	tgcgrneq	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Y \neq s$
39	38	necomd	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to s \neq Y$
40	14	ad3antrrr	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to U \neq V$
41	15	necomd	$⊢ φ \to W \neq V$
42	41	ad3antrrr	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to W \neq V$
43	1 3 4 24 25 26 27 28 29 30 31 32 33 39 40 42	flatcgra	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to ⟨“ Z Y s ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
44	23 43	breqdi	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
45	17	ad3antrrr	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Y \neq Z$
46	24	adantr	$⊢ ((((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land Z = s) \to G \in 𝒢_{Tarski}$
47	25	adantr	$⊢ ((((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land Z = s) \to Z \in P$
48	26	adantr	$⊢ ((((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land Z = s) \to Y \in P$
49		simpllr	$⊢ ((((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land Z = s) \to Y \in (Z I s)$
50		simpr	$⊢ ((((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land Z = s) \to Z = s$
51	50	oveq2d	$⊢ ((((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land Z = s) \to Z I Z = Z I s$
52	49 51	eleqtrrd	$⊢ ((((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land Z = s) \to Y \in (Z I Z)$
53	1 4 3 46 47 48 52	axtgbtwnid	$⊢ ((((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land Z = s) \to Z = Y$
54	53	eqcomd	$⊢ ((((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \land Z = s) \to Y = Z$
55	45 54	mteqand	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Z \neq s$
56	1 3 6 24 25 27 26 55 31	btwnlng1	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Y \in (Z L s)$
57	1 3 6 24 26 25 27 45 56 55	lnrot2	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to s \in (Y L Z)$
58	11	ad3antrrr	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to X \in P$
59	1 4 3 24 27 58	tgbtwntriv1	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to s \in (s I X)$
60	57 59	elind	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to s \in ((Y L Z) \cap (s I X))$
61	60	ne0d	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to (Y L Z) \cap (s I X) \neq \emptyset$
62	44 34 61	3jca	$⊢ (((φ \land s \in P) \land Y \in (Z I s)) \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)$
63	62	anasss	$⊢ ((φ \land s \in P) \land (Y \in (Z I s) \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)$
64	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}$
65	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$
66	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$
67	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$
68	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$
69	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$
70		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$
71		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
72	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)$
73		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 ”⟩$
74	72 73	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 ”⟩$
75	1 3 64 71 68 69 70 65 66 67 74	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 ”⟩$
76	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 V \in (U I W)$
77	1 3 4 64 65 66 67 68 69 70 75 76	cgrabtwn	$⊢ ((((φ \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 (Z I s)$
78		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$
79	77 78	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 (Y \in (Z I s) \land Y \underset{˙}{-} s = V \underset{˙}{-} U)$
80	79	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 (Y \in (Z I s) \land Y \underset{˙}{-} s = V \underset{˙}{-} U)$
81	63 80	impbida	$⊢ (φ \land s \in P) \to ((Y \in (Z I s) \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))$
82	81	reubidva	$⊢ φ \to (\exists! s \in P (Y \in (Z I s) \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))$
83	21 82	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 angmndaddeu3

Proof