Theorem axtg5seg 26243

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 26231	. . . . . . 7 ⊢ TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2		inss2 4204	. . . . . . . 8 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
3		inss1 4203	. . . . . . . 8 ⊢ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) ⊆ TarskiGCB
4	2, 3	sstri 3974	. . . . . . 7 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGCB
5	1, 4	eqsstri 3999	. . . . . 6 ⊢ TarskiG ⊆ TarskiGCB
6		axtrkg.g	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
7	5, 6	sseldi 3963	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ TarskiGCB)
8		axtrkg.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
9		axtrkg.d	. . . . . . . 8 ⊢ − = (dist‘𝐺)
10		axtrkg.i	. . . . . . . 8 ⊢ 𝐼 = (Itv‘𝐺)
11	8, 9, 10	istrkgcb 26234	. . . . . . 7 ⊢ (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)))))
12	11	simprbi 499	. . . . . 6 ⊢ (𝐺 ∈ TarskiGCB → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏))))
13	12	simpld 497	. . . . 5 ⊢ (𝐺 ∈ TarskiGCB → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)))
14	7, 13	syl 17	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)))
15		axtg5seg.1	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
16		axtg5seg.2	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
17		axtg5seg.3	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
18		neeq1 3076	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (𝑥 ≠ 𝑦 ↔ 𝑋 ≠ 𝑦))
19		oveq1 7155	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
20	19	eleq2d 2896	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
21	18, 20	3anbi12d 1431	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
22		oveq1 7155	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (𝑥 − 𝑦) = (𝑋 − 𝑦))
23	22	eqeq1d 2821	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → ((𝑥 − 𝑦) = (𝑎 − 𝑏) ↔ (𝑋 − 𝑦) = (𝑎 − 𝑏)))
24	23	anbi1d 631	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐))))
25		oveq1 7155	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (𝑥 − 𝑢) = (𝑋 − 𝑢))
26	25	eqeq1d 2821	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → ((𝑥 − 𝑢) = (𝑎 − 𝑣) ↔ (𝑋 − 𝑢) = (𝑎 − 𝑣)))
27	26	anbi1d 631	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))))
28	24, 27	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))))
29	21, 28	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))))))
30	29	imbi1d 344	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → ((((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
31	30	ralbidv 3195	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
32	31	2ralbidv 3197	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
33	32	2ralbidv 3197	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
34		neeq2 3077	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝑋 ≠ 𝑦 ↔ 𝑋 ≠ 𝑌))
35		eleq1 2898	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
36	34, 35	3anbi12d 1431	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
37		oveq2 7156	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → (𝑋 − 𝑦) = (𝑋 − 𝑌))
38	37	eqeq1d 2821	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → ((𝑋 − 𝑦) = (𝑎 − 𝑏) ↔ (𝑋 − 𝑌) = (𝑎 − 𝑏)))
39		oveq1 7155	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → (𝑦 − 𝑧) = (𝑌 − 𝑧))
40	39	eqeq1d 2821	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → ((𝑦 − 𝑧) = (𝑏 − 𝑐) ↔ (𝑌 − 𝑧) = (𝑏 − 𝑐)))
41	38, 40	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐))))
42		oveq1 7155	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → (𝑦 − 𝑢) = (𝑌 − 𝑢))
43	42	eqeq1d 2821	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → ((𝑦 − 𝑢) = (𝑏 − 𝑣) ↔ (𝑌 − 𝑢) = (𝑏 − 𝑣)))
44	43	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))))
45	41, 44	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))))
46	36, 45	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑦 = 𝑌 → (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))))))
47	46	imbi1d 344	. . . . . . . . 9 ⊢ (𝑦 = 𝑌 → ((((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
48	47	ralbidv 3195	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → (∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
49	48	2ralbidv 3197	. . . . . . 7 ⊢ (𝑦 = 𝑌 → (∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
50	49	2ralbidv 3197	. . . . . 6 ⊢ (𝑦 = 𝑌 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
51		oveq2 7156	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑍 → (𝑋𝐼𝑧) = (𝑋𝐼𝑍))
52	51	eleq2d 2896	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑍 → (𝑌 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑍)))
53	52	3anbi2d 1435	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
54		oveq2 7156	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑍 → (𝑌 − 𝑧) = (𝑌 − 𝑍))
55	54	eqeq1d 2821	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑍 → ((𝑌 − 𝑧) = (𝑏 − 𝑐) ↔ (𝑌 − 𝑍) = (𝑏 − 𝑐)))
56	55	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑍 → (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐))))
57	56	anbi1d 631	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → ((((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))))
58	53, 57	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))))))
59		oveq1 7155	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → (𝑧 − 𝑢) = (𝑍 − 𝑢))
60	59	eqeq1d 2821	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → ((𝑧 − 𝑢) = (𝑐 − 𝑣) ↔ (𝑍 − 𝑢) = (𝑐 − 𝑣)))
61	58, 60	imbi12d 347	. . . . . . . . 9 ⊢ (𝑧 = 𝑍 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
62	61	ralbidv 3195	. . . . . . . 8 ⊢ (𝑧 = 𝑍 → (∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
63	62	2ralbidv 3197	. . . . . . 7 ⊢ (𝑧 = 𝑍 → (∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
64	63	2ralbidv 3197	. . . . . 6 ⊢ (𝑧 = 𝑍 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
65	33, 50, 64	rspc3v 3634	. . . . 5 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) → ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
66	15, 16, 17, 65	syl3anc 1366	. . . 4 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) → ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
67	14, 66	mpd 15	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)))
68		axtg5seg.7	. . . 4 ⊢ (𝜑 → 𝑈 ∈ 𝑃)
69		axtg5seg.4	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
70		axtg5seg.5	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
71		oveq2 7156	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑈 → (𝑋 − 𝑢) = (𝑋 − 𝑈))
72	71	eqeq1d 2821	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 → ((𝑋 − 𝑢) = (𝑎 − 𝑣) ↔ (𝑋 − 𝑈) = (𝑎 − 𝑣)))
73		oveq2 7156	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑈 → (𝑌 − 𝑢) = (𝑌 − 𝑈))
74	73	eqeq1d 2821	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 → ((𝑌 − 𝑢) = (𝑏 − 𝑣) ↔ (𝑌 − 𝑈) = (𝑏 − 𝑣)))
75	72, 74	anbi12d 632	. . . . . . . . 9 ⊢ (𝑢 = 𝑈 → (((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))
76	75	anbi2d 630	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → ((((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))))
77	76	anbi2d 630	. . . . . . 7 ⊢ (𝑢 = 𝑈 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))))
78		oveq2 7156	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → (𝑍 − 𝑢) = (𝑍 − 𝑈))
79	78	eqeq1d 2821	. . . . . . 7 ⊢ (𝑢 = 𝑈 → ((𝑍 − 𝑢) = (𝑐 − 𝑣) ↔ (𝑍 − 𝑈) = (𝑐 − 𝑣)))
80	77, 79	imbi12d 347	. . . . . 6 ⊢ (𝑢 = 𝑈 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
81	80	2ralbidv 3197	. . . . 5 ⊢ (𝑢 = 𝑈 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
82		oveq1 7155	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → (𝑎𝐼𝑐) = (𝐴𝐼𝑐))
83	82	eleq2d 2896	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (𝑏 ∈ (𝑎𝐼𝑐) ↔ 𝑏 ∈ (𝐴𝐼𝑐)))
84	83	3anbi3d 1436	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐))))
85		oveq1 7155	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝑎 − 𝑏) = (𝐴 − 𝑏))
86	85	eqeq2d 2830	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((𝑋 − 𝑌) = (𝑎 − 𝑏) ↔ (𝑋 − 𝑌) = (𝐴 − 𝑏)))
87	86	anbi1d 631	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐))))
88		oveq1 7155	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝑎 − 𝑣) = (𝐴 − 𝑣))
89	88	eqeq2d 2830	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((𝑋 − 𝑈) = (𝑎 − 𝑣) ↔ (𝑋 − 𝑈) = (𝐴 − 𝑣)))
90	89	anbi1d 631	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))
91	87, 90	anbi12d 632	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ((((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))))
92	84, 91	anbi12d 632	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))))
93	92	imbi1d 344	. . . . . 6 ⊢ (𝑎 = 𝐴 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
94	93	2ralbidv 3197	. . . . 5 ⊢ (𝑎 = 𝐴 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
95		eleq1 2898	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (𝑏 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝑐)))
96	95	3anbi3d 1436	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐))))
97		oveq2 7156	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝐴 − 𝑏) = (𝐴 − 𝐵))
98	97	eqeq2d 2830	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑋 − 𝑌) = (𝐴 − 𝑏) ↔ (𝑋 − 𝑌) = (𝐴 − 𝐵)))
99		oveq1 7155	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝑏 − 𝑐) = (𝐵 − 𝑐))
100	99	eqeq2d 2830	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑌 − 𝑍) = (𝑏 − 𝑐) ↔ (𝑌 − 𝑍) = (𝐵 − 𝑐)))
101	98, 100	anbi12d 632	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐))))
102		oveq1 7155	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝑏 − 𝑣) = (𝐵 − 𝑣))
103	102	eqeq2d 2830	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑌 − 𝑈) = (𝑏 − 𝑣) ↔ (𝑌 − 𝑈) = (𝐵 − 𝑣)))
104	103	anbi2d 630	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))))
105	101, 104	anbi12d 632	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ((((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))))
106	96, 105	anbi12d 632	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))))))
107	106	imbi1d 344	. . . . . 6 ⊢ (𝑏 = 𝐵 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
108	107	2ralbidv 3197	. . . . 5 ⊢ (𝑏 = 𝐵 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
109	81, 94, 108	rspc3v 3634	. . . 4 ⊢ ((𝑈 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) → ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
110	68, 69, 70, 109	syl3anc 1366	. . 3 ⊢ (𝜑 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) → ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
111	67, 110	mpd 15	. 2 ⊢ (𝜑 → ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)))
112		axtg5seg.9	. . . 4 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
113		axtg5seg.10	. . . 4 ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍))
114		axtg5seg.11	. . . 4 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))
115	112, 113, 114	3jca 1123	. . 3 ⊢ (𝜑 → (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)))
116		axtg5seg.12	. . . 4 ⊢ (𝜑 → (𝑋 − 𝑌) = (𝐴 − 𝐵))
117		axtg5seg.13	. . . 4 ⊢ (𝜑 → (𝑌 − 𝑍) = (𝐵 − 𝐶))
118	116, 117	jca 514	. . 3 ⊢ (𝜑 → ((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)))
119		axtg5seg.14	. . . 4 ⊢ (𝜑 → (𝑋 − 𝑈) = (𝐴 − 𝑉))
120		axtg5seg.15	. . . 4 ⊢ (𝜑 → (𝑌 − 𝑈) = (𝐵 − 𝑉))
121	119, 120	jca 514	. . 3 ⊢ (𝜑 → ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))
122	115, 118, 121	jca32 518	. 2 ⊢ (𝜑 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))))
123		axtg5seg.6	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
124		axtg5seg.8	. . 3 ⊢ (𝜑 → 𝑉 ∈ 𝑃)
125		oveq2 7156	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝐴𝐼𝑐) = (𝐴𝐼𝐶))
126	125	eleq2d 2896	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (𝐵 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝐶)))
127	126	3anbi3d 1436	. . . . . 6 ⊢ (𝑐 = 𝐶 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶))))
128		oveq2 7156	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (𝐵 − 𝑐) = (𝐵 − 𝐶))
129	128	eqeq2d 2830	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → ((𝑌 − 𝑍) = (𝐵 − 𝑐) ↔ (𝑌 − 𝑍) = (𝐵 − 𝐶)))
130	129	anbi2d 630	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶))))
131	130	anbi1d 631	. . . . . 6 ⊢ (𝑐 = 𝐶 → ((((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))))
132	127, 131	anbi12d 632	. . . . 5 ⊢ (𝑐 = 𝐶 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))))))
133		oveq1 7155	. . . . . 6 ⊢ (𝑐 = 𝐶 → (𝑐 − 𝑣) = (𝐶 − 𝑣))
134	133	eqeq2d 2830	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝑍 − 𝑈) = (𝑐 − 𝑣) ↔ (𝑍 − 𝑈) = (𝐶 − 𝑣)))
135	132, 134	imbi12d 347	. . . 4 ⊢ (𝑐 = 𝐶 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝐶 − 𝑣))))
136		oveq2 7156	. . . . . . . . 9 ⊢ (𝑣 = 𝑉 → (𝐴 − 𝑣) = (𝐴 − 𝑉))
137	136	eqeq2d 2830	. . . . . . . 8 ⊢ (𝑣 = 𝑉 → ((𝑋 − 𝑈) = (𝐴 − 𝑣) ↔ (𝑋 − 𝑈) = (𝐴 − 𝑉)))
138		oveq2 7156	. . . . . . . . 9 ⊢ (𝑣 = 𝑉 → (𝐵 − 𝑣) = (𝐵 − 𝑉))
139	138	eqeq2d 2830	. . . . . . . 8 ⊢ (𝑣 = 𝑉 → ((𝑌 − 𝑈) = (𝐵 − 𝑣) ↔ (𝑌 − 𝑈) = (𝐵 − 𝑉)))
140	137, 139	anbi12d 632	. . . . . . 7 ⊢ (𝑣 = 𝑉 → (((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉))))
141	140	anbi2d 630	. . . . . 6 ⊢ (𝑣 = 𝑉 → ((((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))))
142	141	anbi2d 630	. . . . 5 ⊢ (𝑣 = 𝑉 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉))))))
143		oveq2 7156	. . . . . 6 ⊢ (𝑣 = 𝑉 → (𝐶 − 𝑣) = (𝐶 − 𝑉))
144	143	eqeq2d 2830	. . . . 5 ⊢ (𝑣 = 𝑉 → ((𝑍 − 𝑈) = (𝐶 − 𝑣) ↔ (𝑍 − 𝑈) = (𝐶 − 𝑉)))
145	142, 144	imbi12d 347	. . . 4 ⊢ (𝑣 = 𝑉 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝐶 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))) → (𝑍 − 𝑈) = (𝐶 − 𝑉))))
146	135, 145	rspc2v 3631	. . 3 ⊢ ((𝐶 ∈ 𝑃 ∧ 𝑉 ∈ 𝑃) → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))) → (𝑍 − 𝑈) = (𝐶 − 𝑉))))
147	123, 124, 146	syl2anc 586	. 2 ⊢ (𝜑 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))) → (𝑍 − 𝑈) = (𝐶 − 𝑉))))
148	111, 122, 147	mp2d 49	1 ⊢ (𝜑 → (𝑍 − 𝑈) = (𝐶 − 𝑉))

Syntax hints:   → wi 4   ∧ wa 398   ∨ w3o 1081   ∧ w3a 1082   = wceq 1531   ∈ wcel 2108  {cab 2797   ≠ wne 3014  ∀wral 3136  ∃wrex 3137  {crab 3140  Vcvv 3493  [wsbc 3770   ∖ cdif 3931   ∩ cin 3933  {csn 4559  ‘cfv 6348  (class class class)co 7148   ∈ cmpo 7150  Basecbs 16475  distcds 16566  TarskiGcstrkg 26208  TarskiG_Ccstrkgc 26209  TarskiG_Bcstrkgb 26210  TarskiG_CBcstrkgcb 26211  Itvcitv 26214  LineGclng 26215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-nul 5201

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7151  df-trkgcb 26228  df-trkg 26231

This theorem is referenced by:  tgcgrextend  26263  tgsegconeq  26264  tgifscgr  26286  tgfscgr  26346  tgbtwnconn1lem2  26351  tgbtwnconn1lem3  26352  miriso  26448  midexlem  26470  ragcgr  26485  footexALT  26496  footexlem1  26497  footexlem2  26498  lmiisolem  26574  f1otrg  26649  tg5segofs  31937