Theorem angmndaddov1lem

Description: Lemma for angmndaddov1 . (Contributed by Thierry Arnoux, 23-Aug-2026)

	Ref	Expression
Hypotheses	angmndadd.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	angmndadd.a	⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
	angmndadd.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	angmndadd.d	⊢ − = ( dist ‘ 𝐺 )
	angmndadd.c	⊢ ∼ = ( cgrA ‘ 𝐺 )
	angmndadd.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	angmndadd.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	angmndaddov.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
	angmndaddov.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
	angmndaddov.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
	angmndaddov.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	angmndaddov.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	angmndaddov.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
	angmndaddeu.1	⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
	angmndaddeu.2	⊢ ( 𝜑 → 𝑉 ≠ 𝑊 )
	angmndaddeu.3	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
	angmndaddeu.4	⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
	angmndaddov1lem.1	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
Assertion	angmndaddov1lem	⊢ ( 𝜑 → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		angmndadd.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		angmndadd.a	⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
3		angmndadd.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		angmndadd.d	⊢ − = ( dist ‘ 𝐺 )
5		angmndadd.c	⊢ ∼ = ( cgrA ‘ 𝐺 )
6		angmndadd.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
7		angmndadd.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8		angmndaddov.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
9		angmndaddov.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
10		angmndaddov.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
11		angmndaddov.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
12		angmndaddov.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
13		angmndaddov.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
14		angmndaddeu.1	⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
15		angmndaddeu.2	⊢ ( 𝜑 → 𝑉 ≠ 𝑊 )
16		angmndaddeu.3	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
17		angmndaddeu.4	⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
18		angmndaddov1lem.1	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
19	7	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝐺 ∈ TarskiG )
20	8	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑈 ∈ 𝑃 )
21	9	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑉 ∈ 𝑃 )
22	10	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑊 ∈ 𝑃 )
23	11	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑋 ∈ 𝑃 )
24	12	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑌 ∈ 𝑃 )
25	13	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑍 ∈ 𝑃 )
26	14	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑈 ≠ 𝑉 )
27	15	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑉 ≠ 𝑊 )
28	16	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑋 ≠ 𝑌 )
29	17	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑌 ≠ 𝑍 )
30	18	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
31		simpr	⊢ ( ( 𝜑 ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 )
32	1 2 3 4 5 6 19 20 21 22 23 24 25 26 27 28 29 30 31	angmndaddeu2	⊢ ( ( 𝜑 ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )
33	32	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )
34	7	adantr	⊢ ( ( 𝜑 ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝐺 ∈ TarskiG )
35	8	adantr	⊢ ( ( 𝜑 ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑈 ∈ 𝑃 )
36	9	adantr	⊢ ( ( 𝜑 ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑉 ∈ 𝑃 )
37	10	adantr	⊢ ( ( 𝜑 ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑊 ∈ 𝑃 )
38	11	adantr	⊢ ( ( 𝜑 ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑋 ∈ 𝑃 )
39	12	adantr	⊢ ( ( 𝜑 ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑌 ∈ 𝑃 )
40	13	adantr	⊢ ( ( 𝜑 ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑍 ∈ 𝑃 )
41	14	adantr	⊢ ( ( 𝜑 ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑈 ≠ 𝑉 )
42	15	adantr	⊢ ( ( 𝜑 ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑉 ≠ 𝑊 )
43	16	adantr	⊢ ( ( 𝜑 ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑋 ≠ 𝑌 )
44	17	adantr	⊢ ( ( 𝜑 ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑌 ≠ 𝑍 )
45	18	adantr	⊢ ( ( 𝜑 ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
46		simpr	⊢ ( ( 𝜑 ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) )
47	1 4 3 34 37 36 35 46	tgbtwncom	⊢ ( ( 𝜑 ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → 𝑉 ∈ ( 𝑈 𝐼 𝑊 ) )
48	1 2 3 4 5 6 34 35 36 37 38 39 40 41 42 43 44 45 47	angmndaddeu3	⊢ ( ( 𝜑 ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )
49	48	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) ∧ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )
50		eqid	⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
51	10	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑊 ∈ 𝑃 )
52	9	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑉 ∈ 𝑃 )
53	8	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑈 ∈ 𝑃 )
54	7	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝐺 ∈ TarskiG )
55	11	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑋 ∈ 𝑃 )
56	15	necomd	⊢ ( 𝜑 → 𝑊 ≠ 𝑉 )
57	56	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑊 ≠ 𝑉 )
58		simpr	⊢ ( ( 𝜑 ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) )
59	1 3 6 54 51 52 53 57 58	lncom	⊢ ( ( 𝜑 ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑈 ∈ ( 𝑊 𝐿 𝑉 ) )
60	1 3 50 51 52 53 54 55 6 59	lnhl	⊢ ( ( 𝜑 ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → ( 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ∨ 𝑉 ∈ ( 𝑊 𝐼 𝑈 ) ) )
61	33 49 60	mpjaodan	⊢ ( ( 𝜑 ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )
62	7	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝐺 ∈ TarskiG )
63	8	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑈 ∈ 𝑃 )
64	9	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑉 ∈ 𝑃 )
65	10	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑊 ∈ 𝑃 )
66	11	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑋 ∈ 𝑃 )
67	12	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑌 ∈ 𝑃 )
68	13	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑍 ∈ 𝑃 )
69	14	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑈 ≠ 𝑉 )
70	15	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑉 ≠ 𝑊 )
71	16	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑋 ≠ 𝑌 )
72	17	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → 𝑌 ≠ 𝑍 )
73	18	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
74		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) )
75	1 2 3 4 5 6 62 63 64 65 66 67 68 69 70 71 72 73 74	angmndaddeu1	⊢ ( ( 𝜑 ∧ ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )
76	61 75	pm2.61dan	⊢ ( 𝜑 → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )