angmndaddeu7

Description: There exists a unique point s satisfying the conditions of angle addition. Case where both angles are straight angles. (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$
	angmndaddeu7.1	$⊢ φ \to Y \in (X I Z)$
	angmndaddeu7.2	$⊢ φ \to V \in (U I W)$
Assertion	angmndaddeu7	$⊢ φ \to \exists! s \in P (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U)$

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		angmndaddeu7.1	$⊢ φ \to Y \in (X I Z)$
19		angmndaddeu7.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	44 34	jca	$⊢ (((φ \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)$
46	45	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)$
47	7	ad3antrrr	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to G \in 𝒢_{Tarski}$
48	8	ad3antrrr	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to U \in P$
49	9	ad3antrrr	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to V \in P$
50	10	ad3antrrr	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to W \in P$
51	13	ad3antrrr	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Z \in P$
52	12	ad3antrrr	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Y \in P$
53		simpllr	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to s \in P$
54		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
55	5	a1i	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
56		simplr	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \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) \to ⟨“ Z Y s ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
58	1 3 47 54 51 52 53 48 49 50 57	cgracom	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to ⟨“ U V W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Z Y s ”⟩$
59	19	ad3antrrr	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to V \in (U I W)$
60	1 3 4 47 48 49 50 51 52 53 58 59	cgrabtwn	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Y \in (Z I s)$
61		simpr	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Y \underset{˙}{-} s = V \underset{˙}{-} U$
62	60 61	jca	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to (Y \in (Z I s) \land Y \underset{˙}{-} s = V \underset{˙}{-} U)$
63	62	anasss	$⊢ ((φ \land s \in P) \land (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U)) \to (Y \in (Z I s) \land Y \underset{˙}{-} s = V \underset{˙}{-} U)$
64	46 63	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))$
65	64	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))$
66	21 65	mpbid	$⊢ φ \to \exists! s \in P (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U)$

Metamath Proof Explorer

Theorem angmndaddeu7

Proof