angmgmaddeu7

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	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$
	angmgmaddeu7.1	$⊢ φ \to Y \in (X I Z)$
	angmgmaddeu7.2	$⊢ φ \to V \in (U I W)$
Assertion	angmgmaddeu7	$⊢ φ \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		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		angmgmaddeu7.1	$⊢ φ \to Y \in (X I Z)$
19		angmgmaddeu7.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 angmgmaddeu7

Proof