angmgmaddeu6

Description: There exists a unique point s satisfying the conditions of angle addition. Case where the first angle is a zero angle, and the second angle is a straight 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$
	angmgmaddeu6.1	$⊢ φ \to Y \in (X I Z)$
	angmgmaddeu6.2	$⊢ φ \to U {hl}_{𝒢} (G) (V) W$
Assertion	angmgmaddeu6	$⊢ φ \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		angmgmaddeu6.1	$⊢ φ \to Y \in (X I Z)$
19		angmgmaddeu6.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	32 33	jca	$⊢ (((φ \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)$
35	34	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)$
36	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$
37		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$
38	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$
39	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}$
40	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$
41	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$
42	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$
43	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)$
44		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 ”⟩$
45	43 44	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 ”⟩$
46	1 3 39 20 36 38 37 40 41 42 45	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 ”⟩$
47	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$
48	1 3 4 39 40 41 42 36 38 37 46 20 47	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$
49	1 3 20 36 37 38 39 48	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) Z$
50		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$
51	49 50	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) Z \land Y \underset{˙}{-} s = V \underset{˙}{-} U)$
52	51	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) Z \land Y \underset{˙}{-} s = V \underset{˙}{-} U)$
53	35 52	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))$
54	53	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))$
55	23 54	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 angmgmaddeu6

Proof