MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axtg5seg Structured version   Visualization version   GIF version

Theorem axtg5seg 25584
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.
StepHypRef Expression
1 df-trkg 25572 . . . . . . 7 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2 inss2 4037 . . . . . . . 8 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
3 inss1 4036 . . . . . . . 8 (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) ⊆ TarskiGCB
42, 3sstri 3814 . . . . . . 7 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGCB
51, 4eqsstri 3839 . . . . . 6 TarskiG ⊆ TarskiGCB
6 axtrkg.g . . . . . 6 (𝜑𝐺 ∈ TarskiG)
75, 6sseldi 3803 . . . . 5 (𝜑𝐺 ∈ TarskiGCB)
8 axtrkg.p . . . . . . . 8 𝑃 = (Base‘𝐺)
9 axtrkg.d . . . . . . . 8 = (dist‘𝐺)
10 axtrkg.i . . . . . . . 8 𝐼 = (Itv‘𝐺)
118, 9, 10istrkgcb 25575 . . . . . . 7 (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)))))
1211simprbi 486 . . . . . 6 (𝐺 ∈ TarskiGCB → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
1312simpld 484 . . . . 5 (𝐺 ∈ TarskiGCB → ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)))
147, 13syl 17 . . . 4 (𝜑 → ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)))
15 axtg5seg.1 . . . . 5 (𝜑𝑋𝑃)
16 axtg5seg.2 . . . . 5 (𝜑𝑌𝑃)
17 axtg5seg.3 . . . . 5 (𝜑𝑍𝑃)
18 neeq1 3047 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑥𝑦𝑋𝑦))
19 oveq1 6884 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
2019eleq2d 2878 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
2118, 203anbi12d 1554 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
22 oveq1 6884 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (𝑥 𝑦) = (𝑋 𝑦))
2322eqeq1d 2815 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → ((𝑥 𝑦) = (𝑎 𝑏) ↔ (𝑋 𝑦) = (𝑎 𝑏)))
2423anbi1d 617 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ↔ ((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐))))
25 oveq1 6884 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (𝑥 𝑢) = (𝑋 𝑢))
2625eqeq1d 2815 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → ((𝑥 𝑢) = (𝑎 𝑣) ↔ (𝑋 𝑢) = (𝑎 𝑣)))
2726anbi1d 617 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)) ↔ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))))
2824, 27anbi12d 618 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))))
2921, 28anbi12d 618 . . . . . . . . . 10 (𝑥 = 𝑋 → (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))))))
3029imbi1d 332 . . . . . . . . 9 (𝑥 = 𝑋 → ((((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
3130ralbidv 3181 . . . . . . . 8 (𝑥 = 𝑋 → (∀𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
32312ralbidv 3184 . . . . . . 7 (𝑥 = 𝑋 → (∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
33322ralbidv 3184 . . . . . 6 (𝑥 = 𝑋 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
34 neeq2 3048 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (𝑋𝑦𝑋𝑌))
35 eleq1 2880 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
3634, 353anbi12d 1554 . . . . . . . . . . 11 (𝑦 = 𝑌 → ((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
37 oveq2 6885 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → (𝑋 𝑦) = (𝑋 𝑌))
3837eqeq1d 2815 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → ((𝑋 𝑦) = (𝑎 𝑏) ↔ (𝑋 𝑌) = (𝑎 𝑏)))
39 oveq1 6884 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → (𝑦 𝑧) = (𝑌 𝑧))
4039eqeq1d 2815 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → ((𝑦 𝑧) = (𝑏 𝑐) ↔ (𝑌 𝑧) = (𝑏 𝑐)))
4138, 40anbi12d 618 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐))))
42 oveq1 6884 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → (𝑦 𝑢) = (𝑌 𝑢))
4342eqeq1d 2815 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → ((𝑦 𝑢) = (𝑏 𝑣) ↔ (𝑌 𝑢) = (𝑏 𝑣)))
4443anbi2d 616 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)) ↔ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))))
4541, 44anbi12d 618 . . . . . . . . . . 11 (𝑦 = 𝑌 → ((((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))))
4636, 45anbi12d 618 . . . . . . . . . 10 (𝑦 = 𝑌 → (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))))))
4746imbi1d 332 . . . . . . . . 9 (𝑦 = 𝑌 → ((((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
4847ralbidv 3181 . . . . . . . 8 (𝑦 = 𝑌 → (∀𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
49482ralbidv 3184 . . . . . . 7 (𝑦 = 𝑌 → (∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
50492ralbidv 3184 . . . . . 6 (𝑦 = 𝑌 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
51 oveq2 6885 . . . . . . . . . . . . 13 (𝑧 = 𝑍 → (𝑋𝐼𝑧) = (𝑋𝐼𝑍))
5251eleq2d 2878 . . . . . . . . . . . 12 (𝑧 = 𝑍 → (𝑌 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑍)))
53523anbi2d 1558 . . . . . . . . . . 11 (𝑧 = 𝑍 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
54 oveq2 6885 . . . . . . . . . . . . . 14 (𝑧 = 𝑍 → (𝑌 𝑧) = (𝑌 𝑍))
5554eqeq1d 2815 . . . . . . . . . . . . 13 (𝑧 = 𝑍 → ((𝑌 𝑧) = (𝑏 𝑐) ↔ (𝑌 𝑍) = (𝑏 𝑐)))
5655anbi2d 616 . . . . . . . . . . . 12 (𝑧 = 𝑍 → (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐))))
5756anbi1d 617 . . . . . . . . . . 11 (𝑧 = 𝑍 → ((((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))))
5853, 57anbi12d 618 . . . . . . . . . 10 (𝑧 = 𝑍 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))))))
59 oveq1 6884 . . . . . . . . . . 11 (𝑧 = 𝑍 → (𝑧 𝑢) = (𝑍 𝑢))
6059eqeq1d 2815 . . . . . . . . . 10 (𝑧 = 𝑍 → ((𝑧 𝑢) = (𝑐 𝑣) ↔ (𝑍 𝑢) = (𝑐 𝑣)))
6158, 60imbi12d 335 . . . . . . . . 9 (𝑧 = 𝑍 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6261ralbidv 3181 . . . . . . . 8 (𝑧 = 𝑍 → (∀𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
63622ralbidv 3184 . . . . . . 7 (𝑧 = 𝑍 → (∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
64632ralbidv 3184 . . . . . 6 (𝑧 = 𝑍 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6533, 50, 64rspc3v 3525 . . . . 5 ((𝑋𝑃𝑌𝑃𝑍𝑃) → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) → ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6615, 16, 17, 65syl3anc 1483 . . . 4 (𝜑 → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) → ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6714, 66mpd 15 . . 3 (𝜑 → ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)))
68 axtg5seg.7 . . . 4 (𝜑𝑈𝑃)
69 axtg5seg.4 . . . 4 (𝜑𝐴𝑃)
70 axtg5seg.5 . . . 4 (𝜑𝐵𝑃)
71 oveq2 6885 . . . . . . . . . . 11 (𝑢 = 𝑈 → (𝑋 𝑢) = (𝑋 𝑈))
7271eqeq1d 2815 . . . . . . . . . 10 (𝑢 = 𝑈 → ((𝑋 𝑢) = (𝑎 𝑣) ↔ (𝑋 𝑈) = (𝑎 𝑣)))
73 oveq2 6885 . . . . . . . . . . 11 (𝑢 = 𝑈 → (𝑌 𝑢) = (𝑌 𝑈))
7473eqeq1d 2815 . . . . . . . . . 10 (𝑢 = 𝑈 → ((𝑌 𝑢) = (𝑏 𝑣) ↔ (𝑌 𝑈) = (𝑏 𝑣)))
7572, 74anbi12d 618 . . . . . . . . 9 (𝑢 = 𝑈 → (((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)) ↔ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))
7675anbi2d 616 . . . . . . . 8 (𝑢 = 𝑈 → ((((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))))
7776anbi2d 616 . . . . . . 7 (𝑢 = 𝑈 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))))
78 oveq2 6885 . . . . . . . 8 (𝑢 = 𝑈 → (𝑍 𝑢) = (𝑍 𝑈))
7978eqeq1d 2815 . . . . . . 7 (𝑢 = 𝑈 → ((𝑍 𝑢) = (𝑐 𝑣) ↔ (𝑍 𝑈) = (𝑐 𝑣)))
8077, 79imbi12d 335 . . . . . 6 (𝑢 = 𝑈 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
81802ralbidv 3184 . . . . 5 (𝑢 = 𝑈 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) ↔ ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
82 oveq1 6884 . . . . . . . . . 10 (𝑎 = 𝐴 → (𝑎𝐼𝑐) = (𝐴𝐼𝑐))
8382eleq2d 2878 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑏 ∈ (𝑎𝐼𝑐) ↔ 𝑏 ∈ (𝐴𝐼𝑐)))
84833anbi3d 1559 . . . . . . . 8 (𝑎 = 𝐴 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐))))
85 oveq1 6884 . . . . . . . . . . 11 (𝑎 = 𝐴 → (𝑎 𝑏) = (𝐴 𝑏))
8685eqeq2d 2823 . . . . . . . . . 10 (𝑎 = 𝐴 → ((𝑋 𝑌) = (𝑎 𝑏) ↔ (𝑋 𝑌) = (𝐴 𝑏)))
8786anbi1d 617 . . . . . . . . 9 (𝑎 = 𝐴 → (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐))))
88 oveq1 6884 . . . . . . . . . . 11 (𝑎 = 𝐴 → (𝑎 𝑣) = (𝐴 𝑣))
8988eqeq2d 2823 . . . . . . . . . 10 (𝑎 = 𝐴 → ((𝑋 𝑈) = (𝑎 𝑣) ↔ (𝑋 𝑈) = (𝐴 𝑣)))
9089anbi1d 617 . . . . . . . . 9 (𝑎 = 𝐴 → (((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)) ↔ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))
9187, 90anbi12d 618 . . . . . . . 8 (𝑎 = 𝐴 → ((((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))))
9284, 91anbi12d 618 . . . . . . 7 (𝑎 = 𝐴 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))))
9392imbi1d 332 . . . . . 6 (𝑎 = 𝐴 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
94932ralbidv 3184 . . . . 5 (𝑎 = 𝐴 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
95 eleq1 2880 . . . . . . . . 9 (𝑏 = 𝐵 → (𝑏 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝑐)))
96953anbi3d 1559 . . . . . . . 8 (𝑏 = 𝐵 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐))))
97 oveq2 6885 . . . . . . . . . . 11 (𝑏 = 𝐵 → (𝐴 𝑏) = (𝐴 𝐵))
9897eqeq2d 2823 . . . . . . . . . 10 (𝑏 = 𝐵 → ((𝑋 𝑌) = (𝐴 𝑏) ↔ (𝑋 𝑌) = (𝐴 𝐵)))
99 oveq1 6884 . . . . . . . . . . 11 (𝑏 = 𝐵 → (𝑏 𝑐) = (𝐵 𝑐))
10099eqeq2d 2823 . . . . . . . . . 10 (𝑏 = 𝐵 → ((𝑌 𝑍) = (𝑏 𝑐) ↔ (𝑌 𝑍) = (𝐵 𝑐)))
10198, 100anbi12d 618 . . . . . . . . 9 (𝑏 = 𝐵 → (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐))))
102 oveq1 6884 . . . . . . . . . . 11 (𝑏 = 𝐵 → (𝑏 𝑣) = (𝐵 𝑣))
103102eqeq2d 2823 . . . . . . . . . 10 (𝑏 = 𝐵 → ((𝑌 𝑈) = (𝑏 𝑣) ↔ (𝑌 𝑈) = (𝐵 𝑣)))
104103anbi2d 616 . . . . . . . . 9 (𝑏 = 𝐵 → (((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)) ↔ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))))
105101, 104anbi12d 618 . . . . . . . 8 (𝑏 = 𝐵 → ((((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))))
10696, 105anbi12d 618 . . . . . . 7 (𝑏 = 𝐵 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))))))
107106imbi1d 332 . . . . . 6 (𝑏 = 𝐵 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
1081072ralbidv 3184 . . . . 5 (𝑏 = 𝐵 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
10981, 94, 108rspc3v 3525 . . . 4 ((𝑈𝑃𝐴𝑃𝐵𝑃) → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) → ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
11068, 69, 70, 109syl3anc 1483 . . 3 (𝜑 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) → ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
11167, 110mpd 15 . 2 (𝜑 → ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)))
112 axtg5seg.9 . . . 4 (𝜑𝑋𝑌)
113 axtg5seg.10 . . . 4 (𝜑𝑌 ∈ (𝑋𝐼𝑍))
114 axtg5seg.11 . . . 4 (𝜑𝐵 ∈ (𝐴𝐼𝐶))
115112, 113, 1143jca 1151 . . 3 (𝜑 → (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)))
116 axtg5seg.12 . . . 4 (𝜑 → (𝑋 𝑌) = (𝐴 𝐵))
117 axtg5seg.13 . . . 4 (𝜑 → (𝑌 𝑍) = (𝐵 𝐶))
118116, 117jca 503 . . 3 (𝜑 → ((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)))
119 axtg5seg.14 . . . 4 (𝜑 → (𝑋 𝑈) = (𝐴 𝑉))
120 axtg5seg.15 . . . 4 (𝜑 → (𝑌 𝑈) = (𝐵 𝑉))
121119, 120jca 503 . . 3 (𝜑 → ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))
122115, 118, 121jca32 507 . 2 (𝜑 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))))
123 axtg5seg.6 . . 3 (𝜑𝐶𝑃)
124 axtg5seg.8 . . 3 (𝜑𝑉𝑃)
125 oveq2 6885 . . . . . . . 8 (𝑐 = 𝐶 → (𝐴𝐼𝑐) = (𝐴𝐼𝐶))
126125eleq2d 2878 . . . . . . 7 (𝑐 = 𝐶 → (𝐵 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝐶)))
1271263anbi3d 1559 . . . . . 6 (𝑐 = 𝐶 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶))))
128 oveq2 6885 . . . . . . . . 9 (𝑐 = 𝐶 → (𝐵 𝑐) = (𝐵 𝐶))
129128eqeq2d 2823 . . . . . . . 8 (𝑐 = 𝐶 → ((𝑌 𝑍) = (𝐵 𝑐) ↔ (𝑌 𝑍) = (𝐵 𝐶)))
130129anbi2d 616 . . . . . . 7 (𝑐 = 𝐶 → (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ↔ ((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶))))
131130anbi1d 617 . . . . . 6 (𝑐 = 𝐶 → ((((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))))
132127, 131anbi12d 618 . . . . 5 (𝑐 = 𝐶 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))))))
133 oveq1 6884 . . . . . 6 (𝑐 = 𝐶 → (𝑐 𝑣) = (𝐶 𝑣))
134133eqeq2d 2823 . . . . 5 (𝑐 = 𝐶 → ((𝑍 𝑈) = (𝑐 𝑣) ↔ (𝑍 𝑈) = (𝐶 𝑣)))
135132, 134imbi12d 335 . . . 4 (𝑐 = 𝐶 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝐶 𝑣))))
136 oveq2 6885 . . . . . . . . 9 (𝑣 = 𝑉 → (𝐴 𝑣) = (𝐴 𝑉))
137136eqeq2d 2823 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑋 𝑈) = (𝐴 𝑣) ↔ (𝑋 𝑈) = (𝐴 𝑉)))
138 oveq2 6885 . . . . . . . . 9 (𝑣 = 𝑉 → (𝐵 𝑣) = (𝐵 𝑉))
139138eqeq2d 2823 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑌 𝑈) = (𝐵 𝑣) ↔ (𝑌 𝑈) = (𝐵 𝑉)))
140137, 139anbi12d 618 . . . . . . 7 (𝑣 = 𝑉 → (((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)) ↔ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉))))
141140anbi2d 616 . . . . . 6 (𝑣 = 𝑉 → ((((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))))
142141anbi2d 616 . . . . 5 (𝑣 = 𝑉 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉))))))
143 oveq2 6885 . . . . . 6 (𝑣 = 𝑉 → (𝐶 𝑣) = (𝐶 𝑉))
144143eqeq2d 2823 . . . . 5 (𝑣 = 𝑉 → ((𝑍 𝑈) = (𝐶 𝑣) ↔ (𝑍 𝑈) = (𝐶 𝑉)))
145142, 144imbi12d 335 . . . 4 (𝑣 = 𝑉 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝐶 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))) → (𝑍 𝑈) = (𝐶 𝑉))))
146135, 145rspc2v 3522 . . 3 ((𝐶𝑃𝑉𝑃) → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))) → (𝑍 𝑈) = (𝐶 𝑉))))
147123, 124, 146syl2anc 575 . 2 (𝜑 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))) → (𝑍 𝑈) = (𝐶 𝑉))))
148111, 122, 147mp2d 49 1 (𝜑 → (𝑍 𝑈) = (𝐶 𝑉))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3o 1099  w3a 1100   = wceq 1637  wcel 2157  {cab 2799  wne 2985  wral 3103  wrex 3104  {crab 3107  Vcvv 3398  [wsbc 3640  cdif 3773  cin 3775  {csn 4377  cfv 6104  (class class class)co 6877  cmpt2 6879  Basecbs 16071  distcds 16165  TarskiGcstrkg 25549  TarskiGCcstrkgc 25550  TarskiGBcstrkgb 25551  TarskiGCBcstrkgcb 25552  Itvcitv 25555  LineGclng 25556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-nul 4990
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-sbc 3641  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-br 4852  df-iota 6067  df-fv 6112  df-ov 6880  df-trkgcb 25569  df-trkg 25572
This theorem is referenced by:  tgcgrextend  25600  tgsegconeq  25601  tgifscgr  25623  tgfscgr  25683  tgbtwnconn1lem2  25688  tgbtwnconn1lem3  25689  miriso  25785  midexlem  25807  ragcgr  25822  footex  25833  lmiisolem  25908  f1otrg  25971  tg5segofs  31082
  Copyright terms: Public domain W3C validator