Theorem axtg5seg 28368

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 28356	. . . . . . 7 ⊢ TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2		inss2 4197	. . . . . . . 8 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
3		inss1 4196	. . . . . . . 8 ⊢ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) ⊆ TarskiGCB
4	2, 3	sstri 3953	. . . . . . 7 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGCB
5	1, 4	eqsstri 3990	. . . . . 6 ⊢ TarskiG ⊆ TarskiGCB
6		axtrkg.g	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
7	5, 6	sselid 3941	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ TarskiGCB)
8		axtrkg.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
9		axtrkg.d	. . . . . . . 8 ⊢ − = (dist‘𝐺)
10		axtrkg.i	. . . . . . . 8 ⊢ 𝐼 = (Itv‘𝐺)
11	8, 9, 10	istrkgcb 28359	. . . . . . 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 2987	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (𝑥 ≠ 𝑦 ↔ 𝑋 ≠ 𝑦))
19		oveq1 7376	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
20	19	eleq2d 2814	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
21	18, 20	3anbi12d 1439	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
22		oveq1 7376	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (𝑥 − 𝑦) = (𝑋 − 𝑦))
23	22	eqeq1d 2731	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → ((𝑥 − 𝑦) = (𝑎 − 𝑏) ↔ (𝑋 − 𝑦) = (𝑎 − 𝑏)))
24	23	anbi1d 631	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐))))
25		oveq1 7376	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (𝑥 − 𝑢) = (𝑋 − 𝑢))
26	25	eqeq1d 2731	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → ((𝑥 − 𝑢) = (𝑎 − 𝑣) ↔ (𝑋 − 𝑢) = (𝑎 − 𝑣)))
27	26	anbi1d 631	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))))
28	24, 27	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))))
29	21, 28	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))))))
30	29	imbi1d 341	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → ((((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
31	30	ralbidv 3156	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
32	31	2ralbidv 3199	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
33	32	2ralbidv 3199	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
34		neeq2 2988	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝑋 ≠ 𝑦 ↔ 𝑋 ≠ 𝑌))
35		eleq1 2816	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
36	34, 35	3anbi12d 1439	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
37		oveq2 7377	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → (𝑋 − 𝑦) = (𝑋 − 𝑌))
38	37	eqeq1d 2731	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → ((𝑋 − 𝑦) = (𝑎 − 𝑏) ↔ (𝑋 − 𝑌) = (𝑎 − 𝑏)))
39		oveq1 7376	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → (𝑦 − 𝑧) = (𝑌 − 𝑧))
40	39	eqeq1d 2731	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → ((𝑦 − 𝑧) = (𝑏 − 𝑐) ↔ (𝑌 − 𝑧) = (𝑏 − 𝑐)))
41	38, 40	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐))))
42		oveq1 7376	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → (𝑦 − 𝑢) = (𝑌 − 𝑢))
43	42	eqeq1d 2731	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → ((𝑦 − 𝑢) = (𝑏 − 𝑣) ↔ (𝑌 − 𝑢) = (𝑏 − 𝑣)))
44	43	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))))
45	41, 44	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))))
46	36, 45	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑦 = 𝑌 → (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))))))
47	46	imbi1d 341	. . . . . . . . 9 ⊢ (𝑦 = 𝑌 → ((((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
48	47	ralbidv 3156	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → (∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
49	48	2ralbidv 3199	. . . . . . 7 ⊢ (𝑦 = 𝑌 → (∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
50	49	2ralbidv 3199	. . . . . 6 ⊢ (𝑦 = 𝑌 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑦 ∧ 𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣))))
51		oveq2 7377	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑍 → (𝑋𝐼𝑧) = (𝑋𝐼𝑍))
52	51	eleq2d 2814	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑍 → (𝑌 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑍)))
53	52	3anbi2d 1443	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
54		oveq2 7377	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑍 → (𝑌 − 𝑧) = (𝑌 − 𝑍))
55	54	eqeq1d 2731	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑍 → ((𝑌 − 𝑧) = (𝑏 − 𝑐) ↔ (𝑌 − 𝑍) = (𝑏 − 𝑐)))
56	55	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑍 → (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐))))
57	56	anbi1d 631	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → ((((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))))
58	53, 57	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))))))
59		oveq1 7376	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → (𝑧 − 𝑢) = (𝑍 − 𝑢))
60	59	eqeq1d 2731	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → ((𝑧 − 𝑢) = (𝑐 − 𝑣) ↔ (𝑍 − 𝑢) = (𝑐 − 𝑣)))
61	58, 60	imbi12d 344	. . . . . . . . 9 ⊢ (𝑧 = 𝑍 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
62	61	ralbidv 3156	. . . . . . . 8 ⊢ (𝑧 = 𝑍 → (∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
63	62	2ralbidv 3199	. . . . . . 7 ⊢ (𝑧 = 𝑍 → (∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
64	63	2ralbidv 3199	. . . . . 6 ⊢ (𝑧 = 𝑍 → (∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣))))
65	33, 50, 64	rspc3v 3601	. . . . 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 7377	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑈 → (𝑋 − 𝑢) = (𝑋 − 𝑈))
72	71	eqeq1d 2731	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 → ((𝑋 − 𝑢) = (𝑎 − 𝑣) ↔ (𝑋 − 𝑈) = (𝑎 − 𝑣)))
73		oveq2 7377	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑈 → (𝑌 − 𝑢) = (𝑌 − 𝑈))
74	73	eqeq1d 2731	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 → ((𝑌 − 𝑢) = (𝑏 − 𝑣) ↔ (𝑌 − 𝑈) = (𝑏 − 𝑣)))
75	72, 74	anbi12d 632	. . . . . . . . 9 ⊢ (𝑢 = 𝑈 → (((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))
76	75	anbi2d 630	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → ((((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))))
77	76	anbi2d 630	. . . . . . 7 ⊢ (𝑢 = 𝑈 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))))
78		oveq2 7377	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → (𝑍 − 𝑢) = (𝑍 − 𝑈))
79	78	eqeq1d 2731	. . . . . . 7 ⊢ (𝑢 = 𝑈 → ((𝑍 − 𝑢) = (𝑐 − 𝑣) ↔ (𝑍 − 𝑈) = (𝑐 − 𝑣)))
80	77, 79	imbi12d 344	. . . . . 6 ⊢ (𝑢 = 𝑈 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
81	80	2ralbidv 3199	. . . . 5 ⊢ (𝑢 = 𝑈 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑢) = (𝑏 − 𝑣)))) → (𝑍 − 𝑢) = (𝑐 − 𝑣)) ↔ ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
82		oveq1 7376	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → (𝑎𝐼𝑐) = (𝐴𝐼𝑐))
83	82	eleq2d 2814	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (𝑏 ∈ (𝑎𝐼𝑐) ↔ 𝑏 ∈ (𝐴𝐼𝑐)))
84	83	3anbi3d 1444	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐))))
85		oveq1 7376	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝑎 − 𝑏) = (𝐴 − 𝑏))
86	85	eqeq2d 2740	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((𝑋 − 𝑌) = (𝑎 − 𝑏) ↔ (𝑋 − 𝑌) = (𝐴 − 𝑏)))
87	86	anbi1d 631	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐))))
88		oveq1 7376	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝑎 − 𝑣) = (𝐴 − 𝑣))
89	88	eqeq2d 2740	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((𝑋 − 𝑈) = (𝑎 − 𝑣) ↔ (𝑋 − 𝑈) = (𝐴 − 𝑣)))
90	89	anbi1d 631	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))
91	87, 90	anbi12d 632	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ((((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))))
92	84, 91	anbi12d 632	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))))))
93	92	imbi1d 341	. . . . . 6 ⊢ (𝑎 = 𝐴 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
94	93	2ralbidv 3199	. . . . 5 ⊢ (𝑎 = 𝐴 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝑎 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝑎 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
95		eleq1 2816	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (𝑏 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝑐)))
96	95	3anbi3d 1444	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐))))
97		oveq2 7377	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝐴 − 𝑏) = (𝐴 − 𝐵))
98	97	eqeq2d 2740	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑋 − 𝑌) = (𝐴 − 𝑏) ↔ (𝑋 − 𝑌) = (𝐴 − 𝐵)))
99		oveq1 7376	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝑏 − 𝑐) = (𝐵 − 𝑐))
100	99	eqeq2d 2740	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑌 − 𝑍) = (𝑏 − 𝑐) ↔ (𝑌 − 𝑍) = (𝐵 − 𝑐)))
101	98, 100	anbi12d 632	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐))))
102		oveq1 7376	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝑏 − 𝑣) = (𝐵 − 𝑣))
103	102	eqeq2d 2740	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑌 − 𝑈) = (𝑏 − 𝑣) ↔ (𝑌 − 𝑈) = (𝐵 − 𝑣)))
104	103	anbi2d 630	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))))
105	101, 104	anbi12d 632	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ((((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))))
106	96, 105	anbi12d 632	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))))))
107	106	imbi1d 341	. . . . . 6 ⊢ (𝑏 = 𝐵 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
108	107	2ralbidv 3199	. . . . 5 ⊢ (𝑏 = 𝐵 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝑏) ∧ (𝑌 − 𝑍) = (𝑏 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝑏 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣))))
109	81, 94, 108	rspc3v 3601	. . . 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 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 7377	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝐴𝐼𝑐) = (𝐴𝐼𝐶))
126	125	eleq2d 2814	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (𝐵 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝐶)))
127	126	3anbi3d 1444	. . . . . 6 ⊢ (𝑐 = 𝐶 → ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ↔ (𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶))))
128		oveq2 7377	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (𝐵 − 𝑐) = (𝐵 − 𝐶))
129	128	eqeq2d 2740	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → ((𝑌 − 𝑍) = (𝐵 − 𝑐) ↔ (𝑌 − 𝑍) = (𝐵 − 𝐶)))
130	129	anbi2d 630	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ↔ ((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶))))
131	130	anbi1d 631	. . . . . 6 ⊢ (𝑐 = 𝐶 → ((((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))))
132	127, 131	anbi12d 632	. . . . 5 ⊢ (𝑐 = 𝐶 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))))))
133		oveq1 7376	. . . . . 6 ⊢ (𝑐 = 𝐶 → (𝑐 − 𝑣) = (𝐶 − 𝑣))
134	133	eqeq2d 2740	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝑍 − 𝑈) = (𝑐 − 𝑣) ↔ (𝑍 − 𝑈) = (𝐶 − 𝑣)))
135	132, 134	imbi12d 344	. . . 4 ⊢ (𝑐 = 𝐶 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝐶 − 𝑣))))
136		oveq2 7377	. . . . . . . . 9 ⊢ (𝑣 = 𝑉 → (𝐴 − 𝑣) = (𝐴 − 𝑉))
137	136	eqeq2d 2740	. . . . . . . 8 ⊢ (𝑣 = 𝑉 → ((𝑋 − 𝑈) = (𝐴 − 𝑣) ↔ (𝑋 − 𝑈) = (𝐴 − 𝑉)))
138		oveq2 7377	. . . . . . . . 9 ⊢ (𝑣 = 𝑉 → (𝐵 − 𝑣) = (𝐵 − 𝑉))
139	138	eqeq2d 2740	. . . . . . . 8 ⊢ (𝑣 = 𝑉 → ((𝑌 − 𝑈) = (𝐵 − 𝑣) ↔ (𝑌 − 𝑈) = (𝐵 − 𝑉)))
140	137, 139	anbi12d 632	. . . . . . 7 ⊢ (𝑣 = 𝑉 → (((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)) ↔ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉))))
141	140	anbi2d 630	. . . . . 6 ⊢ (𝑣 = 𝑉 → ((((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣))) ↔ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))))
142	141	anbi2d 630	. . . . 5 ⊢ (𝑣 = 𝑉 → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) ↔ ((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉))))))
143		oveq2 7377	. . . . . 6 ⊢ (𝑣 = 𝑉 → (𝐶 − 𝑣) = (𝐶 − 𝑉))
144	143	eqeq2d 2740	. . . . 5 ⊢ (𝑣 = 𝑉 → ((𝑍 − 𝑈) = (𝐶 − 𝑣) ↔ (𝑍 − 𝑈) = (𝐶 − 𝑉)))
145	142, 144	imbi12d 344	. . . 4 ⊢ (𝑣 = 𝑉 → ((((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝐶 − 𝑣)) ↔ (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))) → (𝑍 − 𝑈) = (𝐶 − 𝑉))))
146	135, 145	rspc2v 3596	. . 3 ⊢ ((𝐶 ∈ 𝑃 ∧ 𝑉 ∈ 𝑃) → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))) → (𝑍 − 𝑈) = (𝐶 − 𝑉))))
147	123, 124, 146	syl2anc 584	. 2 ⊢ (𝜑 → (∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝑐)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑣) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑣)))) → (𝑍 − 𝑈) = (𝑐 − 𝑣)) → (((𝑋 ≠ 𝑌 ∧ 𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 − 𝑌) = (𝐴 − 𝐵) ∧ (𝑌 − 𝑍) = (𝐵 − 𝐶)) ∧ ((𝑋 − 𝑈) = (𝐴 − 𝑉) ∧ (𝑌 − 𝑈) = (𝐵 − 𝑉)))) → (𝑍 − 𝑈) = (𝐶 − 𝑉))))
148	111, 122, 147	mp2d 49	1 ⊢ (𝜑 → (𝑍 − 𝑈) = (𝐶 − 𝑉))

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  {cab 2707   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  {crab 3402  Vcvv 3444  [wsbc 3750   ∖ cdif 3908   ∩ cin 3910  {csn 4585  ‘cfv 6499  (class class class)co 7369   ∈ cmpo 7371  Basecbs 17155  distcds 17205  TarskiGcstrkg 28330  TarskiG_Ccstrkgc 28331  TarskiG_Bcstrkgb 28332  TarskiG_CBcstrkgcb 28333  Itvcitv 28336  LineGclng 28337

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5256

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-trkgcb 28353  df-trkg 28356

This theorem is referenced by:  tgcgrextend  28388  tgsegconeq  28389  tgifscgr  28411  tgfscgr  28471  tgbtwnconn1lem2  28476  tgbtwnconn1lem3  28477  miriso  28573  midexlem  28595  ragcgr  28610  footexALT  28621  footexlem1  28622  footexlem2  28623  lmiisolem  28699  f1otrg  28774  tg5segofs  34637