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

Theorem axtg5seg 25164
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 25152 . . . . . . 7 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2 inss2 3796 . . . . . . . 8 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
3 inss1 3795 . . . . . . . 8 (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) ⊆ TarskiGCB
42, 3sstri 3577 . . . . . . 7 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGCB
51, 4eqsstri 3598 . . . . . 6 TarskiG ⊆ TarskiGCB
6 axtrkg.g . . . . . 6 (𝜑𝐺 ∈ TarskiG)
75, 6sseldi 3566 . . . . 5 (𝜑𝐺 ∈ TarskiGCB)
8 axtrkg.p . . . . . . . 8 𝑃 = (Base‘𝐺)
9 axtrkg.d . . . . . . . 8 = (dist‘𝐺)
10 axtrkg.i . . . . . . . 8 𝐼 = (Itv‘𝐺)
118, 9, 10istrkgcb 25155 . . . . . . 7 (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)))))
1211simprbi 479 . . . . . 6 (𝐺 ∈ TarskiGCB → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
1312simpld 474 . . . . 5 (𝐺 ∈ TarskiGCB → ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)))
147, 13syl 17 . . . 4 (𝜑 → ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)))
15 axtg5seg.1 . . . . 5 (𝜑𝑋𝑃)
16 axtg5seg.2 . . . . 5 (𝜑𝑌𝑃)
17 axtg5seg.3 . . . . 5 (𝜑𝑍𝑃)
18 neeq1 2844 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑥𝑦𝑋𝑦))
19 oveq1 6556 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
2019eleq2d 2673 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
2118, 203anbi12d 1392 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
22 oveq1 6556 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (𝑥 𝑦) = (𝑋 𝑦))
2322eqeq1d 2612 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → ((𝑥 𝑦) = (𝑎 𝑏) ↔ (𝑋 𝑦) = (𝑎 𝑏)))
2423anbi1d 737 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ↔ ((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐))))
25 oveq1 6556 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (𝑥 𝑢) = (𝑋 𝑢))
2625eqeq1d 2612 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → ((𝑥 𝑢) = (𝑎 𝑣) ↔ (𝑋 𝑢) = (𝑎 𝑣)))
2726anbi1d 737 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)) ↔ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))))
2824, 27anbi12d 743 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))))
2921, 28anbi12d 743 . . . . . . . . . 10 (𝑥 = 𝑋 → (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))))))
3029imbi1d 330 . . . . . . . . 9 (𝑥 = 𝑋 → ((((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
3130ralbidv 2969 . . . . . . . 8 (𝑥 = 𝑋 → (∀𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
32312ralbidv 2972 . . . . . . 7 (𝑥 = 𝑋 → (∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
33322ralbidv 2972 . . . . . 6 (𝑥 = 𝑋 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
34 neeq2 2845 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (𝑋𝑦𝑋𝑌))
35 eleq1 2676 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
3634, 353anbi12d 1392 . . . . . . . . . . 11 (𝑦 = 𝑌 → ((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
37 oveq2 6557 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → (𝑋 𝑦) = (𝑋 𝑌))
3837eqeq1d 2612 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → ((𝑋 𝑦) = (𝑎 𝑏) ↔ (𝑋 𝑌) = (𝑎 𝑏)))
39 oveq1 6556 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → (𝑦 𝑧) = (𝑌 𝑧))
4039eqeq1d 2612 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → ((𝑦 𝑧) = (𝑏 𝑐) ↔ (𝑌 𝑧) = (𝑏 𝑐)))
4138, 40anbi12d 743 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐))))
42 oveq1 6556 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → (𝑦 𝑢) = (𝑌 𝑢))
4342eqeq1d 2612 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → ((𝑦 𝑢) = (𝑏 𝑣) ↔ (𝑌 𝑢) = (𝑏 𝑣)))
4443anbi2d 736 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)) ↔ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))))
4541, 44anbi12d 743 . . . . . . . . . . 11 (𝑦 = 𝑌 → ((((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))))
4636, 45anbi12d 743 . . . . . . . . . 10 (𝑦 = 𝑌 → (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))))))
4746imbi1d 330 . . . . . . . . 9 (𝑦 = 𝑌 → ((((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
4847ralbidv 2969 . . . . . . . 8 (𝑦 = 𝑌 → (∀𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
49482ralbidv 2972 . . . . . . 7 (𝑦 = 𝑌 → (∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
50492ralbidv 2972 . . . . . 6 (𝑦 = 𝑌 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
51 oveq2 6557 . . . . . . . . . . . . 13 (𝑧 = 𝑍 → (𝑋𝐼𝑧) = (𝑋𝐼𝑍))
5251eleq2d 2673 . . . . . . . . . . . 12 (𝑧 = 𝑍 → (𝑌 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑍)))
53523anbi2d 1396 . . . . . . . . . . 11 (𝑧 = 𝑍 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
54 oveq2 6557 . . . . . . . . . . . . . 14 (𝑧 = 𝑍 → (𝑌 𝑧) = (𝑌 𝑍))
5554eqeq1d 2612 . . . . . . . . . . . . 13 (𝑧 = 𝑍 → ((𝑌 𝑧) = (𝑏 𝑐) ↔ (𝑌 𝑍) = (𝑏 𝑐)))
5655anbi2d 736 . . . . . . . . . . . 12 (𝑧 = 𝑍 → (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐))))
5756anbi1d 737 . . . . . . . . . . 11 (𝑧 = 𝑍 → ((((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))))
5853, 57anbi12d 743 . . . . . . . . . 10 (𝑧 = 𝑍 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))))))
59 oveq1 6556 . . . . . . . . . . 11 (𝑧 = 𝑍 → (𝑧 𝑢) = (𝑍 𝑢))
6059eqeq1d 2612 . . . . . . . . . 10 (𝑧 = 𝑍 → ((𝑧 𝑢) = (𝑐 𝑣) ↔ (𝑍 𝑢) = (𝑐 𝑣)))
6158, 60imbi12d 333 . . . . . . . . 9 (𝑧 = 𝑍 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6261ralbidv 2969 . . . . . . . 8 (𝑧 = 𝑍 → (∀𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
63622ralbidv 2972 . . . . . . 7 (𝑧 = 𝑍 → (∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
64632ralbidv 2972 . . . . . 6 (𝑧 = 𝑍 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6533, 50, 64rspc3v 3296 . . . . 5 ((𝑋𝑃𝑌𝑃𝑍𝑃) → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) → ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6615, 16, 17, 65syl3anc 1318 . . . 4 (𝜑 → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) → ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6714, 66mpd 15 . . 3 (𝜑 → ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)))
68 axtg5seg.7 . . . 4 (𝜑𝑈𝑃)
69 axtg5seg.4 . . . 4 (𝜑𝐴𝑃)
70 axtg5seg.5 . . . 4 (𝜑𝐵𝑃)
71 oveq2 6557 . . . . . . . . . . 11 (𝑢 = 𝑈 → (𝑋 𝑢) = (𝑋 𝑈))
7271eqeq1d 2612 . . . . . . . . . 10 (𝑢 = 𝑈 → ((𝑋 𝑢) = (𝑎 𝑣) ↔ (𝑋 𝑈) = (𝑎 𝑣)))
73 oveq2 6557 . . . . . . . . . . 11 (𝑢 = 𝑈 → (𝑌 𝑢) = (𝑌 𝑈))
7473eqeq1d 2612 . . . . . . . . . 10 (𝑢 = 𝑈 → ((𝑌 𝑢) = (𝑏 𝑣) ↔ (𝑌 𝑈) = (𝑏 𝑣)))
7572, 74anbi12d 743 . . . . . . . . 9 (𝑢 = 𝑈 → (((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)) ↔ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))
7675anbi2d 736 . . . . . . . 8 (𝑢 = 𝑈 → ((((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))))
7776anbi2d 736 . . . . . . 7 (𝑢 = 𝑈 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))))
78 oveq2 6557 . . . . . . . 8 (𝑢 = 𝑈 → (𝑍 𝑢) = (𝑍 𝑈))
7978eqeq1d 2612 . . . . . . 7 (𝑢 = 𝑈 → ((𝑍 𝑢) = (𝑐 𝑣) ↔ (𝑍 𝑈) = (𝑐 𝑣)))
8077, 79imbi12d 333 . . . . . 6 (𝑢 = 𝑈 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
81802ralbidv 2972 . . . . 5 (𝑢 = 𝑈 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) ↔ ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
82 oveq1 6556 . . . . . . . . . 10 (𝑎 = 𝐴 → (𝑎𝐼𝑐) = (𝐴𝐼𝑐))
8382eleq2d 2673 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑏 ∈ (𝑎𝐼𝑐) ↔ 𝑏 ∈ (𝐴𝐼𝑐)))
84833anbi3d 1397 . . . . . . . 8 (𝑎 = 𝐴 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐))))
85 oveq1 6556 . . . . . . . . . . 11 (𝑎 = 𝐴 → (𝑎 𝑏) = (𝐴 𝑏))
8685eqeq2d 2620 . . . . . . . . . 10 (𝑎 = 𝐴 → ((𝑋 𝑌) = (𝑎 𝑏) ↔ (𝑋 𝑌) = (𝐴 𝑏)))
8786anbi1d 737 . . . . . . . . 9 (𝑎 = 𝐴 → (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐))))
88 oveq1 6556 . . . . . . . . . . 11 (𝑎 = 𝐴 → (𝑎 𝑣) = (𝐴 𝑣))
8988eqeq2d 2620 . . . . . . . . . 10 (𝑎 = 𝐴 → ((𝑋 𝑈) = (𝑎 𝑣) ↔ (𝑋 𝑈) = (𝐴 𝑣)))
9089anbi1d 737 . . . . . . . . 9 (𝑎 = 𝐴 → (((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)) ↔ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))
9187, 90anbi12d 743 . . . . . . . 8 (𝑎 = 𝐴 → ((((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))))
9284, 91anbi12d 743 . . . . . . 7 (𝑎 = 𝐴 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))))
9392imbi1d 330 . . . . . 6 (𝑎 = 𝐴 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
94932ralbidv 2972 . . . . 5 (𝑎 = 𝐴 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
95 eleq1 2676 . . . . . . . . 9 (𝑏 = 𝐵 → (𝑏 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝑐)))
96953anbi3d 1397 . . . . . . . 8 (𝑏 = 𝐵 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐))))
97 oveq2 6557 . . . . . . . . . . 11 (𝑏 = 𝐵 → (𝐴 𝑏) = (𝐴 𝐵))
9897eqeq2d 2620 . . . . . . . . . 10 (𝑏 = 𝐵 → ((𝑋 𝑌) = (𝐴 𝑏) ↔ (𝑋 𝑌) = (𝐴 𝐵)))
99 oveq1 6556 . . . . . . . . . . 11 (𝑏 = 𝐵 → (𝑏 𝑐) = (𝐵 𝑐))
10099eqeq2d 2620 . . . . . . . . . 10 (𝑏 = 𝐵 → ((𝑌 𝑍) = (𝑏 𝑐) ↔ (𝑌 𝑍) = (𝐵 𝑐)))
10198, 100anbi12d 743 . . . . . . . . 9 (𝑏 = 𝐵 → (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐))))
102 oveq1 6556 . . . . . . . . . . 11 (𝑏 = 𝐵 → (𝑏 𝑣) = (𝐵 𝑣))
103102eqeq2d 2620 . . . . . . . . . 10 (𝑏 = 𝐵 → ((𝑌 𝑈) = (𝑏 𝑣) ↔ (𝑌 𝑈) = (𝐵 𝑣)))
104103anbi2d 736 . . . . . . . . 9 (𝑏 = 𝐵 → (((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)) ↔ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))))
105101, 104anbi12d 743 . . . . . . . 8 (𝑏 = 𝐵 → ((((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))))
10696, 105anbi12d 743 . . . . . . 7 (𝑏 = 𝐵 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))))))
107106imbi1d 330 . . . . . 6 (𝑏 = 𝐵 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
1081072ralbidv 2972 . . . . 5 (𝑏 = 𝐵 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
10981, 94, 108rspc3v 3296 . . . 4 ((𝑈𝑃𝐴𝑃𝐵𝑃) → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) → ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
11068, 69, 70, 109syl3anc 1318 . . 3 (𝜑 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) → ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
11167, 110mpd 15 . 2 (𝜑 → ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)))
112 axtg5seg.9 . . . 4 (𝜑𝑋𝑌)
113 axtg5seg.10 . . . 4 (𝜑𝑌 ∈ (𝑋𝐼𝑍))
114 axtg5seg.11 . . . 4 (𝜑𝐵 ∈ (𝐴𝐼𝐶))
115112, 113, 1143jca 1235 . . 3 (𝜑 → (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)))
116 axtg5seg.12 . . . 4 (𝜑 → (𝑋 𝑌) = (𝐴 𝐵))
117 axtg5seg.13 . . . 4 (𝜑 → (𝑌 𝑍) = (𝐵 𝐶))
118116, 117jca 553 . . 3 (𝜑 → ((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)))
119 axtg5seg.14 . . . 4 (𝜑 → (𝑋 𝑈) = (𝐴 𝑉))
120 axtg5seg.15 . . . 4 (𝜑 → (𝑌 𝑈) = (𝐵 𝑉))
121119, 120jca 553 . . 3 (𝜑 → ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))
122115, 118, 121jca32 556 . 2 (𝜑 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))))
123 axtg5seg.6 . . 3 (𝜑𝐶𝑃)
124 axtg5seg.8 . . 3 (𝜑𝑉𝑃)
125 oveq2 6557 . . . . . . . 8 (𝑐 = 𝐶 → (𝐴𝐼𝑐) = (𝐴𝐼𝐶))
126125eleq2d 2673 . . . . . . 7 (𝑐 = 𝐶 → (𝐵 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝐶)))
1271263anbi3d 1397 . . . . . 6 (𝑐 = 𝐶 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶))))
128 oveq2 6557 . . . . . . . . 9 (𝑐 = 𝐶 → (𝐵 𝑐) = (𝐵 𝐶))
129128eqeq2d 2620 . . . . . . . 8 (𝑐 = 𝐶 → ((𝑌 𝑍) = (𝐵 𝑐) ↔ (𝑌 𝑍) = (𝐵 𝐶)))
130129anbi2d 736 . . . . . . 7 (𝑐 = 𝐶 → (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ↔ ((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶))))
131130anbi1d 737 . . . . . 6 (𝑐 = 𝐶 → ((((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))))
132127, 131anbi12d 743 . . . . 5 (𝑐 = 𝐶 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))))))
133 oveq1 6556 . . . . . 6 (𝑐 = 𝐶 → (𝑐 𝑣) = (𝐶 𝑣))
134133eqeq2d 2620 . . . . 5 (𝑐 = 𝐶 → ((𝑍 𝑈) = (𝑐 𝑣) ↔ (𝑍 𝑈) = (𝐶 𝑣)))
135132, 134imbi12d 333 . . . 4 (𝑐 = 𝐶 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝐶 𝑣))))
136 oveq2 6557 . . . . . . . . 9 (𝑣 = 𝑉 → (𝐴 𝑣) = (𝐴 𝑉))
137136eqeq2d 2620 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑋 𝑈) = (𝐴 𝑣) ↔ (𝑋 𝑈) = (𝐴 𝑉)))
138 oveq2 6557 . . . . . . . . 9 (𝑣 = 𝑉 → (𝐵 𝑣) = (𝐵 𝑉))
139138eqeq2d 2620 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑌 𝑈) = (𝐵 𝑣) ↔ (𝑌 𝑈) = (𝐵 𝑉)))
140137, 139anbi12d 743 . . . . . . 7 (𝑣 = 𝑉 → (((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)) ↔ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉))))
141140anbi2d 736 . . . . . 6 (𝑣 = 𝑉 → ((((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))))
142141anbi2d 736 . . . . 5 (𝑣 = 𝑉 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉))))))
143 oveq2 6557 . . . . . 6 (𝑣 = 𝑉 → (𝐶 𝑣) = (𝐶 𝑉))
144143eqeq2d 2620 . . . . 5 (𝑣 = 𝑉 → ((𝑍 𝑈) = (𝐶 𝑣) ↔ (𝑍 𝑈) = (𝐶 𝑉)))
145142, 144imbi12d 333 . . . 4 (𝑣 = 𝑉 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝐶 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))) → (𝑍 𝑈) = (𝐶 𝑉))))
146135, 145rspc2v 3293 . . 3 ((𝐶𝑃𝑉𝑃) → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))) → (𝑍 𝑈) = (𝐶 𝑉))))
147123, 124, 146syl2anc 691 . 2 (𝜑 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))) → (𝑍 𝑈) = (𝐶 𝑉))))
148111, 122, 147mp2d 47 1 (𝜑 → (𝑍 𝑈) = (𝐶 𝑉))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3o 1030  w3a 1031   = wceq 1475  wcel 1977  {cab 2596  wne 2780  wral 2896  wrex 2897  {crab 2900  Vcvv 3173  [wsbc 3402  cdif 3537  cin 3539  {csn 4125  cfv 5804  (class class class)co 6549  cmpt2 6551  Basecbs 15695  distcds 15777  TarskiGcstrkg 25129  TarskiGCcstrkgc 25130  TarskiGBcstrkgb 25131  TarskiGCBcstrkgcb 25132  Itvcitv 25135  LineGclng 25136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-trkgcb 25149  df-trkg 25152
This theorem is referenced by:  tgcgrextend  25180  tgsegconeq  25181  tgifscgr  25203  tgfscgr  25263  tgbtwnconn1lem2  25268  tgbtwnconn1lem3  25269  miriso  25365  midexlem  25387  ragcgr  25402  footex  25413  lmiisolem  25488  f1otrg  25551  tg5segofs  30004
  Copyright terms: Public domain W3C validator