Metamath Proof Explorer

Theorem axtg5seg

Description: Five segments axiom, Axiom A5 of Schwabhauser p. 11. Take two triangles X Z U and A C V , a point Y on X Z , and a point B on A C . If all corresponding line segments except for Z U and C V are congruent ( i.e., X Y .A B , Y Z .B C , X U .A V , and Y U .B V ), then Z U and C V 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)

Ref Expression
Hypotheses 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 axtg5seg ( 𝜑 → ( 𝑍 − 𝑈 ) = ( 𝐶 − 𝑉 ) )

Proof

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