Theorem axtg5seg 26510

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 26498	. . . . . . 7 ⊢ TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2		inss2 4130	. . . . . . . 8 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
3		inss1 4129	. . . . . . . 8 ⊢ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) ⊆ TarskiGCB
4	2, 3	sstri 3896	. . . . . . 7 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGCB
5	1, 4	eqsstri 3921	. . . . . 6 ⊢ TarskiG ⊆ TarskiGCB
6		axtrkg.g	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
7	5, 6	sseldi 3885	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ TarskiGCB)
8		axtrkg.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
9		axtrkg.d	. . . . . . . 8 ⊢ − = (dist‘𝐺)
10		axtrkg.i	. . . . . . . 8 ⊢ 𝐼 = (Itv‘𝐺)
11	8, 9, 10	istrkgcb 26501	. . . . . . 7 ⊢ (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)))))
12	11	simprbi 500	. . . . . 6 ⊢ (𝐺 ∈ TarskiGCB → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏))))
13	12	simpld 498	. . . . 5 ⊢ (𝐺 ∈ TarskiGCB → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)))
14	7, 13	syl 17	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)))
15		axtg5seg.1	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
16		axtg5seg.2	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
17		axtg5seg.3	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
18		neeq1 2994	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (𝑥 ≠ 𝑦 ↔ 𝑋 ≠ 𝑦))
19		oveq1 7198	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
20	19	eleq2d 2816	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
21	18, 20	3anbi12d 1439	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
22		oveq1 7198	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (𝑥 − 𝑦) = (𝑋 − 𝑦))
23	22	eqeq1d 2738	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → ((𝑥 − 𝑦) = (𝑎 − 𝑏) ↔ (𝑋 − 𝑦) = (𝑎 − 𝑏)))
24	23	anbi1d 633	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐))))
25		oveq1 7198	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (𝑥 − 𝑢) = (𝑋 − 𝑢))
26	25	eqeq1d 2738	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → ((𝑥 − 𝑢) = (𝑎 − 𝑣) ↔ (𝑋 − 𝑢) = (𝑎 − 𝑣)))
27	26	anbi1d 633	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))))
28	24, 27	anbi12d 634	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))))
29	21, 28	anbi12d 634	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))))))
30	29	imbi1d 345	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → ((((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
31	30	ralbidv 3108	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
32	31	2ralbidv 3110	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
33	32	2ralbidv 3110	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
34		neeq2 2995	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝑋 ≠ 𝑦 ↔ 𝑋 ≠ 𝑌))
35		eleq1 2818	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
36	34, 35	3anbi12d 1439	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
37		oveq2 7199	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → (𝑋 − 𝑦) = (𝑋 − 𝑌))
38	37	eqeq1d 2738	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → ((𝑋 − 𝑦) = (𝑎 − 𝑏) ↔ (𝑋 − 𝑌) = (𝑎 − 𝑏)))
39		oveq1 7198	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → (𝑦 − 𝑧) = (𝑌 − 𝑧))
40	39	eqeq1d 2738	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → ((𝑦 − 𝑧) = (𝑏 − 𝑐) ↔ (𝑌 − 𝑧) = (𝑏 − 𝑐)))
41	38, 40	anbi12d 634	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐))))
42		oveq1 7198	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → (𝑦 − 𝑢) = (𝑌 − 𝑢))
43	42	eqeq1d 2738	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → ((𝑦 − 𝑢) = (𝑏 − 𝑣) ↔ (𝑌 − 𝑢) = (𝑏 − 𝑣)))
44	43	anbi2d 632	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))))
45	41, 44	anbi12d 634	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))))
46	36, 45	anbi12d 634	. . . . . . . . . 10 ⊢ (𝑦 = 𝑌 → (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))))))
47	46	imbi1d 345	. . . . . . . . 9 ⊢ (𝑦 = 𝑌 → ((((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
48	47	ralbidv 3108	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → (∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
49	48	2ralbidv 3110	. . . . . . 7 ⊢ (𝑦 = 𝑌 → (∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
50	49	2ralbidv 3110	. . . . . 6 ⊢ (𝑦 = 𝑌 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
51		oveq2 7199	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑍 → (𝑋𝐼𝑧) = (𝑋𝐼𝑍))
52	51	eleq2d 2816	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑍 → (𝑌 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑍)))
53	52	3anbi2d 1443	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
54		oveq2 7199	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑍 → (𝑌 − 𝑧) = (𝑌 − 𝑍))
55	54	eqeq1d 2738	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑍 → ((𝑌 − 𝑧) = (𝑏 − 𝑐) ↔ (𝑌 − 𝑍) = (𝑏 − 𝑐)))
56	55	anbi2d 632	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑍 → (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐))))
57	56	anbi1d 633	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → ((((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))))
58	53, 57	anbi12d 634	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))))))
59		oveq1 7198	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → (𝑧 − 𝑢) = (𝑍 − 𝑢))
60	59	eqeq1d 2738	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → ((𝑧 − 𝑢) = (𝑐 − 𝑣) ↔ (𝑍 − 𝑢) = (𝑐 − 𝑣)))
61	58, 60	imbi12d 348	. . . . . . . . 9 ⊢ (𝑧 = 𝑍 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
62	61	ralbidv 3108	. . . . . . . 8 ⊢ (𝑧 = 𝑍 → (∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
63	62	2ralbidv 3110	. . . . . . 7 ⊢ (𝑧 = 𝑍 → (∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
64	63	2ralbidv 3110	. . . . . 6 ⊢ (𝑧 = 𝑍 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
65	33, 50, 64	rspc3v 3540	. . . . 5 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) → ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
66	15, 16, 17, 65	syl3anc 1373	. . . 4 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) → ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
67	14, 66	mpd 15	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)))
68		axtg5seg.7	. . . 4 ⊢ (𝜑 → 𝑈 ∈ 𝑃)
69		axtg5seg.4	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
70		axtg5seg.5	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
71		oveq2 7199	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑈 → (𝑋 − 𝑢) = (𝑋 − 𝑈))
72	71	eqeq1d 2738	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 → ((𝑋 − 𝑢) = (𝑎 − 𝑣) ↔ (𝑋 − 𝑈) = (𝑎 − 𝑣)))
73		oveq2 7199	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑈 → (𝑌 − 𝑢) = (𝑌 − 𝑈))
74	73	eqeq1d 2738	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 → ((𝑌 − 𝑢) = (𝑏 − 𝑣) ↔ (𝑌 − 𝑈) = (𝑏 − 𝑣)))
75	72, 74	anbi12d 634	. . . . . . . . 9 ⊢ (𝑢 = 𝑈 → (((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))
76	75	anbi2d 632	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → ((((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))))
77	76	anbi2d 632	. . . . . . 7 ⊢ (𝑢 = 𝑈 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))))
78		oveq2 7199	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → (𝑍 − 𝑢) = (𝑍 − 𝑈))
79	78	eqeq1d 2738	. . . . . . 7 ⊢ (𝑢 = 𝑈 → ((𝑍 − 𝑢) = (𝑐 − 𝑣) ↔ (𝑍 − 𝑈) = (𝑐 − 𝑣)))
80	77, 79	imbi12d 348	. . . . . 6 ⊢ (𝑢 = 𝑈 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
81	80	2ralbidv 3110	. . . . 5 ⊢ (𝑢 = 𝑈 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
82		oveq1 7198	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → (𝑎𝐼𝑐) = (𝐴𝐼𝑐))
83	82	eleq2d 2816	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (𝑏 ∈ (𝑎𝐼𝑐) ↔ 𝑏 ∈ (𝐴𝐼𝑐)))
84	83	3anbi3d 1444	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐))))
85		oveq1 7198	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝑎 − 𝑏) = (𝐴 − 𝑏))
86	85	eqeq2d 2747	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((𝑋 − 𝑌) = (𝑎 − 𝑏) ↔ (𝑋 − 𝑌) = (𝐴 − 𝑏)))
87	86	anbi1d 633	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐))))
88		oveq1 7198	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝑎 − 𝑣) = (𝐴 − 𝑣))
89	88	eqeq2d 2747	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((𝑋 − 𝑈) = (𝑎 − 𝑣) ↔ (𝑋 − 𝑈) = (𝐴 − 𝑣)))
90	89	anbi1d 633	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))
91	87, 90	anbi12d 634	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ((((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))))
92	84, 91	anbi12d 634	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))))
93	92	imbi1d 345	. . . . . 6 ⊢ (𝑎 = 𝐴 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
94	93	2ralbidv 3110	. . . . 5 ⊢ (𝑎 = 𝐴 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
95		eleq1 2818	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (𝑏 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝑐)))
96	95	3anbi3d 1444	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐))))
97		oveq2 7199	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝐴 − 𝑏) = (𝐴 − 𝐵))
98	97	eqeq2d 2747	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑋 − 𝑌) = (𝐴 − 𝑏) ↔ (𝑋 − 𝑌) = (𝐴 − 𝐵)))
99		oveq1 7198	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝑏 − 𝑐) = (𝐵 − 𝑐))
100	99	eqeq2d 2747	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑌 − 𝑍) = (𝑏 − 𝑐) ↔ (𝑌 − 𝑍) = (𝐵 − 𝑐)))
101	98, 100	anbi12d 634	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐))))
102		oveq1 7198	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝑏 − 𝑣) = (𝐵 − 𝑣))
103	102	eqeq2d 2747	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑌 − 𝑈) = (𝑏 − 𝑣) ↔ (𝑌 − 𝑈) = (𝐵 − 𝑣)))
104	103	anbi2d 632	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))))
105	101, 104	anbi12d 634	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ((((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))))
106	96, 105	anbi12d 634	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))))))
107	106	imbi1d 345	. . . . . 6 ⊢ (𝑏 = 𝐵 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
108	107	2ralbidv 3110	. . . . 5 ⊢ (𝑏 = 𝐵 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
109	81, 94, 108	rspc3v 3540	. . . 4 ⊢ ((𝑈 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) → ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
110	68, 69, 70, 109	syl3anc 1373	. . 3 ⊢ (𝜑 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) → ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
111	67, 110	mpd 15	. 2 ⊢ (𝜑 → ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)))
112		axtg5seg.9	. . . 4 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
113		axtg5seg.10	. . . 4 ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍))
114		axtg5seg.11	. . . 4 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))
115	112, 113, 114	3jca 1130	. . 3 ⊢ (𝜑 → (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)))
116		axtg5seg.12	. . . 4 ⊢ (𝜑 → (𝑋 − 𝑌) = (𝐴 − 𝐵))
117		axtg5seg.13	. . . 4 ⊢ (𝜑 → (𝑌 − 𝑍) = (𝐵 − 𝐶))
118	116, 117	jca 515	. . 3 ⊢ (𝜑 → ((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)))
119		axtg5seg.14	. . . 4 ⊢ (𝜑 → (𝑋 − 𝑈) = (𝐴 − 𝑉))
120		axtg5seg.15	. . . 4 ⊢ (𝜑 → (𝑌 − 𝑈) = (𝐵 − 𝑉))
121	119, 120	jca 515	. . 3 ⊢ (𝜑 → ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))
122	115, 118, 121	jca32 519	. 2 ⊢ (𝜑 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))))
123		axtg5seg.6	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
124		axtg5seg.8	. . 3 ⊢ (𝜑 → 𝑉 ∈ 𝑃)
125		oveq2 7199	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝐴𝐼𝑐) = (𝐴𝐼𝐶))
126	125	eleq2d 2816	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (𝐵 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝐶)))
127	126	3anbi3d 1444	. . . . . 6 ⊢ (𝑐 = 𝐶 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶))))
128		oveq2 7199	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (𝐵 − 𝑐) = (𝐵 − 𝐶))
129	128	eqeq2d 2747	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → ((𝑌 − 𝑍) = (𝐵 − 𝑐) ↔ (𝑌 − 𝑍) = (𝐵 − 𝐶)))
130	129	anbi2d 632	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶))))
131	130	anbi1d 633	. . . . . 6 ⊢ (𝑐 = 𝐶 → ((((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))))
132	127, 131	anbi12d 634	. . . . 5 ⊢ (𝑐 = 𝐶 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))))))
133		oveq1 7198	. . . . . 6 ⊢ (𝑐 = 𝐶 → (𝑐 − 𝑣) = (𝐶 − 𝑣))
134	133	eqeq2d 2747	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝑍 − 𝑈) = (𝑐 − 𝑣) ↔ (𝑍 − 𝑈) = (𝐶 − 𝑣)))
135	132, 134	imbi12d 348	. . . 4 ⊢ (𝑐 = 𝐶 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝐶 − 𝑣))))
136		oveq2 7199	. . . . . . . . 9 ⊢ (𝑣 = 𝑉 → (𝐴 − 𝑣) = (𝐴 − 𝑉))
137	136	eqeq2d 2747	. . . . . . . 8 ⊢ (𝑣 = 𝑉 → ((𝑋 − 𝑈) = (𝐴 − 𝑣) ↔ (𝑋 − 𝑈) = (𝐴 − 𝑉)))
138		oveq2 7199	. . . . . . . . 9 ⊢ (𝑣 = 𝑉 → (𝐵 − 𝑣) = (𝐵 − 𝑉))
139	138	eqeq2d 2747	. . . . . . . 8 ⊢ (𝑣 = 𝑉 → ((𝑌 − 𝑈) = (𝐵 − 𝑣) ↔ (𝑌 − 𝑈) = (𝐵 − 𝑉)))
140	137, 139	anbi12d 634	. . . . . . 7 ⊢ (𝑣 = 𝑉 → (((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉))))
141	140	anbi2d 632	. . . . . 6 ⊢ (𝑣 = 𝑉 → ((((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))))
142	141	anbi2d 632	. . . . 5 ⊢ (𝑣 = 𝑉 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉))))))
143		oveq2 7199	. . . . . 6 ⊢ (𝑣 = 𝑉 → (𝐶 − 𝑣) = (𝐶 − 𝑉))
144	143	eqeq2d 2747	. . . . 5 ⊢ (𝑣 = 𝑉 → ((𝑍 − 𝑈) = (𝐶 − 𝑣) ↔ (𝑍 − 𝑈) = (𝐶 − 𝑉)))
145	142, 144	imbi12d 348	. . . 4 ⊢ (𝑣 = 𝑉 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝐶 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))) → (𝑍 − 𝑈) = (𝐶 − 𝑉))))
146	135, 145	rspc2v 3537	. . 3 ⊢ ((𝐶 ∈ 𝑃 ∧ 𝑉 ∈ 𝑃) → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))) → (𝑍 − 𝑈) = (𝐶 − 𝑉))))
147	123, 124, 146	syl2anc 587	. 2 ⊢ (𝜑 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))) → (𝑍 − 𝑈) = (𝐶 − 𝑉))))
148	111, 122, 147	mp2d 49	1 ⊢ (𝜑 → (𝑍 − 𝑈) = (𝐶 − 𝑉))

Syntax hints:   → wi 4   ∧ wa 399   ∨ w3o 1088   ∧ w3a 1089   = wceq 1543   ∈ wcel 2112  {cab 2714   ≠ wne 2932  ∀wral 3051  ∃wrex 3052  {crab 3055  Vcvv 3398  [wsbc 3683   ∖ cdif 3850   ∩ cin 3852  {csn 4527  ‘cfv 6358  (class class class)co 7191   ∈ cmpo 7193  Basecbs 16666  distcds 16758  TarskiGcstrkg 26475  TarskiG_Ccstrkgc 26476  TarskiG_Bcstrkgb 26477  TarskiG_CBcstrkgcb 26478  Itvcitv 26481  LineGclng 26482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-nul 5184

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-iota 6316  df-fv 6366  df-ov 7194  df-trkgcb 26495  df-trkg 26498

This theorem is referenced by:  tgcgrextend  26530  tgsegconeq  26531  tgifscgr  26553  tgfscgr  26613  tgbtwnconn1lem2  26618  tgbtwnconn1lem3  26619  miriso  26715  midexlem  26737  ragcgr  26752  footexALT  26763  footexlem1  26764  footexlem2  26765  lmiisolem  26841  f1otrg  26916  tg5segofs  32319