angmgmaddeu4

Description: There exists a unique point s satisfying the conditions of angle addition. Case where both angles are zero 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$
	angmgmaddeu4.1	$⊢ φ \to X {hl}_{𝒢} (G) (Y) Z$
	angmgmaddeu4.2	$⊢ φ \to U {hl}_{𝒢} (G) (V) W$
Assertion	angmgmaddeu4	$⊢ φ \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		angmgmaddeu4.1	$⊢ φ \to X {hl}_{𝒢} (G) (Y) Z$
19		angmgmaddeu4.2	$⊢ φ \to U {hl}_{𝒢} (G) (V) W$
20		eqid	$⊢ Itv (G) = Itv (G)$
21		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
22	14	necomd	$⊢ φ \to V \neq U$
23	1 20 21 12 9 8 7 11 4 16 22	hlcgreu	$⊢ φ \to \exists! s \in P (s {hl}_{𝒢} (G) (Y) X \land Y \underset{˙}{-} s = V \underset{˙}{-} U)$
24	7	ad3antrrr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to G \in 𝒢_{Tarski}$
25	13	ad3antrrr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Z \in P$
26	11	ad3antrrr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to X \in P$
27		simpllr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to s \in P$
28	12	ad3antrrr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Y \in P$
29	1 3 21 11 13 12 7 18	hlcomd	$⊢ φ \to Z {hl}_{𝒢} (G) (Y) X$
30	29	ad3antrrr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Z {hl}_{𝒢} (G) (Y) X$
31		simplr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to s {hl}_{𝒢} (G) (Y) X$
32	1 3 21 27 26 28 24 31	hlcomd	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to X {hl}_{𝒢} (G) (Y) s$
33	1 3 21 25 26 27 24 28 30 32	hltr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Z {hl}_{𝒢} (G) (Y) s$
34	19	ad3antrrr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to U {hl}_{𝒢} (G) (V) W$
35	9	ad3antrrr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to V \in P$
36	1 5 21 24 33 34 28 35	zerocgra	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
37		simpr	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Y \underset{˙}{-} s = V \underset{˙}{-} U$
38	36 37	jca	$⊢ (((φ \land s \in P) \land s {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U)$
39	38	anasss	$⊢ ((φ \land s \in P) \land (s {hl}_{𝒢} (G) (Y) X \land Y \underset{˙}{-} s = V \underset{˙}{-} U)) \to (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U)$
40	11	ad3antrrr	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to X \in P$
41		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$
42	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$
43	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}$
44	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$
45	18	ad3antrrr	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to X {hl}_{𝒢} (G) (Y) Z$
46	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$
47	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$
48	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$
49	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)$
50		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 ”⟩$
51	49 50	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 ”⟩$
52	1 3 43 21 44 42 41 46 47 48 51	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 ”⟩$
53	19	ad3antrrr	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to U {hl}_{𝒢} (G) (V) W$
54	1 3 4 43 46 47 48 44 42 41 52 21 53	cgrahl	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to Z {hl}_{𝒢} (G) (Y) s$
55	1 3 21 40 44 41 43 42 45 54	hltr	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to X {hl}_{𝒢} (G) (Y) s$
56	1 3 21 40 41 42 43 55	hlcomd	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to s {hl}_{𝒢} (G) (Y) X$
57		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$
58	56 57	jca	$⊢ (((φ \land s \in P) \land ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩) \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \to (s {hl}_{𝒢} (G) (Y) X \land Y \underset{˙}{-} s = V \underset{˙}{-} U)$
59	58	anasss	$⊢ ((φ \land s \in P) \land (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U)) \to (s {hl}_{𝒢} (G) (Y) X \land Y \underset{˙}{-} s = V \underset{˙}{-} U)$
60	39 59	impbida	$⊢ (φ \land s \in P) \to ((s {hl}_{𝒢} (G) (Y) X \land Y \underset{˙}{-} s = V \underset{˙}{-} U) \leftrightarrow (⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩ \land Y \underset{˙}{-} s = V \underset{˙}{-} U))$
61	60	reubidva	$⊢ φ \to (\exists! s \in P (s {hl}_{𝒢} (G) (Y) X \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))$
62	23 61	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 angmgmaddeu4

Proof