Theorem axtg5seg 28491

Description: Five segments axiom, Axiom A5 of [Schwabhauser] p. 11. Take two triangles 𝑋𝑍𝑈 and 𝐴𝐶𝑉, a point 𝑌 on 𝑋𝑍, and a point 𝐵 on 𝐴𝐶. If all corresponding line segments except for 𝑍𝑈 and 𝐶𝑉 are congruent ( i.e., 𝑋𝑌 ∼ 𝐴𝐵, 𝑌𝑍 ∼ 𝐵𝐶, 𝑋𝑈 ∼ 𝐴𝑉, and 𝑌𝑈 ∼ 𝐵𝑉), then 𝑍𝑈 and 𝐶𝑉 are also congruent. As noted in Axiom 5 of [Tarski1999] p. 178, "this axiom is similar in character to the well-known theorems of Euclidean geometry that allow one to conclude, from hypotheses about the congruence of certain corresponding sides and angles in two triangles, the congruence of other corresponding sides and angles." (Contributed by Thierry Arnoux, 14-Mar-2019.)

Hypotheses

Ref	Expression
axtrkg.p	⊢ 𝑃 = (Base‘𝐺)
axtrkg.d	⊢ − = (dist‘𝐺)
axtrkg.i	⊢ 𝐼 = (Itv‘𝐺)
axtrkg.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
axtg5seg.1	⊢ (𝜑 → 𝑋 ∈ 𝑃)
axtg5seg.2	⊢ (𝜑 → 𝑌 ∈ 𝑃)
axtg5seg.3	⊢ (𝜑 → 𝑍 ∈ 𝑃)
axtg5seg.4	⊢ (𝜑 → 𝐴 ∈ 𝑃)
axtg5seg.5	⊢ (𝜑 → 𝐵 ∈ 𝑃)
axtg5seg.6	⊢ (𝜑 → 𝐶 ∈ 𝑃)
axtg5seg.7	⊢ (𝜑 → 𝑈 ∈ 𝑃)
axtg5seg.8	⊢ (𝜑 → 𝑉 ∈ 𝑃)
axtg5seg.9	⊢ (𝜑 → 𝑋 ≠ 𝑌)
axtg5seg.10	⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍))
axtg5seg.11	⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))
axtg5seg.12	⊢ (𝜑 → (𝑋 − 𝑌) = (𝐴 − 𝐵))
axtg5seg.13	⊢ (𝜑 → (𝑌 − 𝑍) = (𝐵 − 𝐶))
axtg5seg.14	⊢ (𝜑 → (𝑋 − 𝑈) = (𝐴 − 𝑉))
axtg5seg.15	⊢ (𝜑 → (𝑌 − 𝑈) = (𝐵 − 𝑉))

Assertion

Ref	Expression
axtg5seg	⊢ (𝜑 → (𝑍 − 𝑈) = (𝐶 − 𝑉))

Proof of Theorem axtg5seg

