Theorem axtg5seg 28936

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 28924	. . . . . . 7 ⊢ TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2		inss2 4133	. . . . . . . 8 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
3		inss1 4132	. . . . . . . 8 ⊢ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) ⊆ TarskiGCB
4	2, 3	sstri 3918	. . . . . . 7 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGCB
5	1, 4	eqsstri 3955	. . . . . 6 ⊢ TarskiG ⊆ TarskiGCB
6		axtrkg.g	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
7	5, 6	sselid 3907	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ TarskiGCB)
8		axtrkg.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
9		axtrkg.d	. . . . . . . 8 ⊢ − = (dist‘𝐺)
10		axtrkg.i	. . . . . . . 8 ⊢ 𝐼 = (Itv‘𝐺)
11	8, 9, 10	istrkgcb 28927	. . . . . . 7 ⊢ (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)))))
12	11	simprbi 503	. . . . . 6 ⊢ (𝐺 ∈ TarskiGCB → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏))))
13	12	simpld 500	. . . . 5 ⊢ (𝐺 ∈ TarskiGCB → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)))
14	7, 13	syl 18	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)))
15		axtg5seg.1	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
16		axtg5seg.2	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
17		axtg5seg.3	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
18		neeq1 3017	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (𝑥 ≠ 𝑦 ↔ 𝑋 ≠ 𝑦))
19		oveq1 7431	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
20	19	eleq2d 2846	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
21	18, 20	3anbi12d 1465	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
22		oveq1 7431	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (𝑥 − 𝑦) = (𝑋 − 𝑦))
23	22	eqeq1d 2762	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → ((𝑥 − 𝑦) = (𝑎 − 𝑏) ↔ (𝑋 − 𝑦) = (𝑎 − 𝑏)))
24	23	anbi1d 643	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐))))
25		oveq1 7431	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (𝑥 − 𝑢) = (𝑋 − 𝑢))
26	25	eqeq1d 2762	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → ((𝑥 − 𝑢) = (𝑎 − 𝑣) ↔ (𝑋 − 𝑢) = (𝑎 − 𝑣)))
27	26	anbi1d 643	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))))
28	24, 27	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))))
29	21, 28	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))))))
30	29	imbi1d 344	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → ((((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
31	30	ralbidv 3185	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
32	31	2ralbidv 3226	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
33	32	2ralbidv 3226	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
34		neeq2 3018	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝑋 ≠ 𝑦 ↔ 𝑋 ≠ 𝑌))
35		eleq1 2848	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
36	34, 35	3anbi12d 1465	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
37		oveq2 7432	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → (𝑋 − 𝑦) = (𝑋 − 𝑌))
38	37	eqeq1d 2762	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → ((𝑋 − 𝑦) = (𝑎 − 𝑏) ↔ (𝑋 − 𝑌) = (𝑎 − 𝑏)))
39		oveq1 7431	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → (𝑦 − 𝑧) = (𝑌 − 𝑧))
40	39	eqeq1d 2762	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → ((𝑦 − 𝑧) = (𝑏 − 𝑐) ↔ (𝑌 − 𝑧) = (𝑏 − 𝑐)))
41	38, 40	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐))))
42		oveq1 7431	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → (𝑦 − 𝑢) = (𝑌 − 𝑢))
43	42	eqeq1d 2762	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → ((𝑦 − 𝑢) = (𝑏 − 𝑣) ↔ (𝑌 − 𝑢) = (𝑏 − 𝑣)))
44	43	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))))
45	41, 44	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))))
46	36, 45	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑦 = 𝑌 → (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))))))
47	46	imbi1d 344	. . . . . . . . 9 ⊢ (𝑦 = 𝑌 → ((((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
48	47	ralbidv 3185	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → (∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
49	48	2ralbidv 3226	. . . . . . 7 ⊢ (𝑦 = 𝑌 → (∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
50	49	2ralbidv 3226	. . . . . 6 ⊢ (𝑦 = 𝑌 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
51		oveq2 7432	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑍 → (𝑋𝐼𝑧) = (𝑋𝐼𝑍))
52	51	eleq2d 2846	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑍 → (𝑌 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑍)))
53	52	3anbi2d 1469	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
54		oveq2 7432	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑍 → (𝑌 − 𝑧) = (𝑌 − 𝑍))
55	54	eqeq1d 2762	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑍 → ((𝑌 − 𝑧) = (𝑏 − 𝑐) ↔ (𝑌 − 𝑍) = (𝑏 − 𝑐)))
56	55	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑍 → (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐))))
57	56	anbi1d 643	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → ((((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))))
58	53, 57	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))))))
59		oveq1 7431	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → (𝑧 − 𝑢) = (𝑍 − 𝑢))
60	59	eqeq1d 2762	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → ((𝑧 − 𝑢) = (𝑐 − 𝑣) ↔ (𝑍 − 𝑢) = (𝑐 − 𝑣)))
61	58, 60	imbi12d 347	. . . . . . . . 9 ⊢ (𝑧 = 𝑍 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
62	61	ralbidv 3185	. . . . . . . 8 ⊢ (𝑧 = 𝑍 → (∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
63	62	2ralbidv 3226	. . . . . . 7 ⊢ (𝑧 = 𝑍 → (∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
64	63	2ralbidv 3226	. . . . . 6 ⊢ (𝑧 = 𝑍 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
65	33, 50, 64	rspc3v 3591	. . . . 5 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) → ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
66	15, 16, 17, 65	syl3anc 1398	. . . 4 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) → ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
67	14, 66	mpd 16	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)))
68		axtg5seg.7	. . . 4 ⊢ (𝜑 → 𝑈 ∈ 𝑃)
69		axtg5seg.4	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
70		axtg5seg.5	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
71		oveq2 7432	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑈 → (𝑋 − 𝑢) = (𝑋 − 𝑈))
72	71	eqeq1d 2762	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 → ((𝑋 − 𝑢) = (𝑎 − 𝑣) ↔ (𝑋 − 𝑈) = (𝑎 − 𝑣)))
73		oveq2 7432	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑈 → (𝑌 − 𝑢) = (𝑌 − 𝑈))
74	73	eqeq1d 2762	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 → ((𝑌 − 𝑢) = (𝑏 − 𝑣) ↔ (𝑌 − 𝑈) = (𝑏 − 𝑣)))
75	72, 74	anbi12d 644	. . . . . . . . 9 ⊢ (𝑢 = 𝑈 → (((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))
76	75	anbi2d 642	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → ((((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))))
77	76	anbi2d 642	. . . . . . 7 ⊢ (𝑢 = 𝑈 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))))
78		oveq2 7432	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → (𝑍 − 𝑢) = (𝑍 − 𝑈))
79	78	eqeq1d 2762	. . . . . . 7 ⊢ (𝑢 = 𝑈 → ((𝑍 − 𝑢) = (𝑐 − 𝑣) ↔ (𝑍 − 𝑈) = (𝑐 − 𝑣)))
80	77, 79	imbi12d 347	. . . . . 6 ⊢ (𝑢 = 𝑈 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
81	80	2ralbidv 3226	. . . . 5 ⊢ (𝑢 = 𝑈 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
82		oveq1 7431	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → (𝑎𝐼𝑐) = (𝐴𝐼𝑐))
83	82	eleq2d 2846	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (𝑏 ∈ (𝑎𝐼𝑐) ↔ 𝑏 ∈ (𝐴𝐼𝑐)))
84	83	3anbi3d 1470	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐))))
85		oveq1 7431	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝑎 − 𝑏) = (𝐴 − 𝑏))
86	85	eqeq2d 2771	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((𝑋 − 𝑌) = (𝑎 − 𝑏) ↔ (𝑋 − 𝑌) = (𝐴 − 𝑏)))
87	86	anbi1d 643	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐))))
88		oveq1 7431	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝑎 − 𝑣) = (𝐴 − 𝑣))
89	88	eqeq2d 2771	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((𝑋 − 𝑈) = (𝑎 − 𝑣) ↔ (𝑋 − 𝑈) = (𝐴 − 𝑣)))
90	89	anbi1d 643	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))
91	87, 90	anbi12d 644	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ((((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))))
92	84, 91	anbi12d 644	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))))
93	92	imbi1d 344	. . . . . 6 ⊢ (𝑎 = 𝐴 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
94	93	2ralbidv 3226	. . . . 5 ⊢ (𝑎 = 𝐴 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
95		eleq1 2848	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (𝑏 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝑐)))
96	95	3anbi3d 1470	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐))))
97		oveq2 7432	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝐴 − 𝑏) = (𝐴 − 𝐵))
98	97	eqeq2d 2771	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑋 − 𝑌) = (𝐴 − 𝑏) ↔ (𝑋 − 𝑌) = (𝐴 − 𝐵)))
99		oveq1 7431	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝑏 − 𝑐) = (𝐵 − 𝑐))
100	99	eqeq2d 2771	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑌 − 𝑍) = (𝑏 − 𝑐) ↔ (𝑌 − 𝑍) = (𝐵 − 𝑐)))
101	98, 100	anbi12d 644	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐))))
102		oveq1 7431	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝑏 − 𝑣) = (𝐵 − 𝑣))
103	102	eqeq2d 2771	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑌 − 𝑈) = (𝑏 − 𝑣) ↔ (𝑌 − 𝑈) = (𝐵 − 𝑣)))
104	103	anbi2d 642	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))))
105	101, 104	anbi12d 644	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ((((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))))
106	96, 105	anbi12d 644	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))))))
107	106	imbi1d 344	. . . . . 6 ⊢ (𝑏 = 𝐵 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
108	107	2ralbidv 3226	. . . . 5 ⊢ (𝑏 = 𝐵 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
109	81, 94, 108	rspc3v 3591	. . . 4 ⊢ ((𝑈 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) → ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
110	68, 69, 70, 109	syl3anc 1398	. . 3 ⊢ (𝜑 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) → ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
111	67, 110	mpd 16	. 2 ⊢ (𝜑 → ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)))
112		axtg5seg.9	. . . 4 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
113		axtg5seg.10	. . . 4 ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍))
114		axtg5seg.11	. . . 4 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))
115	112, 113, 114	3jca 1146	. . 3 ⊢ (𝜑 → (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)))
116		axtg5seg.12	. . . 4 ⊢ (𝜑 → (𝑋 − 𝑌) = (𝐴 − 𝐵))
117		axtg5seg.13	. . . 4 ⊢ (𝜑 → (𝑌 − 𝑍) = (𝐵 − 𝐶))
118	116, 117	jca 521	. . 3 ⊢ (𝜑 → ((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)))
119		axtg5seg.14	. . . 4 ⊢ (𝜑 → (𝑋 − 𝑈) = (𝐴 − 𝑉))
120		axtg5seg.15	. . . 4 ⊢ (𝜑 → (𝑌 − 𝑈) = (𝐵 − 𝑉))
121	119, 120	jca 521	. . 3 ⊢ (𝜑 → ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))
122	115, 118, 121	jca32 525	. 2 ⊢ (𝜑 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))))
123		axtg5seg.6	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
124		axtg5seg.8	. . 3 ⊢ (𝜑 → 𝑉 ∈ 𝑃)
125		oveq2 7432	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝐴𝐼𝑐) = (𝐴𝐼𝐶))
126	125	eleq2d 2846	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (𝐵 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝐶)))
127	126	3anbi3d 1470	. . . . . 6 ⊢ (𝑐 = 𝐶 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶))))
128		oveq2 7432	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (𝐵 − 𝑐) = (𝐵 − 𝐶))
129	128	eqeq2d 2771	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → ((𝑌 − 𝑍) = (𝐵 − 𝑐) ↔ (𝑌 − 𝑍) = (𝐵 − 𝐶)))
130	129	anbi2d 642	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶))))
131	130	anbi1d 643	. . . . . 6 ⊢ (𝑐 = 𝐶 → ((((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))))
132	127, 131	anbi12d 644	. . . . 5 ⊢ (𝑐 = 𝐶 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))))))
133		oveq1 7431	. . . . . 6 ⊢ (𝑐 = 𝐶 → (𝑐 − 𝑣) = (𝐶 − 𝑣))
134	133	eqeq2d 2771	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝑍 − 𝑈) = (𝑐 − 𝑣) ↔ (𝑍 − 𝑈) = (𝐶 − 𝑣)))
135	132, 134	imbi12d 347	. . . 4 ⊢ (𝑐 = 𝐶 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝐶 − 𝑣))))
136		oveq2 7432	. . . . . . . . 9 ⊢ (𝑣 = 𝑉 → (𝐴 − 𝑣) = (𝐴 − 𝑉))
137	136	eqeq2d 2771	. . . . . . . 8 ⊢ (𝑣 = 𝑉 → ((𝑋 − 𝑈) = (𝐴 − 𝑣) ↔ (𝑋 − 𝑈) = (𝐴 − 𝑉)))
138		oveq2 7432	. . . . . . . . 9 ⊢ (𝑣 = 𝑉 → (𝐵 − 𝑣) = (𝐵 − 𝑉))
139	138	eqeq2d 2771	. . . . . . . 8 ⊢ (𝑣 = 𝑉 → ((𝑌 − 𝑈) = (𝐵 − 𝑣) ↔ (𝑌 − 𝑈) = (𝐵 − 𝑉)))
140	137, 139	anbi12d 644	. . . . . . 7 ⊢ (𝑣 = 𝑉 → (((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉))))
141	140	anbi2d 642	. . . . . 6 ⊢ (𝑣 = 𝑉 → ((((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))))
142	141	anbi2d 642	. . . . 5 ⊢ (𝑣 = 𝑉 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉))))))
143		oveq2 7432	. . . . . 6 ⊢ (𝑣 = 𝑉 → (𝐶 − 𝑣) = (𝐶 − 𝑉))
144	143	eqeq2d 2771	. . . . 5 ⊢ (𝑣 = 𝑉 → ((𝑍 − 𝑈) = (𝐶 − 𝑣) ↔ (𝑍 − 𝑈) = (𝐶 − 𝑉)))
145	142, 144	imbi12d 347	. . . 4 ⊢ (𝑣 = 𝑉 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝐶 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))) → (𝑍 − 𝑈) = (𝐶 − 𝑉))))
146	135, 145	rspc2v 3586	. . 3 ⊢ ((𝐶 ∈ 𝑃 ∧ 𝑉 ∈ 𝑃) → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))) → (𝑍 − 𝑈) = (𝐶 − 𝑉))))
147	123, 124, 146	syl2anc 596	. 2 ⊢ (𝜑 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))) → (𝑍 − 𝑈) = (𝐶 − 𝑉))))
148	111, 122, 147	mp2d 50	1 ⊢ (𝜑 → (𝑍 − 𝑈) = (𝐶 − 𝑉))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ w3o 1102   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  {cab 2738   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450  [wsbc 3738   ∖ cdif 4044   ∩ cin 4088  {csn 4584  ‘cfv 6543  (class class class)co 7424   ∈ cmpo 7426  Basecbs 17396  distcds 17446  TarskiGcstrkg 28898  TarskiG_Ccstrkgc 28899  TarskiG_Bcstrkgb 28900  TarskiG_CBcstrkgcb 28901  Itvcitv 28904  LineGclng 28905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427  df-trkgcb 28921  df-trkg 28924

This theorem is used by:  tgcgrextend  28956  tgsegconeq  28957  tgifscgr  28980  tgfscgr  29040  tgbtwnconn1lem2  29045  tgbtwnconn1lem3  29046  miriso  29151  midexlem  29173  ragcgr  29191  footexALT  29202  footexlem1  29203  footexlem2  29204  lmiisolem  29310  tgaaddcpbllem1  29358  f1otrg  29457  tg5segofs  35355