Dummy variables 𝑓 𝑖 𝑝 𝑥 𝑦 𝑧 𝑎 𝑏 𝑐 𝑣 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-trkg 28479	. . . . . . 7 ⊢ TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2		inss2 4259	. . . . . . . 8 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
3		inss1 4258	. . . . . . . 8 ⊢ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) ⊆ TarskiGCB
4	2, 3	sstri 4018	. . . . . . 7 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGCB
5	1, 4	eqsstri 4043	. . . . . 6 ⊢ TarskiG ⊆ TarskiGCB
6		axtrkg.g	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
7	5, 6	sselid 4006	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ TarskiGCB)
8		axtrkg.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
9		axtrkg.d	. . . . . . . 8 ⊢ − = (dist‘𝐺)
10		axtrkg.i	. . . . . . . 8 ⊢ 𝐼 = (Itv‘𝐺)
11	8, 9, 10	istrkgcb 28482	. . . . . . 7 ⊢ (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)))))
12	11	simprbi 496	. . . . . 6 ⊢ (𝐺 ∈ TarskiGCB → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏))))
13	12	simpld 494	. . . . 5 ⊢ (𝐺 ∈ TarskiGCB → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)))
14	7, 13	syl 17	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)))
15		axtg5seg.1	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
16		axtg5seg.2	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
17		axtg5seg.3	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
18		neeq1 3009	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (𝑥 ≠ 𝑦 ↔ 𝑋 ≠ 𝑦))
19		oveq1 7455	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
20	19	eleq2d 2830	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
21	18, 20	3anbi12d 1437	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
22		oveq1 7455	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (𝑥 − 𝑦) = (𝑋 − 𝑦))
23	22	eqeq1d 2742	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → ((𝑥 − 𝑦) = (𝑎 − 𝑏) ↔ (𝑋 − 𝑦) = (𝑎 − 𝑏)))
24	23	anbi1d 630	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐))))
25		oveq1 7455	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (𝑥 − 𝑢) = (𝑋 − 𝑢))
26	25	eqeq1d 2742	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → ((𝑥 − 𝑢) = (𝑎 − 𝑣) ↔ (𝑋 − 𝑢) = (𝑎 − 𝑣)))
27	26	anbi1d 630	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))))
28	24, 27	anbi12d 631	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))))
29	21, 28	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))))))
30	29	imbi1d 341	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → ((((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
31	30	ralbidv 3184	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
32	31	2ralbidv 3227	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
33	32	2ralbidv 3227	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
34		neeq2 3010	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝑋 ≠ 𝑦 ↔ 𝑋 ≠ 𝑌))
35		eleq1 2832	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
36	34, 35	3anbi12d 1437	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
37		oveq2 7456	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → (𝑋 − 𝑦) = (𝑋 − 𝑌))
38	37	eqeq1d 2742	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → ((𝑋 − 𝑦) = (𝑎 − 𝑏) ↔ (𝑋 − 𝑌) = (𝑎 − 𝑏)))
39		oveq1 7455	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → (𝑦 − 𝑧) = (𝑌 − 𝑧))
40	39	eqeq1d 2742	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → ((𝑦 − 𝑧) = (𝑏 − 𝑐) ↔ (𝑌 − 𝑧) = (𝑏 − 𝑐)))
41	38, 40	anbi12d 631	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐))))
42		oveq1 7455	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → (𝑦 − 𝑢) = (𝑌 − 𝑢))
43	42	eqeq1d 2742	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → ((𝑦 − 𝑢) = (𝑏 − 𝑣) ↔ (𝑌 − 𝑢) = (𝑏 − 𝑣)))
44	43	anbi2d 629	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))))
45	41, 44	anbi12d 631	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))))
46	36, 45	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑦 = 𝑌 → (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))))))
47	46	imbi1d 341	. . . . . . . . 9 ⊢ (𝑦 = 𝑌 → ((((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
48	47	ralbidv 3184	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → (∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
49	48	2ralbidv 3227	. . . . . . 7 ⊢ (𝑦 = 𝑌 → (∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
50	49	2ralbidv 3227	. . . . . 6 ⊢ (𝑦 = 𝑌 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
51		oveq2 7456	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑍 → (𝑋𝐼𝑧) = (𝑋𝐼𝑍))
52	51	eleq2d 2830	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑍 → (𝑌 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑍)))
53	52	3anbi2d 1441	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
54		oveq2 7456	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑍 → (𝑌 − 𝑧) = (𝑌 − 𝑍))
55	54	eqeq1d 2742	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑍 → ((𝑌 − 𝑧) = (𝑏 − 𝑐) ↔ (𝑌 − 𝑍) = (𝑏 − 𝑐)))
56	55	anbi2d 629	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑍 → (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐))))
57	56	anbi1d 630	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → ((((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))))
58	53, 57	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))))))
59		oveq1 7455	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → (𝑧 − 𝑢) = (𝑍 − 𝑢))
60	59	eqeq1d 2742	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → ((𝑧 − 𝑢) = (𝑐 − 𝑣) ↔ (𝑍 − 𝑢) = (𝑐 − 𝑣)))
61	58, 60	imbi12d 344	. . . . . . . . 9 ⊢ (𝑧 = 𝑍 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
62	61	ralbidv 3184	. . . . . . . 8 ⊢ (𝑧 = 𝑍 → (∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
63	62	2ralbidv 3227	. . . . . . 7 ⊢ (𝑧 = 𝑍 → (∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
64	63	2ralbidv 3227	. . . . . 6 ⊢ (𝑧 = 𝑍 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
65	33, 50, 64	rspc3v 3651	. . . . 5 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) → ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
66	15, 16, 17, 65	syl3anc 1371	. . . 4 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) → ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
67	14, 66	mpd 15	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)))
68		axtg5seg.7	. . . 4 ⊢ (𝜑 → 𝑈 ∈ 𝑃)
69		axtg5seg.4	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
70		axtg5seg.5	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
71		oveq2 7456	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑈 → (𝑋 − 𝑢) = (𝑋 − 𝑈))
72	71	eqeq1d 2742	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 → ((𝑋 − 𝑢) = (𝑎 − 𝑣) ↔ (𝑋 − 𝑈) = (𝑎 − 𝑣)))
73		oveq2 7456	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑈 → (𝑌 − 𝑢) = (𝑌 − 𝑈))
74	73	eqeq1d 2742	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 → ((𝑌 − 𝑢) = (𝑏 − 𝑣) ↔ (𝑌 − 𝑈) = (𝑏 − 𝑣)))
75	72, 74	anbi12d 631	. . . . . . . . 9 ⊢ (𝑢 = 𝑈 → (((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))
76	75	anbi2d 629	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → ((((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))))
77	76	anbi2d 629	. . . . . . 7 ⊢ (𝑢 = 𝑈 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))))
78		oveq2 7456	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → (𝑍 − 𝑢) = (𝑍 − 𝑈))
79	78	eqeq1d 2742	. . . . . . 7 ⊢ (𝑢 = 𝑈 → ((𝑍 − 𝑢) = (𝑐 − 𝑣) ↔ (𝑍 − 𝑈) = (𝑐 − 𝑣)))
80	77, 79	imbi12d 344	. . . . . 6 ⊢ (𝑢 = 𝑈 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
81	80	2ralbidv 3227	. . . . 5 ⊢ (𝑢 = 𝑈 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
82		oveq1 7455	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → (𝑎𝐼𝑐) = (𝐴𝐼𝑐))
83	82	eleq2d 2830	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (𝑏 ∈ (𝑎𝐼𝑐) ↔ 𝑏 ∈ (𝐴𝐼𝑐)))
84	83	3anbi3d 1442	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐))))
85		oveq1 7455	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝑎 − 𝑏) = (𝐴 − 𝑏))
86	85	eqeq2d 2751	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((𝑋 − 𝑌) = (𝑎 − 𝑏) ↔ (𝑋 − 𝑌) = (𝐴 − 𝑏)))
87	86	anbi1d 630	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐))))
88		oveq1 7455	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝑎 − 𝑣) = (𝐴 − 𝑣))
89	88	eqeq2d 2751	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((𝑋 − 𝑈) = (𝑎 − 𝑣) ↔ (𝑋 − 𝑈) = (𝐴 − 𝑣)))
90	89	anbi1d 630	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))
91	87, 90	anbi12d 631	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ((((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))))
92	84, 91	anbi12d 631	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))))
93	92	imbi1d 341	. . . . . 6 ⊢ (𝑎 = 𝐴 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
94	93	2ralbidv 3227	. . . . 5 ⊢ (𝑎 = 𝐴 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
95		eleq1 2832	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (𝑏 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝑐)))
96	95	3anbi3d 1442	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐))))
97		oveq2 7456	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝐴 − 𝑏) = (𝐴 − 𝐵))
98	97	eqeq2d 2751	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑋 − 𝑌) = (𝐴 − 𝑏) ↔ (𝑋 − 𝑌) = (𝐴 − 𝐵)))
99		oveq1 7455	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝑏 − 𝑐) = (𝐵 − 𝑐))
100	99	eqeq2d 2751	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑌 − 𝑍) = (𝑏 − 𝑐) ↔ (𝑌 − 𝑍) = (𝐵 − 𝑐)))
101	98, 100	anbi12d 631	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐))))
102		oveq1 7455	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝑏 − 𝑣) = (𝐵 − 𝑣))
103	102	eqeq2d 2751	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑌 − 𝑈) = (𝑏 − 𝑣) ↔ (𝑌 − 𝑈) = (𝐵 − 𝑣)))
104	103	anbi2d 629	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))))
105	101, 104	anbi12d 631	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ((((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))))
106	96, 105	anbi12d 631	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))))))
107	106	imbi1d 341	. . . . . 6 ⊢ (𝑏 = 𝐵 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
108	107	2ralbidv 3227	. . . . 5 ⊢ (𝑏 = 𝐵 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
109	81, 94, 108	rspc3v 3651	. . . 4 ⊢ ((𝑈 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) → ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
110	68, 69, 70, 109	syl3anc 1371	. . 3 ⊢ (𝜑 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) → ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
111	67, 110	mpd 15	. 2 ⊢ (𝜑 → ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)))
112		axtg5seg.9	. . . 4 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
113		axtg5seg.10	. . . 4 ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍))
114		axtg5seg.11	. . . 4 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))
115	112, 113, 114	3jca 1128	. . 3 ⊢ (𝜑 → (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)))
116		axtg5seg.12	. . . 4 ⊢ (𝜑 → (𝑋 − 𝑌) = (𝐴 − 𝐵))
117		axtg5seg.13	. . . 4 ⊢ (𝜑 → (𝑌 − 𝑍) = (𝐵 − 𝐶))
118	116, 117	jca 511	. . 3 ⊢ (𝜑 → ((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)))
119		axtg5seg.14	. . . 4 ⊢ (𝜑 → (𝑋 − 𝑈) = (𝐴 − 𝑉))
120		axtg5seg.15	. . . 4 ⊢ (𝜑 → (𝑌 − 𝑈) = (𝐵 − 𝑉))
121	119, 120	jca 511	. . 3 ⊢ (𝜑 → ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))
122	115, 118, 121	jca32 515	. 2 ⊢ (𝜑 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))))
123		axtg5seg.6	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
124		axtg5seg.8	. . 3 ⊢ (𝜑 → 𝑉 ∈ 𝑃)
125		oveq2 7456	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝐴𝐼𝑐) = (𝐴𝐼𝐶))
126	125	eleq2d 2830	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (𝐵 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝐶)))
127	126	3anbi3d 1442	. . . . . 6 ⊢ (𝑐 = 𝐶 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶))))
128		oveq2 7456	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (𝐵 − 𝑐) = (𝐵 − 𝐶))
129	128	eqeq2d 2751	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → ((𝑌 − 𝑍) = (𝐵 − 𝑐) ↔ (𝑌 − 𝑍) = (𝐵 − 𝐶)))
130	129	anbi2d 629	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶))))
131	130	anbi1d 630	. . . . . 6 ⊢ (𝑐 = 𝐶 → ((((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))))
132	127, 131	anbi12d 631	. . . . 5 ⊢ (𝑐 = 𝐶 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))))))
133		oveq1 7455	. . . . . 6 ⊢ (𝑐 = 𝐶 → (𝑐 − 𝑣) = (𝐶 − 𝑣))
134	133	eqeq2d 2751	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝑍 − 𝑈) = (𝑐 − 𝑣) ↔ (𝑍 − 𝑈) = (𝐶 − 𝑣)))
135	132, 134	imbi12d 344	. . . 4 ⊢ (𝑐 = 𝐶 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝐶 − 𝑣))))
136		oveq2 7456	. . . . . . . . 9 ⊢ (𝑣 = 𝑉 → (𝐴 − 𝑣) = (𝐴 − 𝑉))
137	136	eqeq2d 2751	. . . . . . . 8 ⊢ (𝑣 = 𝑉 → ((𝑋 − 𝑈) = (𝐴 − 𝑣) ↔ (𝑋 − 𝑈) = (𝐴 − 𝑉)))
138		oveq2 7456	. . . . . . . . 9 ⊢ (𝑣 = 𝑉 → (𝐵 − 𝑣) = (𝐵 − 𝑉))
139	138	eqeq2d 2751	. . . . . . . 8 ⊢ (𝑣 = 𝑉 → ((𝑌 − 𝑈) = (𝐵 − 𝑣) ↔ (𝑌 − 𝑈) = (𝐵 − 𝑉)))
140	137, 139	anbi12d 631	. . . . . . 7 ⊢ (𝑣 = 𝑉 → (((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉))))
141	140	anbi2d 629	. . . . . 6 ⊢ (𝑣 = 𝑉 → ((((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))))
142	141	anbi2d 629	. . . . 5 ⊢ (𝑣 = 𝑉 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉))))))
143		oveq2 7456	. . . . . 6 ⊢ (𝑣 = 𝑉 → (𝐶 − 𝑣) = (𝐶 − 𝑉))
144	143	eqeq2d 2751	. . . . 5 ⊢ (𝑣 = 𝑉 → ((𝑍 − 𝑈) = (𝐶 − 𝑣) ↔ (𝑍 − 𝑈) = (𝐶 − 𝑉)))
145	142, 144	imbi12d 344	. . . 4 ⊢ (𝑣 = 𝑉 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝐶 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))) → (𝑍 − 𝑈) = (𝐶 − 𝑉))))
146	135, 145	rspc2v 3646	. . 3 ⊢ ((𝐶 ∈ 𝑃 ∧ 𝑉 ∈ 𝑃) → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))) → (𝑍 − 𝑈) = (𝐶 − 𝑉))))
147	123, 124, 146	syl2anc 583	. 2 ⊢ (𝜑 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))) → (𝑍 − 𝑈) = (𝐶 − 𝑉))))
148	111, 122, 147	mp2d 49	1 ⊢ (𝜑 → (𝑍 − 𝑈) = (𝐶 − 𝑉))

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1086   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  {cab 2717   ≠ wne 2946  ∀wral 3067  ∃wrex 3076  {crab 3443  Vcvv 3488  [wsbc 3804   ∖ cdif 3973   ∩ cin 3975  {csn 4648  ‘cfv 6573  (class class class)co 7448   ∈ cmpo 7450  Basecbs 17258  distcds 17320  TarskiGcstrkg 28453  TarskiG_Ccstrkgc 28454  TarskiG_Bcstrkgb 28455  TarskiG_CBcstrkgcb 28456  Itvcitv 28459  LineGclng 28460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-trkgcb 28476  df-trkg 28479

This theorem is referenced by:  tgcgrextend  28511  tgsegconeq  28512  tgifscgr  28534  tgfscgr  28594  tgbtwnconn1lem2  28599  tgbtwnconn1lem3  28600  miriso  28696  midexlem  28718  ragcgr  28733  footexALT  28744  footexlem1  28745  footexlem2  28746  lmiisolem  28822  f1otrg  28897  tg5segofs  34650